Experiments with Realizability in Univalent Type Theory

This project formalises categorical realizability from the ground up in Cubical Agda.

Notable results include :

• The category of assemblies having all finite limits and being cartesian closed
• Modest sets are equivalent to partial surjections from the combinatory algebra
• The construction of the subquotient embedding from PERs to modest sets and that it is split essentially surjective on objects
• The internal logic of the realizability tripos
• The construction of the realizability topos

Current formalisation targets include :

• Uniform families of PERs indexed by assemblies form a small and complete fibration
• The category of assemblies is exactly the category of double negation separated objects of the realizability topos