We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Natural models of homotopy type theory.
- Authors
AWODEY, STEVE
- Abstract
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id, as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.
- Subjects
HOMOTOPY theory; PRESHEAVES; TYPE theory; FACTORIZATION; COMPUTATIONAL mathematics
- Publication
Mathematical Structures in Computer Science, 2018, Vol 28, Issue 2, p241
- ISSN
0960-1295
- Publication type
Article
- DOI
10.1017/S0960129516000268