Homotopical inverse diagrams in categories with attributes

Abstract

We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I$ of homotopical diagrams of shape $I$ in $C$ and Reedy types over these; and we show how various logical structure ($\Pi$-types, identity types, and so on) lifts from $C$ to $C^I$. This may be seen as providing a general class of diagram models of type theory. In a companion paper "The homotopy theory of type theories" (arXiv:1610.00037), we apply the present results to construct semi-model structures on categories of contextual categories.

arXiv commentv3: various minor revisions for publication version; no change in theorem numbering

References in corpus (14)

• The identity type weak factorisation system
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Types are weak omega-groupoids
• The local universes model: an overlooked coherence construction for dependent type theories
• Cofibrations in Homotopy Theory
• Univalence for inverse diagrams and homotopy canonicity
• Two-dimensional models of type theory
• On the strength of dependent products in the type theory of Martin-Löf
• Homotopy limits in type theory
• The homotopy theory of type theories
• Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
• Two Models for the Homotopy Theory of Cocomplete Homotopy Theories
• First-Order Logic with Isomorphism
• Categories with families and first-order logic with dependent sorts

Cited by in corpus (2)

• Comparing semantic frameworks for dependently-sorted algebraic theories
• Displayed Type Theory and Semi-Simplicial Types