Homotopy theoretic models of identity types

By S. Awodey, M. Warren. Mathematical Proceedings of the Cambridge Philosophical Society, 2007

277 citations recorded by the source corpus.

Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11, 12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature.

Subfields: Artificial Intelligence, Geometry and Topology, Mathematical Physics

View Paper: https://www.semanticscholar.org/paper/a023d966f31a20b81e5cbc76c44799d4af5cbf0e

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Geometry and Topology

In Mathematical Physics

Citations in the corpus

Types are weak ω‐groupoids (2008, methodology): “Using the machinery of abstract homotopy theory, this analogy has been given a precise form in [1], which constructs type-theoretic structures from homotopy-theoretic ones, and in [6], which does the converse.”
Algebraic weak factorisation systems I: Accessible AWFS☆ (2014, background): “Weak factorisation systems play a key role in Quillen model structures [42], which comprise two intertwined weak factorisation systems on a category; but they also arise elsewhere, for example in the categorical semantics of intensional type theory [4, 20].”
The simplicial model of Univalent Foundations (after Voevodsky) (2012, unknown): “Earlier work on homotopy-theoretic models of type theory can be found in [HS98], [AW09], [War11].”
Isomorphism is equality (2013, background): “4) can be seen as a type-theoretic variant of Bourbaki’s notion of structure (1957), using type-theoretic function spaces instead of power sets.”
Structuralism, Invariance, and Univalence (2014, background): “Specifically, the discovery of an interpretation of Martin-Löf’s constructive type theory into abstract homotopy theory [3] suggests a new approach to the foundations of mathematics, one with both intrinsic geometric content and a computational implementation [5].”
Intuitionistic Type Theory (2016, background): “or in sequential form (1) J1 axiom (2) J2 axiom (3) J3 by rule r1 from (1) and (2) (4) J4 axiom (5) J5 by rule r2 from (4) (6) J6 axiom (7) J7 by rule r3 from(5) and (6) (8) J8 by rule r4 from (3) and (7) The latter form is common in mathematical arguments.”
Univalent categories and the Rezk completion (2013, background): “The distinctive feature of univalent foundations (UF) is its treatment of equality inspired by homotopy-theoretic semantics (Arndt and Kapulkin 2011; Awodey and Warren 2009; van den Berg and Garner 2012; Warren 2008).”
The Frobenius condition, right properness, and uniform fibrations (2015, methodology): “ral weak factorization systems in simplicial and cubical sets that have uniform Kan ﬁbrations as the right maps, which are of interest for the interpretation of Martin-Lo¨f’s rules for identity types [2, 15, 34, 4, 30]. These natural weak factorization systems are obtained using Garner’s small objec”