Towards a constructive simplicial model of Univalent Foundations

DOI10.1112/jlms.12532zbMath1527.18022arXiv1905.06281OpenAlexW2945484163MaRDI QIDQ6176777

Simon Henry, Nicola Gambino

Publication date: 24 August 2023

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

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

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• The identity type weak factorisation system
• On the strength of dependent products in the type theory of Martin-Löf
• Categorical logic and type theory
• Locally cartesian closed exact completions
• A cubical model of homotopy type theory
• The Frobenius condition, right properness, and uniform fibrations
• The simplicial model of univalent foundations (after Voevodsky)
• Revisiting the categorical interpretation of dependent type theory
• Topological and Simplicial Models of Identity Types
• The Local Universes Model
• Weak model categories in classical and constructive mathematics
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Explicit substitutions
• Homotopy Type Theory: Univalent Foundations of Mathematics
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories
• A generalization of the Takeuti–Gandy interpretation
• W-types in homotopy type theory
• Univalence for inverse diagrams and homotopy canonicity
• An experimental library of formalized Mathematics based on the univalent foundations
• The Constructive Kan–Quillen Model Structure: Two New Proofs
• Understanding the small object argument
• The univalence axiom for elegant Reedy presheaves

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