Homotopical inverse diagrams in categories with attributes

TL;DR

This paper develops a framework for homotopical inverse diagrams within categories with attributes, enabling the construction of diagram models of type theory with lifted logical structures.

Contribution

It introduces a method to build categories of homotopical diagrams and lift logical structures, broadening the modeling of type theories.

Findings

Constructed categories of homotopical diagrams of shape I in C

Lifted logical structures such as Pi-types and identity types

Provided groundwork for diagram models of type theory

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.