On the ∞$\infty$‐topos semantics of homotopy type theory

DOI10.1112/blms.12997arXiv2212.06937OpenAlexW4392108299MaRDI QIDQ6150054

Emily Riehl

Publication date: 5 March 2024

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

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

Mathematics Subject Classification ID

Simplicial sets and complexes in algebraic topology (55U10) Topological categories, foundations of homotopy theory (55U40) Homotopical algebra, Quillen model categories, derivators (18N40) Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60) 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
• Survey article: an elementary illustrated introduction to simplicial sets
• Homotopical algebraic geometry. I: Topos theory
• Homotopy-theoretic aspects of 2-monads
• The identity type weak factorisation system
• Comprehension categories and the semantics of type dependency
• The Frobenius condition, right properness, and uniform fibrations
• The simplicial model of univalent foundations (after Voevodsky)
• Injective and projective model structures on enriched diagram categories
• Homotopical algebra
• Homotopy type theory and Voevodsky’s univalent foundations
• The Local Universes Model
• Types are weak ω -groupoids
• Natural models of homotopy type theory
• Voevodsky’s Univalence Axiom in Homotopy Type Theory
• Elements of ∞-Category Theory
• A C-system defined by a universe category
• Homotopy theoretic models of identity types
• Weak ω-Categories from Intensional Type Theory
• Internal type theory
• Semantics of higher inductive types
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• The Geometric Realization of a Kan Fibration is a Serre Fibration
• Universal homotopy theories
• Combinatorial model categories have presentations
• The univalence axiom for elegant Reedy presheaves

This page was built for publication: On the ∞$\infty$‐topos semantics of homotopy type theory