Showing changes from revision #2 to #3:
Added | Removed | Changed
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 . Such categories are also called Heyting bialgebras?. The category has a class of small maps which has a bundle of small assemblies. This provides an internal Heyting bialgebra? which we can use as a target for simplicial `sets'. There is a (Kan-) model structure on these simplicial sets.
Within we can define a universe 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 June 9, 2022 at 19:05:46. See the history of this page for a list of all contributions to it.