Relative elegance and cartesian cubes with one connection

Abstract

We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.

61 pages. v6: Version accepted to Canadian Journal of Mathematics, modulo copy-editing

References in corpus (9)

• Understanding the small object argument
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• On an extension of the notion of Reedy category
• The local universes model: an overlooked coherence construction for dependent type theories
• The Frobenius Condition, Right Properness, and Uniform Fibrations
• Internal Universes in Models of Homotopy Type Theory
• Towards a constructive simplicial model of Univalent Foundations
• The constructive Kan-Quillen model structure: two new proofs
• Induced model structures for higher categories