Remarks on abstract structures of propositions and realizers

TL;DR

This paper introduces an abstract framework called PR-structures that models propositions and realizers, characterizes when these structures form preorderal and posetal doctrines, and examines their connection to partial applicative structures.

Contribution

It proposes a novel abstract notion of PR-structures and characterizes their properties, especially in relation to preorderal and posetal doctrines, with a focus on partial applicative structures.

Findings

PR-structures induce set-based contravariant functors

Characterization of PR-structures leading to preorderal and posetal doctrines

Analysis of PR-structures derived from partial applicative structures

Abstract

We present here an abstract notion of structure consisting of propositions and realizers (which we call PR-structures) giving rise to set based contravariant functors taking values in the category of sets endowed with binary relations. We will characterize those PR-structures giving rise to preorderal and posetal doctrines and we will study in particular the case of a PR-structure induced by a partial applicative structure.