The Equivalence Extension Property and Model Structures

Abstract

We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex^infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.

v4: made main theorem statement self-contained, minor reorganization of corollaries, fixed typos

References in corpus (2)

• The identity type weak factorisation system
• Cubical Type Theory: a constructive interpretation of the univalence axiom

Cited by in corpus (9)

• Internal Universes in Models of Homotopy Type Theory
• Towards a constructive simplicial model of Univalent Foundations
• W-Types with Reductions and the Small Object Argument
• Models of Martin-Löf type theory from algebraic weak factorisation systems
• Lifting Problems in Grothendieck Fibrations
• Identity Types in Algebraic Model Structures and Cubical Sets
• Kripke-Joyal forcing for type theory and uniform fibrations
• Constructive homotopy theory of marked semisimplicial sets
• Stable factorization from a fibred algebraic weak factorization system