Homotopy Type Theory


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 AA. Such categories are also called Heyting bialgebras?. The category AA has a class of small maps which has a bundle of small assemblies. This provides an internal Heyting bialgebra? SS which we can use as a target for simplicial `sets'. There is a (Kan-) model structure on these simplicial sets.

Within SS we can define a universe MM 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.


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

Last revised on March 15, 2015 at 00:01:43. See the history of this page for a list of all contributions to it.