Homotopy Type Theory realizability > history (Rev #2)

Idea

One possible way to find a computational interpretation for univalence is to interpret it in using realizability. Stekelburg provides a univalent universe of modest Kan complexes.

Simplicial homotopy theory can be developed in an extensive locally cartesian closed category $A$. Such categories are also called Heyting bialgebras?. The category $A$ has a class of small maps which has a bundle of small assemblies. This provides an internal Heyting bialgebra? $S$ which we can use as a target for simplicial `sets'. There is a (Kan-) model structure on these simplicial sets.

Within $S$ we can define a universe $M$ and show that it is fibrant. This universe is even univalent.

Now, the category of assemblies in number realizability provides such a Heyting bialgebra. The modest sets, a small internally complete full subcategory, provide the univalent universe. Note that modest sets are an impredicative universe. It models the calculus of constructions.

References

Wouter Stekelenburg, Realizability of Univalence: Modest Kan complexes, arXiv