Towards a constructive simplicial model of Univalent Foundations

Abstract

We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of univalent foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent classifying fibration for small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, $\Sigma$-types, $\Pi$-types and a univalent universe, leaving only a coherence question to be addressed.

v3: changed the definition of the type Weq(U) of weak equivalences to fix a problem with constructivity. Other Minor changes. 31 pages

References in corpus (15)

• Understanding the small object argument
• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Univalence for inverse diagrams and homotopy canonicity
• The Frobenius Condition, Right Properness, and Uniform Fibrations
• On the strength of dependent products in the type theory of Martin-Löf
• Axioms for Modelling Cubical Type Theory in a Topos
• Univalence in Simplicial Sets
• All $(\infty ,1)$-toposes have strict univalent universes
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• The Equivalence Extension Property and Model Structures
• Weak model categories in classical and constructive mathematics
• The constructive Kan-Quillen model structure: two new proofs
• A constructive account of the Kan-Quillen model structure and of Kan's Ex${}^{\infty }$ functor

Cited by in corpus (8)

• Weak model categories in classical and constructive mathematics
• The constructive Kan-Quillen model structure: two new proofs
• Models of Martin-Löf type theory from algebraic weak factorisation systems
• A constructive account of the Kan-Quillen model structure and of Kan's Ex${}^{\infty }$ functor
• Relative elegance and cartesian cubes with one connection
• Toward the effective 2-topos
• The derivator of setoids
• Stable factorization from a fibred algebraic weak factorization system