Univalence in Simplicial Sets

Abstract

We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.

13 pages. Not intended for publication. An extended version appears as "The Simplicial Model of Univalent Foundations (after Voevodsky)", arXiv:1211.2851, presenting the logical as well as the homotopy-theoretic aspects of the model

Cited by in corpus (6)

• An introduction to univalent foundations for mathematicians
• Univalence in locally cartesian closed infinity-categories
• Towards a constructive simplicial model of Univalent Foundations
• Notes on Clans and Tribes
• Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
• A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom