Homotopy Type Theory realizability > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Idea

< realizability

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.

References

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

Last revised on June 9, 2022 at 19:05:46. See the history of this page for a list of all contributions to it.