An Abstract Look at Realizability

Abstract This paper is about the combinatorial properties necessary for the construction of realizability models with certain type-theoretic properties. We take as our basic construction a form of tagging in which elements of sets are equipped with tags, and functions must operate constructively on tags. To complete the construction we allow a form of closure under quotients by equivalence relations. In this paper we analyse first the condition for a natural monoidal structure to be product structure, and then investigate necessary conditions for the realizability model to be locally cartesian closed and to have a subobject classifier.

Authors

• Edmund Robinson
• Giuseppe Rosolini

Keywords

No keywords are indexed for this paper.