Homotopical inverse diagrams in categories with attributes

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 (Π-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.