The homotopy theory of type theories

Abstract

We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCa}{\mathrm{t}}_{\mathrm{Id},1,\mathrm{\Sigma }(,{\mathrm{\Pi }}_{\mathrm{ext}})}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor ${\mathrm{Cl}}_{\infty }$ 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.

arXiv commentv2: revised for release of companion paper arXiv:1808.01816; some theorem numbering changes

References in corpus (12)

• Higher Topos Theory
• On the algebraic K-theory of higher categories
• Operads, Algebras and Modules in General Model Categories
• Univalence for inverse diagrams and homotopy canonicity
• Two-dimensional models of type theory
• Homotopy limits in type theory
• On The Space-Time Fractional Schrödinger Equation with time independent potentials
• Notes on Clans and Tribes
• A C-system defined by a universe category
• Two Models for the Homotopy Theory of Cocomplete Homotopy Theories
• Martin-Lof identity types in the C-systems defined by a universe category
• Locally Cartesian Closed Quasicategories from Type Theory

Cited by in corpus (9)

• A General Framework for the Semantics of Type Theory
• All $(\infty ,1)$-toposes have strict univalent universes
• Nilpotent Types and Fracture Squares in Homotopy Type Theory
• The Hurewicz theorem in Homotopy Type Theory
• Homotopical inverse diagrams in categories with attributes
• Coherence of strict equalities in dependent type theories
• Characterizations of modalities and lex modalities
• Non-accessible localizations
• Central H-spaces and banded types