Towards a constructive simplicial model of Univalent Foundations

DOI10.1112/JLMS.12532MaRDI QIDQ6176777zbMATH OpenOpenAlexFDO

Authors Nicola Gambino, Simon Henry

Publication date 24 August 2023

Published in Journal of the London Mathematical Society (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1905.06281

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

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.

Recommendations

• The simplicial model of univalent foundations (after Voevodsky)
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Effective Kan fibrations in simplicial sets
• Homotopy type theory and Voevodsky's univalent foundations
• Univalent foundations of mathematics

Cites work

• A cubical model of homotopy type theory
• A generalization of the Takeuti-Gandy interpretation
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• An experimental library of formalized mathematics based on the univalent foundations
• Categorical logic and type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Explicit substitutions
• Homotopy theoretic models of identity types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 445156 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 7003193 (Why is no real title available?)
• scientific article; zbMATH DE number 5219541 (Why is no real title available?)
• scientific article; zbMATH DE number 3264757 (Why is no real title available?)
• Locally cartesian closed exact completions
• Natural weak factorization systems.
• Non-constructivity in Kan simplicial sets
• On the strength of dependent products in the type theory of Martin-Löf
• Revisiting the categorical interpretation of dependent type theory
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The Constructive Kan–Quillen Model Structure: Two New Proofs
• The Frobenius condition, right properness, and uniform fibrations
• The identity type weak factorisation system
• The local universes model: an overlooked coherence construction for dependent type theories
• The simplicial model of univalent foundations (after Voevodsky)
• The univalence axiom for elegant Reedy presheaves
• Topological and simplicial models of identity types
• Understanding the small object argument
• Univalence for inverse diagrams and homotopy canonicity
• W-types in homotopy type theory
• Weak model categories in classical and constructive mathematics

Cited in

(9)

• Constructive sheaf models of type theory
• A Constructive Model of Directed Univalence in Bicubical Sets
• Simplicial sets inside cubical sets
• The Constructive Kan–Quillen Model Structure: Two New Proofs
• On notions of compactness, object classifiers, and weak Tarski universes
• Kripke-Joyal forcing for type theory and uniform fibrations
• Formalizing the algebraic small object argument in UniMath
• Toward the effective 2-topos
• The equivariant model structure on cartesian cubical sets

This page was built for publication: Towards a constructive simplicial model of Univalent Foundations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6176777)