Homotopical inverse diagrams in categories with attributes (Q2207273)

The present article deals with categories with attributes (CwA). This is one of several categorical formalisms that allow an algebraic treatment of type theories. They constitute a formalism suitable for the treatment of dependent types. CwA's come along with extra structure that is intended to capture the extensions of contexts, so that for a context of variables \(\Gamma\) and a type \(A\) in context \(\Gamma\) one can form the context \(\Gamma . A\) allowing for fresh variables of type \(A\) to occur. In particular a CwA \(\mathcal{C}\) is a category with terminal object (corresponding to the empty context) equipped with a presheaf \(Ty \colon \mathcal{C} ^{op} \to \mathrm{Set}\) (types of context \(\Gamma \in \mathcal{C}\)) and an assignment, for each type \(A\in Ty(\Gamma),\) of an object \(\Gamma . A \in \mathcal{C} \) and a projection map \( \Gamma . A \to \Gamma\) so that, for a change of contexts \(\Gamma \to \Delta ,\) an obvious square becomes a pullback. The authors examine the behaviour of such structures under the formation of the category of diagrams \(\mathcal{C} ^\mathcal{I}\) for inverse categories \(\mathcal{I}.\) The latter are categories with the feature that, in the dual category, the relation induced by the existence of a non-identity arrow between two objects, is a well-founded ordering and each object has finitely-many predecessors with respect to it. The category of diagrams is then equipped with a structure of a CwA (this is the content of section 3 of the article). Some natural questions arise in this framework. First, if the CwA \(\mathcal{C}\) carries identity, or \(\Sigma\)- or \(\Pi\)-types, does also \(\mathcal{C} ^\mathcal{I}\) do the same? The authors answer affirmatively this question (the answer is section 4 of the article). Secondly, when \(\mathcal{C}\) and \(\mathcal{I}\) have a homotopical structure (meaning here that they both have a distinguished class \(\mathcal{W}\) of morphisms called equivalences, containing the identities and closed under \(2\) out of \(6\)) do homotopical diagrams (those that take equivalences to equivalences) carry a CwA structure? The authors show that they form a sub-CwA of that of ordinary diagrams (section 5). Moreover it carries identity, \(\Sigma\)- and unit types if \(\mathcal{C}\) does do, while it carries \(\Pi\)-types if \(\mathcal{C}\) does so and all maps in \(\mathcal{I}\) are equivalences (Proposition 5.14). Finally, they give conditions on a functor \(\mathcal{J} \to \mathcal{I}\) so that the induced \(\mathcal{C} ^\mathcal{I} \to \mathcal{C} ^\mathcal{J}\) to be a local fibration or local equivalence in the sense of [\textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, Adv. Math. 337, 1--38 (2018; Zbl 1397.18015)]. In particular they show that for a CwA \(\mathcal{C},\) an ordered homotopical discrete opfibration \(\mathcal{J} \to \mathcal{J}\) induces contravariantly a local fibration between the respective diagram categories when it is moreover injective, while it induces a local equivalence when it is a homotopical equivalence.