﻿Relating displayed algebra sections and sections in complete Segal types ======================================================================== Recall the complete Segal type model. Let us forget about the aspect of inner fibrancy and relative completeness of types. What remains is the canonical signature cwf over (D, W)_msemisimp = (Δ_{+,m}, {f : [k] → [n] | f(0) = 0}). Recall also the canonical signature cwfs used to define algebras/algebra morphisms/etc.: - signature cwf of algebras: (D, W)_alg = ({0}, ∅), - signature cwf of morphisms: (D, W)_hom = ({s, t : 0 → 1}, {s}), - signature cwf of displayed algebras: (D, W)_dalg = ({0 → 1}, ∅), - signature cwf of displayed algebra sections: (D, W)_dalgsect = ({0 → 1 → 2}, {0 → 2}). Given a signature S (context of initial signature cwf 0), we denote - msemisimp_S : Reedy fibrant type over Δ_{+,m} - alg_S : Ty - hom_S(X, Y) : Ty for X, Y : Ty, - dalg_S(X) : Ty for X : alg(S), - dalgsect_S(X, Y) : Ty for X : alg(S), Y : dalg(S)(X) the fibrant object of the respective canonical signature cwf that is the image of S under the unique morphism from 0. We wish to relate: - msemisimpl_S and associated notions of complete Segal types on one hand, - and alg_S/hom_S/dalg_S/dalgsect_S on the other hand. On the level of algebras and algebra morphisms, this is easy: - (D, W)_alg → (D, W)_Δ₊ is a sieve, inducing a restriction morphism of signature cwfs. This means that alg_S is simply level 0 of msemisimpl_S, i.e. alg_S = (msemisimpl_S)₀. - (D, W)_alg → (D, W)_Δ₊ is a sieve, inducing a restriction morphism of signature cwfs. This means that hom_S is simply level 1 of msemisimpl_S, i.e. hom_S(X, Y) = (msemisimpl_S)₁(X, Y). We now wish to show that the notion of displayed algebra Y over an algebra X of S coincides up to equivalence with the notion of edge f in semisimpl_S with target X. Furthermore, we wish to show that under this equivalence, the notion of displayed algebra section of Y corresponds to the notion of section of the edge f in msemisimpl_S discussed in an earlier note. Rather than show this by hand in these two cases, we note that they are instances of a more general phenomenon. - An edge in semisimpl_S is the same as a map Δ¹ → msemisimpl_S. Note that N [1] = Δ¹ where N denotes the nerve of a semicategory. But (D, W)_hom = ([1], ∅)! So an edge in semisimpl_S is a map N (D, W)_hom → msemisimpl_S. - We have defined a section in semisimpl_S as consisting of: * vertices x, x', and y * an edge f : (msemisimpl_S)₁(y, x), * an edge s : (msemisimpl_S)₁(x, y), * a marked edge e : (msemisimpl_S)₁(x', x), * a triangle u : (msemisimpl_S)₂(s, f, e). This is the same as a map A → semisimpl_S where A = (Δ², {02}). But A = N {{0 → 1 → 2}, {02}} = (D, W)_dhom where N denotes the nerve of a marked semicategory! So a section in semisimpl_S is a map N (D, W)_dhom → msemisimpl_S. The general pattern becomes clearer. For a finite marked direct category (D, W), the (fibrant) limit of the interpretation of S in the canonical signature cwf over (D, W) should be equivalent to the fibrant type of maps N (D, W) → msemisimpl_S. [This looks similar to Reedy fibrant strict diagrams versus homotopy coherent diagrams.] Note that the map ∫ N (D, W) → Δ_{+,m} is a discrete opfibration. [We can arrange for the slices of ∫ N (D, W) to be ordered so that this map is order preserving on slices.] Thus, restriction along it forms a morphism from the canonical signature cwf over Δ_{+,m} to the canonical signature cwf over ∫ N (D, W). The fibrant type of maps N (D, W) → msemisimpl_S is isomorphic to the (fibrant) limit of the interpretation of S in the canonical signature cwf over ∫ N (D, W). Furthermore, this correspondence is natural with respect to sieves between marked direct categories. What remains is the following. We want the (fibrant) limit of the interpretation of S in the following sigature cwfs to be equivalent: - canonical signature cwf over (D, W), - canonical signature cwf over ∫ N (D, W). Furthermore, the equivalence should live over the equivalence obtained when restricting along a sieve D' → D. Note that we have a functor p : ∫ N (D, W) → (D, W) sending an object σ : [n] → D to the last vertex σ(n). This functor is compatible with the markings, in fact it creates markings. It is also a local opfibration (local in the sense of only having local cartesian lifts, i.e. cartesian lifts characterized by a universal property, but not stable under composition; this corresponds to a lax bifunctor). Unfortunately, this is not enough for restriction along p to preserve Reedy fibrancy. However, right Kan extension along p is well behaved on fibrant objects. [Indeed, this is an abstract way to see the equivalence of strict Reedy diagrams and homotopy coherent diagrams.] In detail, right Kan extension along p induces a pseudomorphism of cwfs p_* : Presheaf_rf(∫ N (D, W))_fib → Presheaf_rf((D, W))_fib that preserves contractible types. This is perhaps best seen as an exact functor of fibration categories. In fact, one may show that it is a weak equivalence of fibration categories. For this, see notes that I wrote some time ago (available on request). In the language of cwfs, p_* has what Lumsdaine-Kapulkin call /weak type lifting/ and /weak term lifting/: type lifting and term lifting to lifts up to equivalence and identity type, respectively. How do we use p_* to relate the canonical signature cwfs over ∫ N (D, W) and (D, W), respectively? Since p_* is not a morphism of cwfs, we do not obtain commutativity with the unique map from the initial signature cwf. We could try to solve this by using a binary /glueing model/ (see the paper with Ambrus and Simon for a very explicit way of doing glueing for in the unary case) with a homotopicality restriction. The underlying category would be the oplax limit of the cospan p_* : Presheaf(∫ N D) → Presheaf(D) id : Presheaf(D) → Presheaf(D). That is, a context X consists of X₀ ∈ Presheaf(∫ N D) X₁ ∈ Presheaf(D) X₀₁ ∈ Presheaf(D) f₀ : X₀₁ → p_* X₀ f₁ : X₀₁ → X₁. For the types, one would make use of the fact that p_* descends to Reedy fibrant presheaves. One then has to separately check that p_* preserves homotopical Reedy fibrant presheaves (I have this check written up somewhere, can find it on request). A type A over X would be as in the binary glueing model, that is A₀ ∈ Ty_{Presheaf_rf(∫ N (D, W))}(X₀) A₁ ∈ Ty_{Presheaf_rf((D, W))}(X₁) A₀₁ ∈ Ty_{Presheaf_rf((D, W))}(X₀₁.(p_*(A₀) f₀).(A₁ f₁)) (weakening omitted), but with the additional homotopicality conditions that X₀₁.(p_*(A₀) f₀).(A₁ f₁).A₀₁ → X₀₁.(p_*(A₀) f₀) X₀₁.(p_*(A₀) f₀).(A₁ f₁).A₀₁ → X₀₁.(A₁ f₁) are equivalences over X₀₁. The verification that Π-types (with domain in U) in this model preserve homotopicality would have to use that the cwf morphism p_* : Presheaf_rf(∫ N (D, W)) → Presheaf_rf(∫ N (D, W)) preserves Π-types up to equivalence because it is in fact an equivalence of fibration categories. Let us leave this perspective open for further examination. I suspect it is actually equivalent to the following more explicit development. Consider the pushout {1 → 01} × ∫ N (D, W) ----[p]----> {1 → 01} × (D, W) | (*) | {0 → 01 ← 1, All} × ∫ N (D, W) --> (D_new, W_new). The category D_new can also be described as the oplax [or lax?] colimit of the span id : D → D p_* : ∫ N D → D. That is, presheaves over it are exactly the category of contexts from the above discussion on the glueing model approach. Let us describe this category explicitly. The objects are of the form: - (0, σ) for σ : [n] → D a semifunctor. - (1, I) for I ∈ D, - (01, I) for I ∈ D, The morphisms are of the following form. - The objects (0, -) form a full subcategory isomorphic to ∫ N D. That is, a map * (0, σ') → (0, σ) for σ : [n] → D and σ' : [n'] → D consists of h : [n'] → [n] such that σ' = σ h. Composition is evident. - The objects (1, -) and (01, -) and form a full subcategories isomorphic to [1] × D. That is, a map * (1, I') → (1, I) * (1, I') → (01, I) * (01, I') → (01, I) consists of f : I' → I. There are no maps * (01, I') → (1, I). Composition is evident. - Let σ : [n] → D and I ∈ D. There are no maps * (0, σ) → (1, I). A map * (0, σ) → (01, I) consists of g : σ(n) → I in D. The postcomposite with f : (01, I) → (01, J) is given by f g. The precomposite with h : (0, σ h) → (0, σ) where h : [n'] → [n] is given by the composition of g and the induced map σ(h(n')) → σ(n). Note that associativity holds. Under this description, note that a "heterogeneous" map in D_new described by an f : I' → I in D is in W_new exactly if f is in W. Note that the construction sending D to D_new is a cocontinuous endofunctor in the category of direct categories with discrete opfibrations as morphisms. Its functorial action preserves sieves. Let H be the following class of monomorphisms H in presheaves over D_new: - y(01, I)|({0} × ∫ N D) → y(01, I) for I ∈ D. Here, y(01, I)|({0} × ∫ N D) consists of all maps f : (0, σ) → y(01, I) for σ : [n] → D and f : σ(n) → I. - id_I : y(1, I) → y(01, I) for I ∈ D. We will build a signature cwf whose basic cwf structure is the Reedy fibration model over D_new restricted to those types that are orthogonal against H. The details of the model are very similar to those of Lemma 3 in variations-equivalent.txt It is essentially a heterogeneous variation of it. The universe (U, El) is the classifier for Reedy ty-types that are homotopical with respect to W_new. The only interesting checks will be the universe and dependent products with domain in U forming types. To facilitate these checks, we define a variant H' of H of monomorphisms in presheaves over D_new. - Let I ∈ D. Then S₀(I) → y(01, I) is in H where the sieve S₀(I) consists of: * f : (0, σ) → (01, I) for σ : [n] → D and f : σ(n) → I, * f : (1 , I') → (01, I) for non-identity f : I' → I, * f : (01, I') → (01, I) for non-identity f : I' → I. Note that the complement consists of two elements: * id_I : (1 , I) → (01, I), * id_I : (01, I) → (01, I). - Let I ∈ D. Then S₁(I) → y(01, I) is in H where the sieve S₁(I) consists of: * f : (0, σ) → (01, I) for σ : [n] → D and non-identity f : σ(n) → I, * f : (1, I') → (01, I) for f : I' → I, * f : (01, I') → (01, I) for non-identity f : I' → I. Note that the complement consists of: * id_I : (0, σ) → (01, I) for σ : [n] → D with σ(n) = I, * id_I : (01, I) → (01, I). Lemma 1. H and H' have the same closure under: - pushouts, - finite compositions, - pre-cancellation (if u and v u are in, then v is in) in monomorphisms in presheaves over D_new. As a consequence, the following are equivalent for Reedy fibrant A over X ∈ Presheaf(D_new): - H ⊥ A, - H' ⊥ A. Proof. This is just combinatorics (no fibrant types involved). Let Cl(-) denote the closure operation of the statement. For I ∈ D_New, let H_{≤I}, H_{ S₀(I) --> y(01, I). The complement of the first factor consists of: - f : ( 1, I') → (01, I) for non-identity f : I' → I, - f : (01, I') → (01, I) for non-identity f : I' → I. It is a finite cell complex (composite of pushouts) of S₀(I') → y(01, I') for non-identity f : I' → I. In particular, it is in Cl(H_{ S₁(I) --> y(01, I). The complement of the first factor consists of: - f : (0, σ) → (01, I) for σ : [n] → D and non-identity f : σ(n) → I, - f : (01, I') → (01, I) for non-identity f : I' → I. It is a finite cell complex of S₁(I') → y(01, I') for non-identity f : I' → I. In particular, it is in Cl(H_{ {0} × ∫ N (D, W) --> (D_new, W_new), (D, W) --> {1} × (D, W) --> (D_new, W_new) induce morphisms of signature cwfs to the canonical signature cwf over∫ N (D, W) and (D, W), respectively. Proof. The following constructions work the same as before: - identity types in U, - Tm(A)-indexed products of types for fibrant A, - Tm(A)-indexed products in U for fibrant A. We do not bother going through them again. The core of the model is in the following: - orthogonality of U against H, - orthogonality of Π-types with domain in U against H. In all cases, the constructions of the model at stages (0, σ) for σ ∈ ∫ N D and (1, I) for I ∈ D is chosen such that it agrees with the corresponding stage in the canonical signature cwf over ∫ N (D, W) and (D, W), respectively. Note that the maps in the statement of the lemma are sieves that create weak equivalences. This guarantees that the restriction maps form morphisms of signature cwfs as required. Universe U ---------- We check that H ⊥ U. By Lemma 1, this is equivalent to H' ⊥ U. Inspecting the proof of Lemma 1, we can mix these two condition. We will show that U is orthogonal against the following sieves: (1) S₀(I) → y(01, I) for I ∈ D, (2) id_I : y(1, I) → y(01, I) for I ∈ D. We proceed by induction on I. Let us do (2). We recall for M ∈ D_new that hom(M, D) = Presheaf_rf((D_new, W_new)/M) is the type of homotopical Reedy-ty presheaves over (D_new, W_new)/M. We have to show that the restriction map Presheaf_rf((D_new, W_new)/(01, I)) → Presheaf_rf((D_new, W_new)/(1, I)) is an equivalence. This is an instance of Corollary S.3 below (since y(1, I) → y(01, I) is a sieve, it is a discrete opfibration). For this, we note that (D_new, W_new)/(1, I) → (D_new, W_new)/(01, I) is a homotopy equivalence by Lemma S.5 below. Let us do (1). Let T be the sieve of (01, I) consisting of: - f : (0, σ) → (01, I) for σ : [n] → D and non-identity f : σ(n) → I, - f : (1 , I') → (01, I) for non-identity f : I' → I, - f : (01, I') → (01, I) for non-identity f : I' → I. Using functoriality properties of D ↦ D_new noted earlier, ∂(1, I) → T is a finite cell complex of S₀(J) → y(01, J) for non-identity J → I. By induction hypothesis, we know S₀(J) → y(01, J) ⊥ U. It follows that (3) ∂(1, I) → T ⊥ U. We are given - X_((0, σ), f) : U(0, σ)(…) for σ : [n] → D and non-identity f : σ(n) → I, - X_((1, I'), f) : U(1, I')(…) for f : I' → I, - X_((01, I'), f) : U(01, I')(…) for non-identity f : I' → I. We wish to show that the dependent sum of X_((1, I), id_I) : U(1, I)(…) X_((01, I), id_I) : U(01, I)(…) is contractible. Let us combine Lemmas 2 and 3. The resulting statement says that homotopicality for W_new is equivalent to the following two conditions: - orthogonality against H', - homotopicality for the markings in {0} × ∫ N (D, W). Let V denote the universe of Reedy-ty types. Using the above, U(01, I)(…) consists of (up to equivalence) of fibrant families X_(01,id_I) : V(01, I)(…) = (…) → ty such that X is orthogonal against S₀(I) → y(01, I), S₁(I) → y(01, I). More specifically, this means (hom)(S₀(I) → y(01, I), X)(id, x₁) (hom)(S₁(I) → y(01, I), X)(id, x₁) are contractible for all x₀ and x₁, respectively. We now rewrite (up to equivalence) the dependent sum X_((1, I), id_I) : U(1, I)(…) X_((01, I), id_I) : U(01, I)(…) to the dependent sum X_((1, I), id_I) : V(1, I)(…) X_((1, I), id_I) homotopical with respect to f : (1, I') → (1, I) for f : I' → I in W X_((01, I), id_I) : V(01, I)(…) (hom)(S₀(I) → y(01, I), X)(id, x₀) contractible ∀x₀ (hom)(S₁(I) → y(01, I), X)(id, x₁) contractible ∀x₁. In turn, this is equivalent to the dependent sum X_((1, I), id_I) : V(1, I)(…) X_((01, I), id_I) : V(01, I)(…) (hom)(S₀(I) → y(01, I), X)(id, x₀) contractible ∀x₀ (hom)(S₁(I) → y(01, I), X)(id, x₁) contractible ∀x₁. For this, note that the homotopicality condition for X_((1, I), id_I) with respect to f : (1, I') → (1, I) for f : I' → I in W follows from that for X_(0, f : [1] → D) with respect to 1 : (0, I' : [0] → D) → (0, f : [1] → D) by 2-out-of-3 in a diagram of weighted limits of X induced by (the image under Yoneda of) the following diagram of weights: (0, I' : [0] → D) --> (01, I') --> (1, I') | | | (0, f : [1] → D) ---> (01, I) ---> (1, I). Here, all horizontal maps and the left vertical maps get sent to equivalences. Now we rewrite V(1, I)(…), = hom(∂(1, I), X)(•) → ty ≃ hom(T, X)(•) → ty, recalling from (3) that ∂(1, I) → T ⊥ X. With this, the dependent sum X_((1, I), id_I) : V(1, I)(…) X_((01, I), id_I) : V(01, I)(…) (hom)(S₀(I) → y(01, I), X)(id, x₀) contractible ∀x₀ (hom)(S₁(I) → y(01, I), X)(id, x₁) contractible ∀x₁. rewrites as X_((1, I), id_I) : hom(T, X)(•) → ty, X_((01, I), id_I) : hom(∂(01, I))(id) → ty, (hom)(S₀(I) → y(01, I), X)(id, x₀) contractible ∀x₀ (hom)(S₁(I) → y(01, I), X)(id, x₁) contractible ∀x₁. This is the product over x : hom(T, X)(•) of X_((1, I), id_I) : ty, X_((01, I), id_I) : (hom)(T → S₀(I), X)(•, x) × X_((1, I), id_I) → ty, [x₁ : X_((1, I), id_I), x₀₁ : X_((01, I), id_I)(x₀, x₁)] contractible ∀x₀ [x₀ : (hom)(T → S₀(I), X)(•, x), x₀₁ : X_((01, I), id_I)(x₀, x₁)] contractible ∀x₁. Using univalence, the latter is a presentation of X_((1, I), id_I) : ty, X_((01, I), id_I) : (hom)(T → S₀(I), X)(•, x) ≃ X_((1, I), id_I), hence contractible. Π-types with domain in U ------------------------ Let X be a context, A : X → U, and B : Ty(X.(El A)). We check that H' ⊥ Π_E(A, B). There are two cases: 1. S₀(I) → y(01, I) for I ∈ D, 2. S₁(I) → y(01, I) for I ∈ D. The strategy for H' ⊥ Π_E(A, B) is as before, reducing to H' ⊥ B. For this, following the previous strategy, we need that all maps into y(01, I) in the complement of either 1. or 2. are in W_new. For 1., this is - id_I : (1 , I) → (01, I), - id_I : (01, I) → (01, I), clearly in W_new. For 2., this is - id_I : (0, σ) → (01, I) for σ : [n] → D with σ(n) = I, - id_I : (01, I) → (01, I), clearly in W_new. Note that the only relevant fact concering W is that it contains all identities. This ends the construction of the signature cwf. □ Recall the missing part of our development. Let S be a signature (object of the initial signature cwf). Denote - X₀ the interpretation of S in the canonical signature cwf over ∫ N (D, W), - X₁ the interpretation of S in the canonical signature cwf over (D, W). These are fibrant contexts, i.e - X₀ is a Reedy fibrant presheaf over ∫ N D, - X₁ is a Reedy fibrant presheaf over D. We want that hom(1, X₀) ≃ hom(1, X₁). Furthermore, this equivalence should live over the equivalence obtained when restricting along a sieve D' → D. Let X₀₁ denote the interpretation of S in the signature cwf constructed in Lemma 3. We obtain a fibrant context. This is, X₀₁ is a Reedy fibrant presheaf over D_new that is orthogonal against H. Using the restriction signature cwf morphisms of Lemma 3, we have: - the restriction of X₀₁ to {0} × ∫ N (D, W) is X₀, - the restriction of X₀₁ to {1} × (D, W) is X₁. Using finite cell complexes built from H', we have that X₀₁ is orthogonal against - 1|({0} × ∫ N D) → 1, - 1|({1} × D) → 1. This means that the Reedy fibrant span hom(1, X₀₁) → hom(1, X₀) × hom(1, X₁) has legs that are trivial fibrations. Thus, it presents an equivalence between hom(1, X₀) and hom(1, X₁). Furthermore, this equivalence is natural in the desired way with respect to sieves D' → D by construction. Standard tools for Reedy fibrations =================================== For a finite marked direct category (D, W), we write Presheaf_rf(D, W) for the fibrant type of homotopical Reedy-ty presheaves (i.e. homotopical Reedy fibrant diagrams whose fibrant type over each matching object is classified by ty). We write Presheaf_f(D, W) for the (non-fibrant) type of homotopical levelwise-ty presheaves (i.e. levelwise fibrant homotopical presheaves whose value at every level is classified by ty). We will ignore smallness issue in the following. Instead of ty-types, we will just speak of fibrant types and the reader is supposed to insert references to the universe ty as appropriate. We have an evident forgetful map Presheaf_rf(D, W) → Presheaf_f(D, W), often left implicit. (In the absence of η for fibrant 1/Σ, there are some subtleties that require one to work with ty-telescopes.) Recall the fibrant replacement operation Q : Presheaf_f(D, W) → Presheaf_rf(D, W). It associates to each levelwise-ty presheaf X a Reedy-ty presheaf QX with a natural transformation between levelwise-ty presheaves η_X : X → QX that is levelwise an equivalence. Note that by 2-out-of-3, if X is homotopical, then so is QX. Let f : (D₀, W₀) → (D₁, W₁) be a map between marked finite direct categories. We write f^* : Presheaf_f(D₁, W₁) → Presheaf_f(D₀, W₀) for the evident restriction map. If we wish to pass between Reedy fibrant presheaves, we have to use Q f^* : Presheaf_rf(D₁, W₁) → Presheaf_rf(D₀, W₀). If f is a discrete opfibration, then no fibrant replacement is needed and we obtain f^* : Presheaf_rf(D₁, W₁) → Presheaf_rf(D₀, W₀). Lemma S.1. Let f, g : (D₀, W₀) → (D₁, W₁) be maps between finite marked direct categories. Let u : f → g be a natural transformation valued in marked maps. Then u induces a homotopy between Q f^*, Q g^* : Presheaf_rf(D₁, W₁) → Presheaf_rf(D₀, W₀). Proof. Proved by Reedy induction. □ An /element homotopy/ between maps f, g : (D₀, W₀) → (D₁, W₁) between marked direct categories is a natural transformation f → g valued in marked maps. A homotopy, written f ~ g, is a zig-zag of elementary homotopies. A map f : (D₀, W₀) → (D₁, W₁) between marked direct categories is called a /homotopy equivalence/ if there is g : (D₁, W₁) → (D₀, W₀) that is homotopy inverse, i.e. f g ~ id g f ~ id. Note that homotopy equivalences are: - invariant under homotopy, - closed under 2-out-of-6, - closed under finitary product. Corollary S.2. Let f : (D₀, W₀) → (D₁, W₁) be a homotopy equivalence between finite marked direct categories. Then Q f_* : Presheaf_rf(D₁, W₁) → Presheaf_rf(D₀, W₀) is an equivalence. Proof. This follows immediately from Lemma 1. □ Corollary S.3. In the situation of Corollary 2, assume that f is a discrete opfibration. Then f_* : Presheaf_rf(D₁, W₁) → Presheaf_rf(D₀, W₀) is an equivalence. □ For the next few statements, recall from (*) the construction of the marked direct category (D_new, W_new) from a marked direct category (D, W). Lemma S.4. The map (D, W) = {1} × (D, W) --> (D_new, W_new). is a homotopy equivalences. Proof. We factor the map as {1} × (D, W) --> {1 → 01, All} × (D, W) --> (D_new, W_new). The map {1} → {1 → 01, All} is a homotopy equivalence (with unique homotopy inverse). Thus, the first factor is a homotopy equivalene. For the second factor f : {1 → 01, All} × (D, W) → (D_new, W_new), recall the last vertex projection p : ∫ N (D, W) → (D, W). We define a homotopy inverse g : (D_new, W_new) → {1 → 01, All} × (D, W) of f acting as the identity on {1 → 01, All} × (D, W) and sending (0, σ : [n] → D) to (01, p(σ) = σ(n)). The action on maps is obvious. Note that g f = id. In the other direction, we have id → f g sending (1, I) and (01, I) to identities in D_new and (0, σ : [n] → D) to id_σ(n) : (0, σ) → (01, σ(n)), which is in W_new. □ Lemma S.5. For I ∈ D, the map (D_new, W_new)/(1, I) → (D_new, W_new)/(01, I) is a homotopy equivalence. Proof. Note that (D_new, W_new)/(1, I) = {1}/1 × (D, W)/I. We factor the given map as {1}/1 × (D, W)/I --> {1 → 01, All}/01 × (D, W)/I --> (D_new, W_new)/(01, I). The map {1}/1 --> {1 → 01, All}/01 is a homotopy equivalence as in Lemma S.4 Hence the first factor is a homotopy equivalence. For the second factor f, we define a homotopy inverse g : (D_new, W_new)/(01, I) --> {1 → 01, All}/01 × (D, W)/I. acting as the identity on {1 → 01, All}/01 × (D, W)/I and sending ((0, !), (σ : [n] → D, f : σ(n) → I)) to ((01, !), (σ(n), f)). The action on maps is obvious. Note that g f = id. In the other direction, we have id → f g sending ((1, !), (I', f : I' → I)) ((01, !), (I', f : I' → I)) to identities in D_new and sending ((0, !), (σ : [n] → D, f : σ(n) → I)) to id_{σ(n)} : ((0, !), (σ : [n] → D, f : σ(n) → I)) → ((01, !), (σ(n), f)), which is in W_new. □