{'fraction_non_alphanumeric': 0.04940025008876608, 'fraction_numerical': 0.007826852123438874, 'mean_word_length': 3.842852870813397, 'pattern_counts': {'":': 1, '<': 15, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Homotopical inverse diagrams in categories with attributes

We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes (CwA's). 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 the original CwA to the diagram CwA. This may be seen as providing a general class of diagram models of type theory, and forms a companion paper to arXiv:1610.00037,"The homotopy theory of type theories", which applies the present results in constructing semi-model structures on categories of contextual categories.


Introduction
Diagram models are a well-established tool in both categorical logic and homotopical algebra. For semantics of type theory (particularly intensional and homotopical type theory), however, diagram models are comparatively under-developed (with the exception of presheaf models). The complication is that logical constructors in this setting are typically not strictly functorial, making it harder to lift them to diagram models.
Specific cases, however, such as spans [Ton13], spreads [ML10], and the various categories considered in [KL16,§5], have shown that at least on certain domain categories, diagram models for intensional type theory should be viable.
Homotopy theory provides a well-established setup to deal with such non-functorial constructions and unify these special cases: the language of Reedy diagrams on inverse categories.
The first main contribution of the present paper is constructing Reedy diagram models on inverse categories in categories with attributes (CwA's), an algebraic formulation of type theories, and showing that these inherit various logical constructors from the original CwA. Specifically, we show: Theorem. Let C be a category with attributes, and I an inverse category. 1 Then the diagram category C I , together with the presheaf of Reedy types over I in C, is again a Date: August 8, 2018. 1 In fact the diagram model will depend on some extra structure on I -certain orderings -but every inverse category admits such structure. category with attributes. If in addition C carries identity, Σ-, unit-, or Π-types, possibly with functional extensionality, then so does C I .
Further mileage can be obtained by restricting to homotopical diagrams, another tool borrowed from homotopy theory.
Specifically, given a category with a class of morphisms distinguished as "equivalences", a diagram on it is homotopical if it sends these equivalences to equivalences in the typetheoretic sense. We show: Theorem. Let C be a CwA with identity types, and I an inverse category equipped with a class of equivalences. Then the homotopical diagrams and Reedy types forms a sub-CwA C I of the non-homotopical diagram CwA C I • . If in addition C carries Σ-types or unittypes, then C I is closed under these in C I • ; and similarly for Π-types with functional extensionality, provided all maps in I are equivalences.
Constructions along these lines are familiar from abstract homotopy theory, presented in terms of fibration categories [Bro73,RB09,Szu14] or comparable settings. An application of such constructions to type theory has previously been given by Shulman [Shu15], using type-theoretic fibration categories; see Remark 7. 3(3) for comparison with the present work.
This paper originated as a spin-off of another paper of ours [KL16], developing a left semi-model structure on the category of contextual categories. Section 5 of that paper requires four specific diagram models, which we originally planned to give individually as they appeared. However, the details became sufficiently lengthy and repetitive to write out (and to read!) that it seemed more worthwhile to break them out into a separate paper, and give the construction in generality.
We therefore make use in the present paper of results from Sections 1-4 of [KL16], while Sections 5-6 in that paper make use of the constructions presented here.
Organization. We begin in Section 2 by setting up some general background material on categories with attributes and logical structure on them. There are no substantively novel ideas, but some aspects of the presentation are new -for instance, the systematic development of elimination structures.
In Section 3, we introduce inverse categories, and set up the CwA's of Reedy types, along with an auxiliary infrastructure of Reedy limits, for constructing matching objects and the like. Having done this, we show in Section 4 how logical structure on the base CwA C (identity types, Π-types, and so on) induces similar structure on the diagram CwA's C I . Along the way, we also characterise elimination structures and equivalences in C I .
In Section 5, we consider the restriction to CwA's of homotopical diagrams, and show when the logical structure restricts from plain to homotopical diagram CwA's. Lastly, in Section 6, we give conditions on a functor u : J I for the induced map C I C J to be a local fibration or local equivalence in the sense of [KL16,§4].
We conclude in Section 7 by summarising the main constructions of the earlier sections for quick reference, briefly surveying the connections with related work, and noting various possible generalisations that we have not covered in this paper.

Type-theoretic background
We recall in this section some background on categories with attributes, and logical structure on them. Most of the material is standard, but some aspects of the presentation -for instance, the systematic use of elimination structures -are novel.

Categories with Attributes.
Definition 2.1. A category with attributes (CwA) C consists of: (1) a category C, with a chosen terminal object 1; 2 (2) a functor Ty : C op Set; (3) an assignment to each A ∈ Ty(Γ), an object Γ.A ∈ C (the extension of Γ by A) and a map p A : Γ.A Γ (which we distinguish graphically as ); (4) for each A ∈ Ty(Γ) and f : ∆ Γ, a map f.A : ∆.f * A Γ.A such that the following square is a pullback: As defined, categories with attributes are models for an evident essentially algebraic theory. A map of categories with attributes is a homomorphism of such models: explicitly, a functor F : C C ′ and transformation F Ty : Ty C Ty C ′ · F , strictly preserving all the structure (chosen terminal object, context extension, and so on). Write CwA for the category of categories with attributes. 3 Definition 2.2. A comprehension category consists of a category C together with a Grothendieck fibration p : T C and functor χ : T C → , such that cod · χ = p, and sending p-cartesian arrows to pullback squares.
It is easy to see that CwA's correspond to discrete comprehension categories (i.e., ones in which the fibration p is discrete), via the correspondence between presheaves and discrete fibrations. 4 Elements of the sets Ty(Γ) in a CwA, or of the fibers T Γ in a comprehension category, will be called types over Γ. It is often also useful to consider more general context extensions: Definition 2.3. A context extension A of an object Γ of a CwA C is a sequence (A 1 , . . . , A n ), where A i ∈ Ty(Γ.A 1 . . . . .A i−1 ).
We will often write just extensions, when this is not ambiguous. Context extensions form an evident presheaf Ty * over C, and indeed an alternative CwA structure on C [Lum10, 1.3.1], with p A given by the composite p A 1 p A 2 . . . p An : Γ. A Γ. We distinguish maps of the form p A diagrammatically as .
Remark 2.9. The context extension argument ∆ in the "eliminator" operations above is usually omitted. In the presence of Π-type structure, it is redundant, since these general eliminators can be constructed from the special case where ∆ is empty. When considering the logical constructors individually, though, the more general form seems desirable, as noted in [GG08] for the case of identity types. For disambiguation, these could be called Frobenius Id-type structure, and so on, since as noted in [vdBG11], the argument ∆ corresponds to a categorical Frobenius condition.
Except for this difference, the present definitions are unchanged from [KL12, App. A, B], which in turn are direct algebraic translations of the original rules of [ML84].

Elimination structures.
It is often profitable to encapsulate type-theoretic induction principles in the notion of an elimination structure, defined in [Lum10]. We work for this subsection in a fixed ambient CwA C.
. A pre-elimination structure e on a map j : ∆ ′ ∆ is an operation providing, for each type C ∈ Ty(∆) and map d : ∆ ′ ∆.C over ∆, a section e C,d of C such that e C,d j = d.
A Frobenius pre-elimination structure on j : ∆ ′ ∆ is a family of pre-elimination structures e E on j. E : ∆ ′ .j * E ∆. E, for each context extension E of ∆. (We impose no compatibility condition between these elimination structures.) Given context extensions A, B of a common base Γ, a stable Frobenius elimination structure on a map j : Γ. A Γ. B over Γ is: • a family of Frobenius pre-elimination structures e f on f * j : • commuting with reindexing, in that given any g : Γ ′′ Γ ′ , f : Γ ′ Γ, C ∈ Ty(Γ ′ .f * B), and suitable inputs E, C, d for e f , we have g * e f E,C,d = e f g g * E,g * C,g * d .
By an elimination structure, we mean in the present paper a stable Frobenius elimination structure.
Proposition 2.11. Suppose j : Γ. A Γ. B is equipped with an elimination structure e over Γ. Then for any f : Γ ′ Γ, the pullback f * j : Γ ′ .f * A Γ ′ .f * B carries an elimination structure f * e; and this operation is functorial in f . Similarly, any context extension j. E of j carries an elimination structure e. E; and this commutes with the preceding operation, i.e. f * (e. E) = f * e.f * E. Definition 2.12. Suppose C is equipped with (Frobenius) Id-type structure. Then for any A ∈ Ty(Γ), the map r A : Γ.A Γ.A.p * A.Id A carries an elimination structure, which we call the canonical such structure, induced by the elimination operation and computation axiom of the Id-type structure. Moreover, this is stable under reindexing in Γ, and functorial in C.
Similarly, if C is equipped with (Frobenius) Σ-type structure, then for all suitable Γ, A, B, the pairing map pair A,B : Γ.A.B Γ.Σ A B carries a canonical elimination structure, stably in Γ and functorially in C.
For inductive types/families with multiple constructors, e.g., binary sums, one could generalise the definitions above to elimination structures not only on single maps but on families of maps; but we do not treat such type-formers in the present work.
Elimination structures are a type-theoretic analogue of left lifting properties, and are frequently used as such: Proposition 2.13. Let e : Γ. A Γ. B be equipped with an elimination structure over Γ, and suppose k : Γ. B ∆ and h : Γ. A ∆.C form a commutative square from e to π C . Then there is an induced diagonal filler j, making both triangles commute: Moreover, this construction commutes with pullback in the base.
Proof. Apply the elimination structure to the induced map Γ. A Γ. B.k * C.
Under that analogy, the following propositions are familiar from the theory of weak factorisation systems, and their proofs adapt directly. (2) For any C ∈ Ty(Γ. A), there is a type e C ∈ Ty(Γ. B) such that e * (e C) = C; we call e C the descent of C along e.
Moreover, both these constructions are stable in the base Γ, and functorial in C.
Proof. The elimination structure, applied to (e, id) : Γ. A Γ. B.π B A, gives a section of π * B A, whose composite with π B . A yields the desired retraction r.
Now, given C ∈ Ty(Γ. A, take e C to be r * C. Id A is given by induction on the length of A. When A is empty, so is Id A , and r A is the identity map. When A = ( A <n , A n ), then assuming that we have constructed Id A<n , r A<n , and its elimination structure, we take Id A to be (Id A<n , (Id A ) n ), where the type (Id A ) n is given as a descent of Id An as in the following diagram: Then r A is the composite the upper edge of the diagram; that is, of r An , a context extension of r A<n , and an isomorphism, and so as such, carries an elimination structure. We note for future use that r A is always a composite of context extensions of the individual reflexivity maps r A i and isomorphisms.
Similarly, the Π-type structure can be lifted to (C, Ty * ) via the following construction. (Although this construction is well-known in practice, we are unaware of it being documented in the literature.) Construction 2.18. If a CwA C carries Π-type structure, then so does (C, Ty * ), functorially in C.
Let A = A 1 . · · · .A n be an extension of Γ ∈ C, and B = B 1 . · · · .B m a further extension of Γ. The construction of the λ operation is straightforward along similar lines, by induction again on the length of B.
We will generally consider both identity contexts and iterated Π-types not from the point of view of (C, Ty * ) as a CwA in its own right, but as auxiliary operations for working in C. A similar construction is possible for Σ-types, but we do not recall it here as we will not require it.
2.4. Equivalences. We recall here the well-known definition of equivalences of types or contexts, along with a generalisation from [KL16] to arbitrary maps in CwA's, and some key facts about these notions.
Work for the remainder of this subsection in a fixed ambient CwA C equipped with Id-types.
B be a map between context extensions over some where Id B is the iterated identity type as constructed above), such that p Id B h = (f, g). We write f ∼ g to mean that some such h exists.
Definition 2.20. Let A, B be context extensions of some base Γ ∈ C. A map f : Γ. A Γ. B over Γ is an equivalence over Γ if there exist maps g, g ′ : Γ. B Γ. A and homotopies η : f g ∼ id Γ. B and ε : g ′ f ∼ id Γ. A over Γ. Equivalence data for f consists of some choice of such g, η, g ′ , ε.
This approach works only within "fibrant slices" of a CwA, since iterated identity types are available just for context extensions, not for arbitrary objects. In Section 5, we will need a more general notion: . A map f : Γ ′ Γ in C is an equivalence if it satisfies the following properties: (1) weak type lifting: given any context extension A of Γ and type B ∈ Ty(Γ ′ .f * A), there exists some type B ′ ∈ Ty(Γ ′ .f * A) and equivalence w : From the point of view of f , these might be more naturally called descent properties; they are lifting when viewed as properties of the induced functor f * : C(Γ) C(Γ ′ ) (cf. Definition 6.1 below).
We recall without proof some key facts about these notions: all stable under pullback in the base. We say a Π η -type structure is extensional if it is additionally equipped with function extensionality structure, and write Π ext -structure to refer to the combined structure.
For the remainder of this subsection, fix a CwA C equipped with Id-and Π-type structure. The following alternative form of function extensionality is less type-theoretically economical, but more categorically succinct: It is straightforward to check that just like Id-and Π-types, extensionality also lifts to context extensions, and hence to general homotopies: Lemma 2.28. Suppose C is equipped with Π-types, Id-types, and function extensionality structure. Then (C, Ty * ) carries functional extensionality structure, for the Π-type structure and Id-type structure given above.
In particular, given two sections b, b ′ of a context extension B ∈ Ty * (Γ. A), and a homotopy h : b ∼ b ′ between them over A, there is an induced homotopy between their abstractions Moreover, these constructions are functorial in C.
As a corollary, we derive the covariant action of iterated Π-types on equivalences between their codomains (though without making its functoriality precise, as we do not need it):

Inverse diagrams and Reedy types
In this section, we recall the definition of inverse categories, and define Reedy types over diagrams on inverse categories valued in a CwA. These are analogous to Reedy fibrations, a well developed tool from the homotopy theory of (co-)fibration categories [RB09,Szu14] and similar settings.
Compared to such settings, Reedy types in CwA's incur several extra complications. Due to these, we split the definition into two stages. We first define weak Reedy types, which are unsatisfactorily flabby, but suffice for setting up the machinery of Reedy limits. Armed with these we can then define (strict) Reedy types, which are what we really want.
3.1. Inverse categories and weak Reedy types. Definition 3.1. Let I be a category. The precedence ordering ≺ on Ob I is defined by taking i ≺ j just if there exists some non-identity arrow α : i j. An inverse category I is a category in which the precedence ordering is well-founded, and each object has finitely many predecessors. 5 For i ∈ I, we write yi ∈ Set I for the Yoneda co-presheaf I(i, −), and ∂i ⊆ yi for the sub-co-presheaf of non-identity maps out of i. Example 3.2. A useful running example throughout this paper is the "walking span": the posetal inverse category (0 01 1), which we denote Span.
Definition 3.3. Given an inverse category I, a category C, diagrams F ∈ Set I , D ∈ C I , and an object C ∈ C, an F -cone λ from C to D consists of maps λ x : C D(i) for each i ∈ I and x ∈ F (i), such that D(α)λ x = λ αx for each α : i j, x ∈ F (i). We denote such cones by λ : C F D. They are easily seen to be functorial in all parameters: contravariantly in C, covariantly in D, contravariantly in F , covariantly 2functorial in C, and contravariantly 2-functorial in I. Definition 3.4. Let C, I be categories, and p : Y X a map in C I . Then for i ∈ I, a (relative) matching object for p at i is • an object M i p ∈ C equipped with a yi-cone λ : M i p λ X and a ∂i-cone µ : M i p µ Y , such that λ| ∂i = pµ, • that is moveover terminal among objects equipped with such a cone.
In classical presentations of Reedy fibrations, relative matching objects are not often explicitly defined, appearing instead as pullbacks of absolute matching objects: In our setting of CwA's, however, these absolute matching objects may often fail to exist; so we define the relative ones directly.
Relative matching objects may also be seen as limits indexed over the oplax pushout category Proposition 3.5. Let u : J I be a discrete opfibration of inverse categories. Then for any category C, the precomposition functor u * : C I C J preserves relative matching objects.
Proof. Since u is a discrete opfibration, its induced maps (j ↓ u) on co-slices and ∂(j ↓ u) on strict co-slices are isomorphisms; so the required limit property of matching objects is unchanged by u * .
Before defining the "Reedy types" that we actually want, we need to start with a more general "weak" notion, from which we will afterwards carve out the "strict" ones.
Fix, for the next few definitions, a CwA C and an inverse category I. We will define the fibration of weak Reedy I-types in C over the diagram category C I (or just weak Reedy types, when I and C are clear).
Definition 3.6. A weak Reedy I-type over a base X ∈ C I consists of: • an object Y and map p : Y X in C I , together with • chosen matching objects M i p for p, for each i ∈ I, and • for each i ∈ I, a type A i ∈ Ty(M i p), and an isomorphism ϕ i : , over a map f : X ′ X in C I , consists of: Write T wR(C,I) for the total category of weak Reedy I-types in C (or just T wR when C, I are implicit); this has an evident forgetful functor p to C I . Weak Reedy types are reasonably transparently an analogue of Reedy fibrations, as ordinarily defined in a fibration category or similar settings. However, in our setting they are a little unsatisfactorily flabby, due to the essentially redundant data of chosen matching objects: for instance, in the case I = 1, a weak Reedy type corresponds to "a map in C isomorphic to a dependent projection".
For these reasons, we will rein in the redundancy by cutting down to strict Reedy types, whose matching objects are constructed canonically rather than forming extra data. These matching objects are also needed to show that weak Reedy types form a comprehension category; for now we note as much of that as is obvious.
, forgetting the given matching objects and types.
We write C I wR to denote this whole triangle of data, considered as a comprehension category minus the existence and preservation of cartesian lifts.
Moreover a discrete opfibration u : J I induces a functor u * : T wR(C,I) T wR(C,J ) (by Proposition 3.5), and a CwA map F : C D induces a partial functor F I : T wR(C,I) T wR(D,I) , defined just on types whose matching objects are preserved by F .
In Proposition 3.21 below we will fill in the gaps: we will show that T wR(C,I) has and χ preserves cartesian lifts, and that arbitrary CwA maps preserve the required matching objects; so C I wR forms a comprehension category, bifunctorially in C and I.

Reedy limits.
It is familiar from homotopy theory that one does not really need general finite completeness to work with Reedy diagrams, since the limits used-matching objects of Reedy fibrant diagrams, and related constructions-can always be constructed from just pullbacks of fibrations. Analogously, in our setting, matching objects and other limits we use can be constructed as context extensions, using just pullbacks of types.
Here we set up machinery for constructing and manipulating these limits rather precisely, since we often care about strict preservation of types/context extensions under reindexing and CwA maps.
Fix, for this subsection, an inverse category I.
Definition 3.8. Let i : F G be a map in Set I , p : Y X a map in C I (for some category C); suppose moreover we are given C ∈ C, and a G-cone λ : When enough limits exist, this universal property says just that (A, q, γ) is a pullback of i⋔ p along (µ, λ), where i⋔ p is the Leibniz cotensor of i with p: Relative matching objects are a special case, with F = 0, G = δi, and C = X i .
To construct such relative pullbacks, we will assume additional structure on i : F G.
Definition 3.10. A finite extension in Set I is a monomorphism i : F G, together with a linear ordering on its total complement i G i \ F i , such that: • the total complement is finite, and • for any α : A map of finite extensions is a pushout square between them that preserves the given orders on the total complements.
Equivalently, a finite extension is a map exhibited as a finite cell complex of the boundary inclusions ∂i yi. The orderings given in finite extensions are exactly the extra data needed to construct relative pullbacks of Reedy types. Lemma 3.11 (Master lemma for Reedy limits). Suppose we are given a finite extension i : F G in Set I , a weak Reedy type A over Γ in C I , an object ∆ ∈ C, a G-cone λ : ∆ G Γ, and an F -cone µ : together with π (λ,µ) * A and (λ, µ).A forms an i-relative pullback of π A along (λ, µ): F . In this case, λ| yi and µ| ∂i induce a map m : ∆ M i A. We take (λ, µ) * A to be the pullback of A i along m, and (λ, µ).A to be the (F G is given as a composite of single-step extensions: Then we define by induction a sequence of objects ∆ k ∈ C, along with G-cones λ k : ∆ k G Γ and F k -cones µ k : ∆ k Γ.A over λ k , for k = 0, . . . , n, as follows: Now we take (λ, µ) * A to be the resulting context extension ∆ n ∆, and (λ, µ).A to be µ n .
By Reedy limits, we will mean the objects and cones constructed according to the preceding lemma. (1) Functoriality in ∆: Given F G, Γ, A, ∆, λ, µ as above, and a map f : ∆ ′ ∆, (2) Functoriality in Γ, A: Given data as above together with Proof. The functoriality statements are routine to verify, immediate in the single-step case and extending by induction to the general case. The preservation statement comes in the single-step case from the fact that CwA maps preserve canonical pullbacks of types, and again extends to the general case straightforwardly by induction.
Reedy limits are moreover functorial in the inverse category I, but the statement of this functoriality is slightly less straightforward.
For a functor F : C D, write F ! and F * for its pushforward/restriction functors: . Given a discrete opfibration u : J I, we have u ! (∂j yj) ∼ = (∂uj yuj) for each j ∈ J . More generally, u ! sends finite extensions in Set J to finite extensions in Set I .
Proof. Since u is a discrete opfibration, u ! can be computed by u ! (F )(i) = j∈J i F (j). The desired isomorphism is immediate. As a left adjoint, u ! also preserves pushouts, so the action on finite extensions follows, viewing them as cell complexes of the boundary inclusions.
Lemma 3.14. For any category C, object X in C, diagram Y : I C, and co-presheaf Lemma 3.15 (Functoriality of Reedy limits in the domain). Suppose given a discrete opfibration of inverse categories u : J I, along with Γ ∈ C I , a weak Reedy I-type A over Γ, a finite extension F G in Set I , an object ∆ ∈ C, and cones λ : correspond in the sense of the preceding lemma.
Proof. Direct from the construction of (λ, µ) * A, together with the action of u ! on finite extensions. Then we obtain a context extension (λ, µ) * A ∈ Ty * ∆ (with length mn, where m is the length of A and n the length of i : F G), along with (λ, µ).A : ∆.(λ, µ) * A G Γ.A, forming an i-relative pullback of π A along (λ, µ) as in the master lemma.
Moreover, this construction enjoys all the functoriality properties of Lemmas 3.12 and 3.15.
Proof. Built from Reedy limits given by the master lemma, just like the generalisation there from a single-step finite extension to the multi-step case.
3.3. Strict Reedy types. Each weak Reedy type comes supplied, by definition, with matching objects. However, given a little extra data on the domain category I, the master lemma provides us with canonical matching objects, as context extensions of the objects in the base.
Definition 3.17. By an ordered inverse category we mean an inverse category I with equipped with, for each i, a total order on the set of morphisms out of i extending the precedence ordering of i/I, i.e. such that for any composable f, g, with f non-identity, we have f g < g.
A discrete fibration u : J I between ordered inverse categories is ordered if it respects the given orderings.
Choosing such structure on an inverse category I amounts precisely to giving each 0 yi the structure of a finite extension; or equivalently, each 0 ∂i, since the ordering on yi must have id i as its top element. This extra data is not burdensome to supply: Proposition 3.18. Any inverse category I admits some ordering.
Proof. Any finite partial order can be extended to a total order. Example 3.19. We will consider Span, the category (0 01 1), as ordered by 0 < 01 1. (The rest of the ordering is determined.) Definition 3.20. Once I is ordered, then given a weak Reedy type A = (Y, p, M, A, ϕ) over a diagram Γ ∈ C I , we can for any i ∈ I apply the master lemma with the finite extension 0 ∂i to construct a relative matching object for p A as observed in Remark 3.9: We call this the canonical matching object for A at i, and denote it (as a context extension) by A ∂i ∈ Ty * Γ i . It has a canonical isomorphism to the given matching objects of A, ψ i : Γ i .A ∂i ∼ = M i A. We write A yi for the further context extension A ∂i .ψ * A i ∈ Ty * Γ i (which may be constructed directly as a Reedy limit along the finite extension 0 yi). More generally, for a context extension A of weak Reedy types over a diagram Γ, we write A ∂i and A yi for the corresponding Reedy limits supplied by Lemma 3.16, and M i A for the resulting matching objects Γ i . A ∂i .
Correspondingly, for a map f : We can now tie up the dangling thread from above: Proof. Fix some ordering on I. As noted in Proposition 3.21, we just need to give cartesian lifts, and show they are sent to pullbacks by comprehension. For construction of the lifts, suppose f : Γ ′ Γ is a map in C I , and A = (Y, p, M i , A, ϕ) a weak Reedy type over Γ. We construct f * A, along with the map f.A : f * A A over f , by induction on i ∈ I (under the precedence ordering). Suppose f * A and f.A have been constructed in all levels j < i. Then this suffices to construct a matching object M i (f * A) as a Reedy limit (using the given ordering on I), and also the induced map

Cartesianness of this lift is immediate.
To see that the comprehension of f.A is a pullback in C I , we show by induction that it is a levelwise pullback. Its i-th component is as in the diagram above. The upper square is a pullback by construction, while the lower is a pullback by the universal property of matching objects together with the assumption that it χ(f.A) j is a pullback for all j < i. Functoriality in I was already noted in Proposition 3.7. For functoriality in C, note again that matching objects of a weak Reedy type are up to isomorphism Reedy limits, and so preserved by the action of CwA maps. Definition 3.22. A (strict) Reedy type over Γ is a weak Reedy type A = (Y, p, M, A, ϕ) over Γ such that for each i ∈ I, • the given matching objects M i p are precisely the matching objects Γ i .A ∂i supplied by the master lemma (including their associated cones); Write T R(C,I) (or just T R ) for the full subcategory of T wR(C,I) on strict Reedy types. We will generally write just "Reedy types" to mean the strict ones, except when explicitly contrasting them with weak Reedy types. Proof. Parts not specifically noted here follow directly from earlier ones. (2) is straightforward by induction on levels, using the fact that Ty is a discrete fibration. For (4), note that when u : J I is ordered, the isomorphism u ! ∂j ∼ = ∂uj is a map of finite extensions; naturality of Reedy limits (Lemma 3.12(3)) then implies that the canonical matching objects are preserved by u * . (6) similarly uses naturality of Reedy limits under CwA maps (Lemma 3.12(5)).
These observations justify the following definition: Definition 3.24. We write just C I for the CwA of strict Reedy types, with base category C I and presheaf Ty corresponding to the discrete fibration T R(C,I) . (Occasionally for emphasis or disambiguation we may write C I R or Ty R .) This construction is covariantly functorial in CwA maps, and contravariantly in ordered discrete opfibrations.
When we speak of types over diagrams Γ ∈ C I , we will always mean strict Reedy types unless specified otherwise, and similary for context extensions, etc. Remark 3.26. We will often construct strict Reedy types and maps between them by induction, as with the reindexings in Proposition 3.21. Such constructions often involve applying lemmas about Reedy types to the type under construction, before it is fully defined.
For instance, suppose one has earlier proved a lemma that "Reedy limits of levelwise nice Reedy types are nice", and is now constructing by induction a levelwise nice Reedy type A.
In the induction step, one must construct A i and prove it nice, assuming that A j is given and nice in all levels j < i. Then, in the proof of niceness of A i , one may invoke the lemma to conclude that M i A is nice.
Formally, this may be justified by noting that the data given constitute a levelwise nice Reedy type over the subcategory I <i (or the strict slice ∂(i ↓ I)), and that M i A can be computed as a Reedy limit of this type, to which the lemma then applies.
For the sake of readability, we will generally avoid belabouring such points.
3.4. Levelwise extensions. Besides Reedy types, we will in places make use of levelwise context extensions of diagrams.
Definition 3.27. Let I be an arbitrary category, and Γ ∈ C I a diagram. A levelwise extension A over Γ is a family of context extensions A i ∈ Ty * (Γ i ), for each i ∈ I, along with maps in C making the objects Γ i .A i and their projection maps into a diagram over Γ (which we denote Γ. A).
Write the set of levelwise extensions over Γ as Ty lw (Γ); these constitute an evident CwA structure on the category C I , which we write as C I lw . Moreover, the construction of C I is bifunctorial in CwA maps C D and arbitrary functors J I. In case I is an ordered inverse category, there is an evident natural map from Reedy types to levelwise extensions, commuting with the context extension operation; that is, a strict CwA map C I C I lw , acting as the identity as on the base category. The CwA C I lw is in general of less intrinsic interest than C I , since it will not typically inherit as much logical structure from C. However, levelwise extensions appear naturally as intermediate stages in several constructions/proofs on Reedy types.
In diagrams, we denote projections from levelwise extensions by Γ. A lw Γ.

Logical structure on inverse diagrams
The goal of this section is to show that if C carries Id-types (resp. Σ, unit, Π, funext), then so does C I , for any ordered inverse category I.
As the statement suggests, each piece of logical structure lifts from C to C I individually (except of course for functional extensionality, which relies on Id and Π); we will tackle them one at a time in the propositions of this section. In the course of this, we will also require a few technical lemmas on the interaction of Reedy limits with elimination structures and equivalences.
Fix the CwA C and ordered inverse category I throughout. When we say that constructions are functorial in C and I, we mean with respect to CwA maps C D preserving whatever logical structure is under consideration, and ordered discrete opfibrations J I.

Elimination structures in inverse diagrams.
Lemma 4.1. Suppose f : Γ. A Γ. B is a map over Γ in C I equipped with a levelwise elimination structure, i.e. an elimination structure on each f i over Γ i . Then f carries an elimination structure over Γ in C I . Moreover, this is stable under pullback in Γ, and functorial in C and I.
Proof. First we give the pre-elimination structure. Suppose we have a type C over Γ. B, and map d : Γ. A Γ. B.C over Γ. B. We wish to construct a section e of C such that ef = d.
Work by Reedy induction: suppose that e has already been constructed in degrees below i, satisfying the desired equations. Then these components assemble to give a section e ′ of M i C (Γ. B) i , forming a commutative square from f i to p C i ; we take e i as the diagonal filler for this square supplied by the elimination structure of f i : Next, for the Frobenius condition, note that the components of any pullback f. C of f along a context extension π C : Γ. B. C Γ. B are just pullbacks of the components of f along the context extensions C yi . So any such pullback f. C again carries a levelwise elimination structure, and hence a pre-elimination structure by the previous paragraph.
Finally, note that the above constructions are all stable under pullback in Γ, so they assemble to produce an elimination structure stably in Γ, as required; and similarly, are functorial in C and I.
So levelwise elimination structures suffice to give elimination structures in C I . However, for some purposes one needs a slightly stronger notion.    Specifically, in the case of a single-step extension F F + h yi, (λ, µ) * f is a genuine pullback of m i f along the map ∆ M i A induced by (λ| yi , µ| ∂i ) and, as such, carries an induced elimination structure by stability.
In the case of a multi-step extension F G, write it as a composite of single-step extensions F = F 0 F 1 · · · F n = G. Then, similarly to in the proof of the master lemma, we form a tower: Each of the comparison maps g k carries an elimination structure by the single-step case, so by induction up the tower using the Frobenius property and composition of elimination structures, each composite h k g k carries an elimination structure; but the final such map h n g n is isomorphic over ∆ to our desired map (λ, µ) * f . For the levelwise elimination structure, note that f i is canonically isomorphic to the Reedy limit f yi : M i A. A yi M i B. B yi , which carries an elimination structure by the first statement.
Finally, as ever, all constructions used are stable in Γ, and functorial in C and I.
Combining the preceding two lemmas gives:

4.2.
Unit types in inverse diagrams. We begin the logical structure with the lowesthanging fruit.
Proposition 4.6. Suppose C is equipped with unit-type structure. Then so is C I .
Moreover, this construction is functorial in C (with respect to CwA maps preserving unit types) and in I.

Proof.
Given Γ ∈ C I , define the unit Reedy type 1 Γ over it by induction, taking (1 Γ ) i to be 1 M i 1 Γ ∈ Ty(M i 1 Γ ). Similarly, take (⋆ Γ ) i to be ⋆ M i 1 Γ · (M i ⋆ Γ ). The ith comparison component of ⋆ Γ is then exactly ⋆ Γ i ; so the canonical elimination structures on these maps assemble to form a Reedy elimination structure, and hence by Corollary 4.5 an elimination structure in C I .
These constructions are all stable under reindexing, and so constitute unit-type structure on C I . Functoriality in C and I is routine to check, since all constructions involved (matching objects over I, and the unit-type structure on C applied at each level) were so functorial.

Identity types in inverse diagrams.
Proposition 4.7. Suppose C is equipped with Id-type structure. Then so is C I . Moreover, this construction is functorial in C and I Proof. Let Γ.A Γ be a type over a diagram in C I . We will construct, by the usual Reedy induction over i ∈ I, the type Id A ∈ Ty(Γ.A.A), together with a map Id A carries an elimination structure over Γ i . Now take (Id A ) i as the descent of Id A i along r ′ as given by Lemma 2.16, and (r A ) i to be the composite of r ′ .(Id A ) i with r A i : Now the new comparison component m i r is by construction r A i , so carries an elimination structure over M i A as required. This completes the inductive construction of Id A , r A , and the Reedy elimination structure on r A . Corollary 4.5 turns this into an elimination structure on r A in C I , and all these components are by construction stable under pullback in Γ; so together, they constitute Id-type structure on C I , as required. Functoriality in C and I is once again routine to check.

Equivalences in inverse diagrams.
With the identity types available, we are now able to speak of homotopies and equivalences in C I , and compare them with these notions in C. The first lemma is a direct analogue of Lemma 4.4 on Reedy limits of elimination structures.
We say w is a Reedy equivalence if m i w is an equivalence for all i; similarly, by Reedy equivalence data on w we mean a choice of equivalence data on each m i w. Lemma 4.9. Suppose w : Γ. A Γ. B is a Reedy equivalence (resp. equipped with Reedy equivalence data) over Γ in C I . Then: (1) for any finite extension F G, and any ∆, λ, µ as before, (λ, µ) * w is an equivalence (resp. carries induced equivalence data); (2) and w is a levelwise equivalence (resp. each w i carries equivalence data). Moreover, for the "data" version, these constructions are stable under pullback in the base, and functorial in C and I.

Proof. Entirely analogous to Lemma 4.4. When F
G is a single-step extension by ∂i yi, then (λ, µ) * w is a pullback of m i w along a map into the Γ i . In the multi-step case, (λ, µ) * w has a canonical decomposition as a composite of context extensions of such single-step pullbacks. Since equivalences (resp. equivalence data) are preserved by pullback in the base, pullback along context extensions, and composition, the Reedy limit statement follows.
The levelwise statement follows as a special case, since w i is isomorphic to w yi . Finally, stability/functoriality of the "data" version follows from stability/functoriality of all steps in the construction.

carries levelwise equivalence data) if and only if it is a Reedy equivalence (resp. carries Reedy equivalence data). Moreover, the maps between levelwise and Reedy equivalence data are stable under pullback in Γ, and functorial in C and I.
Proof. The "if" direction is just part (2) of the previous lemma.
For the converse, suppose w is a levelwise equivalence, and work by induction: assume we have shown m j w is an equivalence for each j < i. Then M i w is an equivalence, by part (1) of the previous lemma, applied to w| i/I in C i/I . But now w i = (M i w. B i ).(m i w), so by 2 out of 3, m i w is an equivalence as required.
Moreover, all the above reasoning extends directly to a construction on equivalence data, stably in the base and functorially in C, I.
To convert these into the desired levelwise homotopies, we need to construct maps For this, it suffices to give an elimination structure on each map or in other words, to show that (Id B ) yi is itself an alternative identity context for B. By We are now equipped to completely characterise the equivalences of C I within fibrant slices, and give a recognition condition for them in general. Lemma 4.12. A map f : Γ. A Γ. B over Γ is an equivalence (resp. carries equivalence data) in C I (Γ), and hence C I , if and only if it is a levelwise equivalence (resp. carries levelwise equivalence data). Moreover, these constructions on equivalence data are stable in Γ and functorial in C, I.

Proof.
First, suppose f is an equivalence in C I (Γ). Pick some homotopy section (g, α) and homotopy retraction (g ′ , β). By Lemma 4.11, these give levelwise homotopy sections and retractions of f ; so f is a levelwise equivalence.
Conversely, suppose f is a levelwise equivalence. Without loss of generality, we may assume f is a dependent projection Γ. A Γ. (For the general case, first factor f as an equivalence f ′ : Γ. A Γ. B. A ′ in C I (Γ) followed by a dependent projection π A ′ , according to [GG08,Lem. 11]. By the first direction of the present lemma, f ′ is a levelwise equivalence; so by 2 out of 3, so is π A ′ . So by the special case, π A ′ is an equivalence in C(Γ. B), hence in C(Γ); and by 2 out of 3, so is f .) For the case of a dependent projection, first recall that a type is contractible just if it is inhabited and a proposition [Uni13, Lemma 3. With this in mind, suppose π A : Γ.A Γ is a levelwise equivalence. By Lemma 4.10, it is then also a Reedy equivalence. But its comparison maps m i π A are exactly the projections π A i : (Γ.A) i M i A; so these are equivalences, and we may choose for each i sections s i of A i , and g i of Id A i . From these, we will construct a sections a of A and h of Id A , in C I . The former is direct by Reedy induction, taking each a i to be the composite Γ i For the latter, first take for each i a section of g ′ i of (Id A ) i as in the following diagram: where r ′ and the isomorphism are as in the construction of identity types (Proposition 4.7), and as noted there r ′ carries an elimination structure, which we apply to g i to yield g ′ i . Now we get the desired section h of Id A by Reedy induction, setting  Proof. First, for weak type lifting, suppose we are given A ∈ Ty(Γ). We will construct a type B over ∆, together with a Reedy equivalence e : Γ.A Γ.f * B over Γ). Once this is done, it follows by Lemmas 4.9 and 4.12 that e is an equivalence in C I , and so exhibits B as a weak lift of A as required.
To construct B and e, we work by induction. Suppose they have been constructed in degrees < i.
its comparison component at i is exactly w i ; so e is a Reedy equivalence in degree i as required.
For weak term lifting, the argument is similarly straightforward. The lifting term and homotopy are built by induction, using at each stage first transport along the homotopy in lower degrees, and then weak term lifting along a right-proper pullback of a component of f .
Summarising the two previous lemmas, we have: Lemma 4.14.
(1) A map f : Γ. A Γ. B over Γ is an equivalence (resp. carries equivalence data) in C I (Γ), and hence C I , if and only if it is a levelwise equivalence (resp. carries levelwise equivalence data). Moreover, these constructions on equivalence data are stable in Γ and functorial in C, I.
Remark 4.15. Note that the slightly careful phrasing above is necessary: in general, an equivalence f : Γ ∆ in C I may fail to be levelwise. For instance, consider the case where: • I is the arrow category (1 → 0); • C is constructed by freely adjoining a terminal object ⊥ to some non-trivial CwA, e.g. Set, and setting Ty(⊥) := 0; • e 0 : Γ 0 ∆ 0 is id ⊥ , and e 1 : Γ 1 ∆ 1 is any non-equivalence in Set: Then e is not a levelwise equivalence, by choice of e 1 ; but it is an equivalence in C → , since there are no Reedy types over Γ (as there are no types over ⊥), so both weak lifting properties hold vacuously.

Σ-types in inverse diagrams.
Proposition 4.16. Suppose C is equipped with Σ-type structure. Then so is C I . Moreover, this construction is functorial in C and I.
Proof. The construction is analogous to the one for identity types in Proposition 4.7. Let Γ.A.B Γ.A Γ be a pair of types over a diagram in C I . We will construct by Reedy induction the type Σ A B over Γ, along with its pairing morphism pair : Γ.A.B Γ.Σ A B and a Reedy elimination structure on pair over Γ.
As usual, we assume by induction that these are defined on I <i , and wish to define them at i. We will construct (Σ A B) i as a Σ-type of a pair of typesĀ i ,B i over M i Σ A B.
By the inductive Reedy elimination structure of pair, and Lemma 4.4, we know that carries an elimination structure; so we can takeĀ i ,B i to be the descent of A i , B i along M i pair, according to Lemma 2.16. We then set (Σ A B) i := ΣĀ iB i , and take pair i to be the composite of the top edge of the following diagram: Proposition 4.17. Suppose C carries Π-type (resp. Π η -) structure. Then so does C I . Moreover, this construction is functorial in C and I. equivalence data, and every step was stable in the base Γ and functorial in C and I; so we are done.
Summarising the results of this section, we have: Proposition 4.20. Let C be a CwA, and I an ordered inverse category. If C carries Id-, Σ-, unit, Π-, Π η , or Π ext -types, then so does C I . Moreover, all this logical structure is preserved by the functorial action under ordered discrete opfibrations in I, and under CwA maps preserving the given logical structure on C.
Example 4.21. Note that for functoriality in I, the restriction to ordered discrete opfibrations is really unavoidable here -more so than for functoriality of the bare CwA C I .
A non-ordered discrete fibration u : J I will still induce a pseudo-map of CwA's C I C J : acting (strictly) naturally on types, and preserving context extension up to coherent isomorphism. However, that pseudo-map will not typically preserve the logical structure constructed in this section.
For instance, consider the "symmetry" automorphism σ : (−) Span (−) Span , switching 0 and 1. For any CwA C, this induces a symmetry pseudo-map σ * : C Span C Span ; but it is straightforward to check that this will not strictly preserve Π-types in general.

Homotopical diagrams
A homotopical category is a category C together with a distinguished subclass W of morphisms, containing all identities and closed under 2-out-of-6. The morphisms in W will be called equivalences.
A functor F : (C, W) (C ′ , W ′ ) is called homotopical if it preserves equivalences. Given a homotopical category C = (C, W), write C • for C considered as an ordinary category (i.e. with the equivalences forgotten).
In any CwA with identity types, we have the class of equivalences given by Definition 2.21. Given a homotopical inverse category I = (I, W), we can therefore consider homotopical diagrams on I in C.
The main goal of this section is to show that these form a sub-CwA C I of the ordinary diagram CwA C I • already constructed, and moreover that under reasonable assumptions, C I is closed under much of the logical structure on C I • .
5.1. Homotopical diagrams. For this section, fix a CwA C with Id-types.
Definition 5.2. Let I be an ordered homotopical inverse category.
A levelwise extension A of a diagram Γ in C I • is homotopical if for each equivalence α : i j in I, the comparison map Γ i . A i Γ i .Γ * α A j is an equivalence. A (Reedy) type in C I • is homotopical if it is so when viewed as a levelwise extension. Proof. Immediate by right properness and 2-out-of-3: if Γ α is an equivalence, then the comparison map Γ i . A i Γ i .Γ * α A j is an equivalence if and only if (Γ. A) α is.
Definition 5.5. Take C I (resp. C I lw ) to be the full sub-CwA of C I • (resp. C I • lw ) on homotopical diagrams and homotopical Reedy types (resp. homotopical levelwise extensions). The preceding propositions ensure that this indeed forms a sub-CwA.
In the remainder of this paper, we will consider homotopical types only over homotopical diagrams; we will therefore make use of Proposition 5.4 without comment.
It is easy to see that this construction is functorial in suitable maps: A map of CwAs with identity types will always preserve equivalences within fibrant slices, since these are defined in terms of identity types. However, the definition of general equivalences in CwA's is not algebraic, so their preservation is not automatic. For instance, every category C admits a CwA structure in which Ty is the terminal presheaf 1, and context extension acts trivially: every dependent projection is an identity map. Call this CwA (C, 1); it admits (a unique choice of) identity, unit, Σ-, and extensional Π-type structure. Each fibrant slice of (C, 1) is the terminal CwA, so every map in it is an equivalence. Meanwhile, with a little care, one can put a CwA structure on Set, equivalent to the usual one, except that over each context X, there is only one "singleton family" (i.e. only one A ∈ Ty(X) such that each A x is a singleton), and the context extension by this family is id X . Call this Set ′ ; it carries all the same structure mentioned above, and its equivalences will be just the isomorphisms. Now any functor F : C Set induces a CwA map (C, 1) Set ′ preserving the aforementioned structure; but if F hits any non-isomorphism, this will not preserve equivalences. Proof. The first statement is immediate by 2-out-of-3. The second follows since equivalences in fibrant slices are levelwise, by Lemma 4.14.
5.2. Logical structure. We give logical structure on C I by showing that, under suitable hypotheses, it is closed under the relevant operations in C I • . It is enough to show closure under the type-forming operations; for term-forming operations, closure is automatic since C I is a full subcategory.
For the covariant type-formers we consider, no extra hypotheses are needed: Proposition 5.9. For any ordered homotopical inverse cat I, C I is closed under the Idtype, Σ-type, and unit type operations on C I • constructed in Section 4.
Proof. We claim that in each case, the comprehension of the type produced is levelwise equivalent to a diagram which we already know is homotopical, so is homotopical by 5.8. The levelwise equivalences are given by the constructor maps Γ.1 Γ These maps are certainly equivalences in C I • , since they are always equivalences in any CwA with the logical structure in question. But they also lie within fibrant slices of C I • , and so by Lemma 4.14 are levelwise.
The question of closure under Π-types is less straightforward. To obtain this closure, we will assume two extra hypotheses: functional extensionality in C, and the condition that all maps in I are equivalences.
The extensionality hypothesis is unsurprising, since it is needed to know that Π-types respect equivalences in C. On the other hand, the hypothesis that all maps in I are equivalences seems quite possibly stronger than necessary. However, some restriction on I is certainly needed for the closure of C I under Π-types: To see this, note that equivalences in Set are exactly isomorphisms, and so Set WkMap ≃ Set → . Failure of closure then amounts roughly to the fact that Set → Set Span does not preserve exponentials, which may be seen from the standard calculation of exponentials in presheaf categories.
The proof that Π-types preserve homotopicality under these assumptions requires a couple of preparatory observations on the levelwise-to-Reedy Π-types given in Proposition 4.18. Fix for the next couple of lemmas a CwA with Id-and Π ext -structure C, and an ordered inverse category I. Lemma 5.11. Let A be a context extension over Γ in C; write C I Γ and C I A for the constant diagram and levelwise extension on these in C I . Let B be a Reedy type over Proof. By induction on i ∈ I, unwinding the construction of Proposition 4.18. Proposition 5.13. Let I be an ordered homotopical inverse category with all maps equivalences, and C a CwA with Id-and Π ext -structure. Then C I is closed under Π-types in C I • , and hence carries Π ext -structure.
Proof. Take homotopical diagrams and types Γ, A, and B as in the input of Π-formation; we need to show that Π[A, B] is homotopical.
Roughly, our strategy will be to show that under the given assumption on I, each component Π[A, B] i of the dependent product is "naturally" equivalent to the corresponding levelwise dependent product Π[A yi , B yi ], and then to note that this latter construction "respects equivalences". This is complicated by the fact that the levelwise dependent product does not itself form a diagram, since it is not covariantly functorial in the domain, so the desired "natural" equivalence can at best be dinatural; and also by the change of base due to its components living over different components of Γ.
Concretely, given α : i j in I, we will construct a diagram in C Here (−)| j/I denotes restriction of diagrams along the inclusion j/I I, and C j/I denotes constant diagrams. The map ν Γ : C j/I Γ j Γ| j/I has components given by the action on arrows of Γ, and is a levelwise equivalence since all arrows in I are equivalences, and ν Γ.A similarly. All un-named objects and arrows are given by context extension and pullback, as marked, and the remaining horizontal arrows are equivalences by right properness and 2-out-of-3.
The equivalence w 1 is given by the contravariant action of Π (Lemma 5.12) applied to the third column of this diagram, evaluated at id j ∈ j/I. Lemma 5.11 ensures that its domain, which by construction is as required for the main diagram. Then w 2 is the reindexing of w 1 along Γ α ; so it is an equivalence by stability in the base (or alternatively by 2 out of 3), and the square from w 2 to w 1 commutes.
Next, w 3 is given also by the contravariant action of Π, this time on the left-most column of the second diagram. The equivalence w 4 , by contrast, is given by the covariant action of iterated Π-types, Lemma 2.29. The last required map, w 5 , is constructed just like w 1 , but for i instead of j.
Finally, the pentagon in the main diagram commutes up to homotopy by extensionality for iterated Π-types (Lemma 2.28), along with the defining properties of the maps w i .
Putting together Propositions 5.9, 5.13, and , we have: Proposition 5.14. Let C be a CwA with Id-types, and I an ordered homotopical inverse category. Then the homotopical diagram CwA C I carries Id-types; if additionally C carries Σor unit types, then so does C I ; and if additionally all maps in I are equivalences, then if C carries extensional Π-types, so does C I . Moreover, all this logical structure is preserved by the functorial action under ordered homotopical discrete opfibrations in I, and under CwA maps preserving the given logical structure on C.

Properties of induced functors
We conclude by investigating conditions on functors u : J I under which the induced maps of CwA's u * : C I C J enjoy desirable extra properties. Specifically, we will want to know when this map is a local fibration, trivial fibration, or equivalence in the sense of [KL16], which we recall here: (1) F is a local fibration if it satisfies the properties • equivalence lifting: given any Γ ∈ C, A ∈ Ty C Γ, B ∈ Ty D (F Γ), and structured equivalence w : F A ≃ B over F Γ, there exists some liftB ∈ Ty C Γ of B, together with a structured equivalencew : A ≃B over Γ such that Fw = w; • path lifting: given any Γ ∈ C, A ∈ Ty C Γ, section a of the projection p A in C, section a ′ of p F A in D, and section e of p Id F A (F a,a ′ ) , there exist lifts of a ′ , e to C. (2) F is a local trivial fibration if it satisfies • type lifting: given any Γ ∈ C and A ∈ Ty D (F Γ), there exists some A ∈ Ty C Γ such that F A = A; • term lifting: given any Γ ∈ C, A ∈ Ty C Γ, and section a of F A in D, there exists some section a of A such that F a = a. (3) F is a local equivalence if it satisfies • weak type lifting: given any Γ ∈ C and A ∈ Ty D (F Γ), there exists A ∈ Ty C Γ and equivalence w : F Γ.F A ∼ F Γ.A over F Γ; • weak term lifting: given any Γ ∈ C, A ∈ Ty C Γ, and section a of F A in D, there exist some section a of A and propositional equality p : Id F A (F a, a).
We give these results just for homotopical diagram CwA's: the non-homotopical version then arises as a special case, by considering any ordinary category as a homotopical category with no maps marked as equivalences. No generality is lost, since local fibrations and equivalences already require consideration of Id-types.
For the remainder of this section, fix a CwA C with identity types. Proof. For type lifting, consider Γ ∈ C I , A ∈ Ty I (Γ), B ∈ Ty J (u * Γ), and an equivalence e : u * Γ.B u * Γ.u * A over u * Γ. We will define an extension B ∈ Ty I • (Γ) of B, along with a levelwise equivalence e : Γ.B Γ.A over Γ extending e. By Proposition 5.8, B must be homotopical since A is, and by Lemma 4.12, e will be an equivalence in C I , as required.
As usual, we work by induction on j ∈ I. If j = f i for some i ∈ J , we take B j = B i and e j = e i (an equivalence by 4.12). Otherwise, if j / ∈ im u, take B j to be (M j e) * A j and e j to be (M j e).A j : By Lemmas 4.9 and 4.10, M j e is an equivalence, and hence by right properness, so is e j . For term lifting, the argument is exactly parallel, using transport along a "matching map" propositional equality.
6.2. Equivalences between diagram CwA's. The main remaining goal of this section is to show that if an ordered discrete opfibration u : J I is a homotopy equivalence, then the induced map u * : C I C J is an equivalence of CwA's (Theorem 6.10 below). This involves several technical difficulties, arising from two main sources: firstly, from the zigzags witnessing the homotopy equivalence, and further zigzags and grids arising from these; and secondly, from the fact that the functors appearing in these zigzags may not be discrete opfibrations, so will not act on Reedy types. We therefore first establish some tools for dealing with these issues. Proof. Work by Reedy induction; suppose C, w have been constructed in dimensions < i. Then we have a map g i : (Γ. A) i M i C over Γ i , induced by f i together with w j for j ∈ i/J . Since g i lies in the fibrant slice C(Γ i ), we can obtain C i , w i by factoring it as (Γ. A) i w i M i C.C i M i C using [AKL15, Lem. 3.2.11]; that is, using the factorisation of [GG08, Lem. 11], then taking an iterated Σ-type to collapse the context extension factor into a single type.
An important special case of Lemma 6.4 is when B is the empty context extension; this gives the "Reedy replacement" of a levelwise extension A over Γ.
Lemma 6.5. Let J be an ordered homotopical inverse category, and suppose C is equipped with Σ-types. Suppose e : Γ ∼ ∆ is an equivalence in C J , and A a levelwise extension over Γ. Then there is a Reedy type B over ∆, and equivalenceē : Γ. A ∆.B over e.
Proof. First, by Lemma 6.4, we obtain a Reedy replacement for A, i.e. a Reedy type A ′ with an equivalence w 0 : Γ. A ∼ Γ.A ′ over Γ. Then, since e is an equivalence, its weak type lifting property gives a Reedy type B over ∆ along with an equivalence w 1 : Γ.A ′ ∼ Γ.e * B over Γ. Takingē := (e.B)w 1 w 0 : Γ. A ∆.B, we are done.
Lemma 6.9. Let J be an ordered homotopical inverse category. Suppose we have a commutative grid of diagrams Γ i,j in C J , with each row and column a zigzag of equivalences, as in the diagram below. Suppose moreover we have Reedy types A 0 , D 0 over Γ 0,0 , and a path of zigzags of levelwise extensions and equivalences between them going around the boundary of the base grid: Then there is some equivalence A 0 ∼ D 0 over Γ 0,0 .
Proof. First, by applying Lemma 6.7, we can assume that all the types involved are Reedy. By repeatedly applying Lemma 6.8, starting from the bottom right and proceeding upwards and leftwards, we can complete the path to a (not necessarily commutative) grid of Reedy types and equivalences over the base grid, except for the top-left square, which ends up like case (I) of the proof of Lemma 6.8. But now, just as in the proof of that case, we can obtain from this square an equivalence A 0 ∼ D 0 over Γ 0,0 as required.
We are now prepared for the main result: Theorem 6.10. Let u : J I be an ordered homotopical discrete opfibration between ordered homotopical inverse categories. If u is a homotopy equivalence, then the CwA map u * : C I C J is a local weak equivalence.
Proof. Take v : I J , along with zigzags η : id uv, ε : vu id of natural equivalences witnessing that u is a homotopy equivalence. (Note we cannot assume that v or the functors appearing in η, ε are discrete opfibrations.) First, we show weak type lifting for u * . The argument is rather involved, but in outline is entirely analogous to showing that an equivalence of categories F : C D (presented via unit and counit isomorphisms) induces an essentially surjective map on slices: • given A F C, apply a quasi-inverse G to get GA GF C; composing with the unit η C : C GF C gives GA C; • the co-unit gives an isomorphism ε A : F GA A, and provided the equivalence was adjoint, this isomorphism will be over F C; • if the original equivalence was not assumed adjoint, one adjointifies it beforehand, replacing ε with the modified co-unit ε · Gη −1 F · GF ε −1 . Returning to weak type lifting, take Γ ∈ C I , and A ∈ Ty J (u * Γ). Then v * A is a levelwise extension over v * u * Γ; so by alternately pulling back and pushing forward along the zigzag η * Γ (using Lemma 6.5), we obtain a typeĀ over Γ connected to v * A by a zigzag α :Ā v * A of levelwise equivalences between levelwise extensions over η * Γ : Γ v * u * Γ. (Here and in the rest of this proof, we write just A for the total object u * Γ.A, and similarly for other Reedy/levelwise extensions. ) We now need to show that u * Ā ≃ A over u * Γ. For this, we start by constructing a commutative grid of functors J I and zigzags of natural weak equivalences between (1) The definitions of Reedy types extend without difficulty from CwA's to more general comprehension categories, and it seems likely that the constructions of logical structure on C I should also extend to that setting, using something like the pseudo-stable logical structure of [LW14]. However, the basic theory of such logical structure on comprehension categories is as yet very little developed; so extending the present constructions to that setting would require a significant amount of preliminary development.
(2) Similarly, it seems likely that many of the present constructions should work without much modification not just for diagrams valued in a single CwA C, but for some analogue of the oplax diagrams considered in [Shu15]. (3) More concretely, our assumption in Proposition 5.13 that all maps in I are equivalences is certainly stronger than necessary for constructing Π-types in C I . On the one hand, there are at least some other cases where C I is closed under Π-types in C I • : for instance, the degenerate case where no maps in I are equivalences.
On the other hand, one may hope that C I may sometimes have Π-types even if they do not agree with those of C I • , as for instance in Example 5.10. It seems unlikely to us that C I as defined here can admit Π-types in such cases for general C; but it seems hopeful that by modifying C I to include chosen equivalence data, one might be able to construct Π-types for such examples. (4) [Shu15] shows that in the setting of type-theoretic fibration categories, univalent universes lift from the input categories to the categories of oplax inverse diagrams. It seems hopeful that an analogous construction should give univalent universes in our CwA's of homotopical inverse diagrams, but we have not pursued this since it was not needed in our applications. (5) The results of Section 6 were stated merely in terms of existence of liftings. However, their proofs gave rather more: pullback-stable type-and term-lifting operations, which moreover are functorial in various senses. These can therefore be read as constructing structured analogues of the fibrations and equivalences of [KL16,§3].