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