The homotopy theory of type theories

DOI10.1016/J.AIM.2018.08.003zbMATH Open1397.18015arXiv1610.00037OpenAlexW2964239360MaRDI QIDQ1785779FDOQ1785779

Authors: Krzysztof Kapulkin, Peter Lefanu Lumsdaine 

Publication date: 1 October 2018

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

Abstract: We construct a left semi-model structure on the category of intensional type theories (precisely, on $mathrmCxlCa{t}_{Id,1,Sigma(,P{i}_{ext})}$). This presents an $infty$-category of such type theories; we show moreover that there is an $infty$-functor $mathrm{Cl}_{i}nfty$ from there to the $infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

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

Recommendations

• Homotopy-theoretic models of type theory
• Homotopy type theory
• Homotopy Type Theory
• Type theory and homotopy
• Homotopy type theory and the formalization of mathematics
• Homotopy Type Theory: A synthetic approach to higher equalities
• Homotopy type theory. Univalent foundations of mathematics
• Homotopy type theory and Voevodsky's univalent foundations
• Higher Structures in Homotopy Type Theory
• The Hurewicz theorem in homotopy type theory

zbMATH Keywords

internal languagemodel categoryhigher category theoryhomotopy type theory (HoTT)

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Higher Topos Theory (AM-170)
• Homotopy type theory. Univalent foundations of mathematics
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• A characterization of simplicial localization functors and a discussion of DK equivalences
• Towards an axiomatization of the theory of higher categories
• Abstract homotopy theory and generalized sheaf cohomology
• On left and right model categories and left and right Bousfield localizations
• Operads, algebras and modules in model categories and motives
• Two-dimensional models of type theory
• Quasicategories of frames of cofibration categories
• On the algebraic \(K\)-theory of higher categories
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves
• Title not available (Why is that?)
• Homotopy limits in type theory
• Univalence for inverse EI diagrams
• Products of families of types and (Pi,lambda)-structures on C-systems
• Subsystems and regular quotients of C-systems
• Locally Cartesian closed quasi-categories from type theory
• A C-system defined by a universe category

Cited In (37)

• Synthetic topology in Homotopy Type Theory for probabilistic programming
• $L'$-localization in an $\infty$-topos
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• Non-accessible localizations
• Extending homotopy type theory with strict equality
• A general framework for the semantics of type theory
• Characterizations of modalities and lex modalities
• Nilpotent types and fracture squares in homotopy type theory
• Homology groups of types in stable theories and the Hurewicz correspondence
• Mathesis Universalis and Homotopy Type Theory
• Semantics of higher inductive types
• Homotopy type theory as internal languages of diagrams of \(\infty\)-logoses
• Homotopy Type Theory: A synthetic approach to higher equalities
• Univalent completion
• The Hurewicz theorem in homotopy type theory
• Principal type-schemes and condensed detachment
• Higher Structures in Homotopy Type Theory
• Higher inductive types as homotopy-initial algebras
• Towards Constructive Homological Algebra in Type Theory
• Title not available (Why is that?)
• Indexed type theories
• A type theory for strictly unital \(\infty \)-categories
• The space of strong types and an open map theorem
• Localization in Homotopy Type Theory
• Modalities in homotopy type theory
• Modal dependent type theory and dependent right adjoints
• Homotopy Type Theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• A type theory for synthetic \(\infty\)-categories
• Types for Proofs and Programs
• The symbol of type and the Wilson theorem
• The role of compactification theory in the type problem
• Weak ω-Categories from Intensional Type Theory
• Internal languages of finitely complete \((\infty , 1)\)-categories
• Homotopical inverse diagrams in categories with attributes
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Cellular Cohomology in Homotopy Type Theory

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

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