Experiments with Realizability in Univalent Type Theory

This repository contains code for a formalisation of categorical realisability in cubical type theory.

This project is very much a work-in-progress and undergoing active hackery. As of right now, Agda will not type-check things with `–safe` enabled.

Here you can find both a timeline and an agenda of the formalisation. Some things are only formalised to the extent necessary.

Combinatory Algebras

[X] Applicative Structures
[X] Feferman structure on an AS
[X] Combinatorial completeness
[X] Computation rule for $λ*$
Combinators
- [X] Identity, booleans, if-then-else, pairs, projections, B combinator, some Curry numerals
- [X] Computation rule for pairs
- [ ] Fixpoint combinators and primitive recursion combinator

Category of Assemblies

Definition, limits and colimits

[X] Define assemblies
[X] Define the category $\mathsf{Asm}$
[X] Cartesian closure and similar structure
- [X] Binary products
- [X] Binary coproducts
- [X] Equalisers
- [X] Exponentials
- [X] Initial and terminal objects
- [X] Coequalisers

Regular and exact

[ ] $\mathsf{Asm}$ is regular (requires Axiom of Choice)
- [x] Kernel pairs of morphisms exist
- [x] Kernel pairs have coequalisers
- [ ] Regular epics stable under pullback
[ ] Exact completion
- [x] Internal equivalence relations of a category
- [ ] Functional relations

Tripos to Topos Construction

See PR #6

A valued Predicates

[X] Heyting-valued Predicates
[X] $∀$ and $∃$ are adjoints
[X] Beck-Chevalley condition
[X] Heyting prealgebra structure
[X] Interpret intuitionistic logic

Realisability Topos

[X] Partial Equivalence Relations
[X] Functional Relations
[X] Morphisms and RT is a category
[X] Finite limits
- [X] Terminal object
- [X] Binary products
- [X] Equalisers (can be shown to merely exist)
[X] Power objects
- [-] Monomorphisms
- [ ] Subobjects and pullbacks lemmas
- [ ] Power objects exist