The homotopy theory of type theories

DOI10.1016/J.AIM.2018.08.003zbMath1397.18015arXiv1610.00037OpenAlexW2964239360MaRDI QIDQ1785779

Krzysztof Kapulkin, Peter LeFanu Lumsdaine

Publication date: 1 October 2018

Published in: Advances in Mathematics (Search for Journal in Brave)

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

zbMATH Keywords

model categoryinternal languagehigher category theoryhomotopy type theory (HoTT)

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Categorical semantics of formal languages (18C50)

Related Items (12)

Localization in Homotopy Type Theory ⋮ Univalent completion ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ The Hurewicz theorem in homotopy type theory ⋮ A general framework for the semantics of type theory ⋮ Homotopical inverse diagrams in categories with attributes ⋮ Nilpotent types and fracture squares in homotopy type theory ⋮ Characterizations of modalities and lex modalities ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Unnamed Item ⋮ Semantics of higher inductive types ⋮ Modal dependent type theory and dependent right adjoints

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On left and right model categories and left and right Bousfield localizations
• A characterization of simplicial localization functors and a discussion of DK equivalences
• Univalence for inverse EI diagrams
• Quasicategories of frames of cofibration categories
• Towards an axiomatization of the theory of higher categories
• On the algebraicK-theory of higher categories
• Products of families of types and (Pi,lambda)-structures on C-systems
• Subsystems and regular quotients of C-systems
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• Locally cartesian closed quasi‐categories from type theory
• Two-dimensional models of type theory
• A C-system defined by a universe category
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• Abstract homotopy theory and generalized sheaf cohomology
• Homotopy limits in type theory
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves

This page was built for publication: The homotopy theory of type theories