rahulc29/realizability

Experiments with Realizability in Univalent Type Theory

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

realizability's Issues

Perform major refactor

Break Assembly.agda into

• Base - definition
• Morphism - definition and basic lemmas
• Asm is a category
• Binary products + terminal
• Binary coproducts + initial
• Exponentials
• Coequalizers
• Equalizers
• Regular epi characterisation lemma
• Asm is a regular category

Complete the construction of the partiality monad

1. Add the induction principle for the partiality monad
2. Define >>= and >>>
3. Prove the monad laws

Fix workflows

Currently the workflow does not work properly so an ad-hoc method of building HTML locally has been applied.

Tripos to Topos Construction

Formalise the tripos to topos construction.

Automate intuitionistic logic

Write a prover for intuitionistic logic and get the tripos-to-topos construction working using that.

Potential ideas :

1. Tableaux for Intutionistic Logics, from Handbook of Tableaux Logics
2. A Tableau Decision Procedure for Propositional Intuitionistic Logic

Construct the effective topos

Depends on #7.
With $\mathcal{K}_1$ in hand, proceed with a similar tripos-to-topos construction and construct the effective topos.

Separate data structures from logical structures

Right now, everything is in a single Agda record. Refactor into

1. IsPartialityAlgebra
2. IsBinaryApplicativeStructure
3. IsPartialCombinatoryAlgebra

This makes for cleaner code and allows for cleaner distinction between property and structure since most of these are probably properties.

Migrate from `.agda` to `.lagda.md`

Convert to literate programming. The code is very unreadable.

Add models of combinatory algebras

Add (at least) the following models of combinatory algebras :

1. $\lambda$ calculus terms with $\beta$ equality
2. $\lambda$ calculus terms with $\beta \eta$ equality
3. $\lambda$ calculus terms with the equational theory generated by their Bohm trees
4. Scott's $D_{\infty}$
5. Scott's graph model (and other graph models too maybe?)

Refactor assemblies and tripos modules

When I refactored some of the topos modules, I forgot to do it for assemblies and the tripos modules.

Treat partiality and construct Kleene's first algebra

An outline :

1. Define the lifting monad $\mathcal{L}$
2. Define the syntax primitive recursive functions
3. Define $\mu$
4. Interpret the syntax of partial recursive functions using the $\mathcal{L}$
5. Use the syntax of partial recursive functions to create a (partial) combinatory algbera. No need for Godel codes.
6. This should be equivalent to Kleene's first algebra.

Prove uniqueness of morphism from `♯ A` to any partiality algebra is unique

I've formalised the initiality condition by saying that the Hom-space is contractible.

Refactor into using `opaque/unfolding`

Especially considering that using set quotients seems to create large ugly hcomps which take forever to type-check, it is necessary to control unfolding.

Classical Realizability

Add stuff about realisability algebras of Krivine and how they create a tripos that yields a Boolean topos. There's also $\lambda_c$ calculus and all the cool ZF models.

Polymorphism and Partial Equivalence Relations

To be formalised.