﻿Table of contents: - A. Universe of left fibrations as higher category of spaces - B. Finite completeness of universe of left fibrations - C. Finite limits from terminal objects and pullbacks A. Universe of left fibrations as higher category of spaces =========================================================== The universe of left fibrations should model the higher category of spaces. To see this, we prove a series of useful facts. Recall the universe U = U_left : SSet_m of left fibratons. It comes with left fibrant El : Ty_{SSet_m,rf}(U). It can be defined by restricting the universe of Reedy fibrations as follows. At level n, given matching data A : M_n U, we keep only those A_n : (M_n El)(A) → ty for which the composite projection (a : (M_n El)(A)) × A(a) → (M_n El)(A) → A_0 induced by {0} → ∂Δ^n → Δ^n is an equivalence (trivial fibration). Lemma A.1. The universe U of left fibrant objects is a complete Segal type. Proof. We first show that it is a Segal type, i.e. inner fibrant. Let us not worry about special outer horns here and only consider inner horns. We check Λ^n_k → Δ^n ⊥ U for 0 < k < n. That is, given X : Λ^n_k → U, want (hom)(Λ^n_k → Δ^n, U)(X) contractible. We compute (hom)(Λ^n_k → Δ^n, U)(X) = (A : U_{n-1}(X|∂Δ^{[n]-k})) × (B : U_n(X, A)) = [ A : (M_{n-1} El)(X|∂Δ^{[n]-k}) → ty , (a₀ : El(X|0)) → is-contr (hom)({0} → Δ^{[n]-k}, El)((X|Δ^{[n]-k}, A), a) , B : (M_n El)(X, A) → ty , (a₀ : El(X|0)) → is-contr (hom)({0} → Δ^n, El)((X, A, B), a) ] = (a₀ : El(X|0)) → [ A : (hom)({0} → ∂Δ^{[n]-k}, El)(X|∂Δ^{[n]-k}, a₀) → ty , A representable , B : (hom)({0} → ∂Δ^n, El)((X, A), a) → ty , B representable ] where P : C → ty is said to be representable if (c : C) × P(c) is contractible. Note that we have used k > 0 in the above chain of equations to ensure that the initial vertices of Δ^{[n]-k} and Δ^n coincide. It suffices to show given a₀ : El(X|0) that the inner expression is contractible. We compute [ A : (hom)({0} → ∂Δ^{[n]-k}, El)(X|∂Δ^{[n]-k}, a₀) → ty , A representable , B : (hom)({0} → ∂Δ^n, El)((X, A), a) → ty , B representable ] = [ A : (hom)({0} → ∂Δ^{[n]-k}, El)(X|Δ∂^{[n]-k}, a₀) → ty , A representable , B : [ M : (hom)({0} → ∂Δ^{[n]-k}, El)(X|∂Δ^{[n]-k}, a₀) , N : (hom)(∂Δ^{[n]-k} → Δ^{[n]-k}, El)((X|∂Δ^{[n]-k}, A), (a₀, M)) , O : (hom)(∂Δ^{[n]-k} → Λ^n_k, El)(X, (a₀, M)) ] → ty , B representable ]. Note that the Σ-type of M and O as above, given by (hom)({0} → Λ^n_k, El)(X, a₀), is contractible. Indeed, since k < n, we have {0} → Λ^n_k ∈ Cell(J_left) and J_left ⊥ El. The claim now follows from Lemma A.2 below. To finish the check that U is a complete Segal type, it remains to identify the invertible edges and check completeness. For this, we use a more explicit description of the lowest levels of U. Consider the following Reedy fibrant type over Δ_+^{≤2}: - V₀ = ty - V₁(A₀, A₁) ≃ A₀ → A₁ - V₂( A_i for 0 ≤ i ≤ 2, , f_ij : A_i → A_j for 0 ≤ i < j ≤ 2 ) ≃ (a₀ : A₀) → f₁₂(f₀₁(a₀)) = f₀₂(a₀). It is straightforward to check that V ≃ U|^{≤2}. In V, the invertible edges are given by equivalences: V₁^inv(A₀, A₁, f : A₀ → A₁) = is-equiv f. Completeness is thus exactly univalence. □ Lemma A.2. Let B : A → U be representable. Then the dependent sum of P : A → U representable and Q : (a : A) (p : P(a)) (b : B(a)) → U representable is contractible. Proof. Since P is representable, the type of (P, Q) as above is equivalent to P : A → U representable Q : (b : B()) → U representable. By Yoneda applied to P, this is equivalent to a : A Q : (b : B(a)) → U representable. By Yoneda applied to Q, this is equivalent to a : A b : B(a). This is contractible since B is representable. □ The universe ty of fibrant types has the structure of a semicategory: - the fibrant types of objects is ty - the fibrant type of morphisms from X to Y is X → Y. (If fibrant exponentials have η, then this has the structure of a category.) We take the nerve N ty of this semicategory, resulting in a levelwise fibrant semisimplicial type. It thus makes sense to talk about Reedy fibrant replacements of N ty. Lemma A.3. Any fibrant replacement V of N ty is inner fibrant. Proof. Consider 0 < a < n. Recall that {0, …, n} is the pushout of {a} → {0, …, a} and {a} → {a, …, n} in Δ_+. This pushout is not preserved under Yoneda. Let instead D → Δ^n denote the pushout corner map in its image under Yoneda, i.e. D = Δ^{0,…,a} +_{Δ^{a}} Δ^{a, …, n}. To show that V is inner fibrant, it suffices to prove that D ⊥ V. This means that V_{0, …, n} --> V_{0, …, a} | | V_{a, …, n} --> V_{a} should be a homotopy pullback in fibrant types. Since V was constructed as a Reedy fibrant replacement, this square is equivalent to (N ty)_{0, …, n} --> (N ty)_{0, …, a} | | (N ty)_{a, …, n} --> (N ty)_{a}. As for any nerve, this is a strict pullback. Since the maps into (N ty)_{a} are additionally fibrations, it is also a homotopy pullback. The claim now follows by invariance of homotopy pullbacks under equivalence. □ Lemma A.4. Let e : N ty → V be a Reedy fibrant replacement. Then V\e₀(1) → V is a left fibration. Its classifying map c : V → U is an equivalence. Proof. Lemma A.3 showed that V is inner fibrant. It follows that V\e₀(1) → V is a left fibration. It thus has a classifying map c : V → U that witnesses V\e₀(1) → V as a strict pullback of U.El → U. To show that c : V → U is an equivalence, it thus suffices to verify this on levels 0 and 1. This means to check that the following maps are equivalences: - c₀ : V₀ → U₀ c₀(X) = V₁(e₀(1), X), - c₁ : V₁(X, Y) → U₁(c₀(X), c₀(Y)) c₁(f)(x, y) = V₂(f, y, x). Since N ty → V is a Reedy fibrant replacement, we have equivalences. e₀ : ty ≃ V₀, e₁ : A → B ≃ V₁(e₀ A, e₀ B), e₂ : (a : A) → g(f(a)) = h(a) ≃ V₂(e₀ A, e₀ B, e₀ C, e₁ f, e₁ g, e₁ h). Under these equivalences, the previous maps become - c₀ : ty → U₀ c₀(X) = 1 → X, - c₁ : (X → Y) → U₁(1 → X, 1 → Y) c₁(f)(x, y) = (* : 1) → f (x ⋆) = y ⋆. Under the equivalence 1 → X ≃ X, these become: - c₀ : V₀ → U₀ c₀(X) = X, - c₁ : V₁(X, Y) → U₁(X, Y) c₁(f)(x, y) = f x = y. These are clearly equivalences. □ Lemma A.5. The universe U of left fibrant objects is a Reedy fibrant replacement of N ty. Proof. Let N ty → V be an arbitrary Reedy fibrant replacement. By Lemma A.4, we have an equivalence V → U. This shows that U is a Reedy fibrant replacement of N ty as well. □ Remark A.6. Note that the induced map N ty → U sends the object 1 to a contractible type. Using Lemma A.4, it thus follows that U\1 → U is a strict pullback U.El → U along an equivalence. In particular, the maps U\1 → U and U.El → U are equivalent. Since U is univalent, one may use U\1 → U just as well as a classifying map (in the sense of complete Segal types) for left fibrations. □ B. Finite completeness of universe of left fibrations ===================================================== We present two approaches to the following claim. Lemma B.1. The universe U of left fibrations is finitely complete. The first approach one is self-contained. The second one depends on Section F (which is general, not depending on this section). Recollection: finite limits in complete Segal types --------------------------------------------------- We recall the cone operation on complete Segal types. Fix a simplicial type K. Let first X just be a simplicial type. Given a diagram d : K → X, we have a simplicial type X/d. This is the action of the right adjoint to - * K : SSet → SSet\K. In particular, an n-simplex in X/d is a map Δ^n ⋆ K → X that restricts to d on K. This operation lifts to types in the cwf SSet. Given X : SSet, d : K → X, Y : Ty_SSet(X), and e : Tm_SSet(K, Y d), we have Y/e : Ty_SSet(X/d) defined as (Y/e)_n(x : Δ^n ⋆ K → X restricting to d on K) = Tm_SSet(Δ^n ⋆ K, Y x) restricting to e on K = (hom)(K → Δ^n ⋆ K, Y)(x, e) If you think of types Y in SSet via their comprehension X.Y → X, this is the functorial action of the cone operation SSet\K → SSet. Note that t : Tm_SSet(X, Y) gives rise to Tm_SSet(X/d, Y/(t d)). We have the same operation in SSet_m for marked semisimplicial types K. Let K now be finite (meaning that 0 → K is in Cell(I)). In that case, the cone operation interacts well with Reedy fibrancy: - if X is Reedy fibrant, then so is X/d, - if Y is Reedy fibrant, then so is Y/e, - if X is a complete Segal type, then so is X/d, - if Y is inner fibrant, then so is Y/e. A complete Segal space X is said to be /finitely complete/ (i.e. have finite limits) if X/d has a terminal object for each finite diagram d : K → X. First approach -------------- Proof of Lemma B.1. We verify that U has finite limits. For this, let d : K → U be a finite diagram. We have to find a terminal object in U/d. We have El d : Ty_{SSet_m,rf}(K). Since K is finite, L = Tm_{SSet_m}(K, El d) is fibrant. In the remainder, we will construct an equivalence U/d ≃ U/L. Since U/L is a slice category, it has a terminal object. Then U/d does as well, and we will be finished. Both U/d and U/L come with a forgetful map to U. We construct a map f : U/d → U/L over U. On level 0, we are given A : Δ⁰ ⋆ K → U restricting to d on K. We take f₀(A)₁ = A|Δ⁰ f₀(A)₂(a, l) = λ(a, l). (hom)(Δ⁰ + K → Δ⁰ ⋆ K, El)(A, (a, l)) = λ(a, l). . Note that fixing a : A|0, the Σ-type of l and f₀(A)₂(a, l) is contractible as required. This is an instance of Δ⁰ → Δ⁰ ⋆ K ⊥ El, which holds since Δ⁰ → Δ⁰ ⋆ K ∈ Cell(J_left). On level 1, we are given A : Δ¹ ⋆ K → U restricting to d on K. We define f₁(A)₁(a₀, a₁) = A|Δ¹(a₀, a₁) f₁(A)₂(a₀, a₁, a₀₁, l, r₀, r₁) = (hom)(∂Δ¹ ⋆ K ∪ Δ¹ → Δ¹ ⋆ K, El)(A, a₀, a₁, a₀₁, l, r₀, r₁) = Note that fixing a₀ : A|0, the Σ-type of a₁, a₀₁, l, r₀, r₁ and f₁(A)₂(a₁, a₀₁, l, r₀, r₁) is contractible as required. This is an instance of {0} → Δ¹ ⋆ K ⊥ El, which holds since - {0} → {0} ⋆ K ∈ Cell(J_left), - {0} ⋆ K → Δ¹ ⋆ K ∈ Cell(J_left) (J_left is stable under - ⋆ K). In general, on level n, we are given A : Δ^n ⋆ K → U restricting to d on K. We define f_n(A)₁(a : Tm(∂Δ^n, El A)) = A|Δ^n(a) f_n(A)₂(a : Tm(∂Δ^n ⋆ K ∪ Δ^n, El A)) = (hom)(∂Δ^n ⋆ K ∪ Δ^n → Δ^n ⋆ K)(A, a) = B | |[f] C --[g]-> D be a (strict) pullback of complete Segal types. Assume that: - B and C have terminal objects, - D has binary products, - B → D and C → D are right fibrations. Then A has a terminal object. Think of right fibrations over D as presheaves over D. The pullback A models the product of the presheaves B and C. The lemma then says that if the base D has binary products, then representable presheaves are closed under binary products. This can be seen as a special case of the fact that the higher Yoneda functor preserves limits. Proof of Lemma C.1. Without loss of generality, we identify A₀ = [d : D₀ , b : B₀ , c : C₀ , f b = d , g c = d] (with all equalities strict) and similarly for higher cells. We take terminal objects t_B : B₀ t_C : C₀. We take the product of f t_B and g t_c in D: d : D₀ u : D₁(d, f t_B) v : D₁(d, g t_C) Since B → D and C → D are right fibrations, we have lifts b : B₀ with f b = d u' : B₁(b, t_B) with f u' = u and c : C₀ with g c = d v' : C₁(c, t_C) with g v' = v. We claim that (d, b, c) : A₀ is terminal. Let (d', b', c') : A₀ be arbitrary. We compute via insertions and deletions of contractible singletons A₁((d', b', c'), (d, b, c)) = [ d₀₁ : D₁(d', d) , b₀₁ : B₁(b', b) over d₀₁ via f , c₀₁ : C₁(c', c) over d₀₁ via g ] ≃ (taking the composite of d₀₁ with the span in D (insertion)) [ d₀₁ : D₁(d', d) , x : D₁(d', f t_B) , x-coh : D₂(d₀₁, u, x) , y : D₁(d', g t_C) , y-coh : D₂(d₀₁, v, y) , b₀₁ : B₁(b', b) over d₀₁ via f , c₀₁ : C₁(c', c) over d₀₁ via g ] ≃ (using that f and g are right fibrations (insertion then deletion)) [ d₀₁ : D₁(d', d) , x : D₁(d', f t_B) , x-coh : D₂(d₀₁, u, x) , y : D₁(d', g t_C) , y-coh : D₂(d₀₁, v, y) , b₀₁ : B₁(b', t_B) over x via f , c₀₁ : C₁(c', t_C) over y via g ] ≃ (using the universal property of the product in D, we contract d₀₁ with the coh-terms (deletion)) [ x : D₁(d', f t_B) , y : D₁(d', g t_C) , b₀₁ : B₁(b', t_B) over x via f , c₀₁ : C₁(c', t_C) over y via g ] = [ b₀₁ : B₁(b', t_B) , c₀₁ : C₁(c', t_C) ] ≃ (since t_B and t_C are terminal) 1. □ Lemma C.1b. Let X be a complete Segal type. If X has pullbacks and terminal objects, it has binary products. Proof. We compute the product of a, b : X₀. Let t : X₀ be terminal. From terminality, we get f : X₁(a, t) g : X₁(b, t). We take the pullback p : X₀ u : X₁(p, a) v : X₁(p, b) w : X₁(p, t) α : X₂(u, f, w) β : X₂(v, g, w). We claim that (p, u, v) : (X/(a, b))₀ is terminal Let (p', u', v') : (X/(a, b))₀, that is p' : X₀ u' : X₁(p', a) v' : X₁(p', b), be arbitrary. Since t is terminal, we have w' : X₁(p', t) α' : X₂(u', f, w') β' : X₂(v', g, w'). We compute via insertions and deletions of contractible singletons (X/(a, b))₁((p', u', v'), (p, u, v)) = [ p₀₁ : X₁(p', p) , u₀₁ : X₂(p₀₁, u, u') , v₀₁ : X₂(p₀₁, v, v') ] ≃ (since t is terminal) [ p₀₁ : X₁(p', p) , u₀₁ : X₂(p₀₁, u, u') , v₀₁ : X₂(p₀₁, v, v') , w₀₁ : X₂(p₀₁, w, w') , α₀₁ : X₃(α, α', w₀₁, u₀₁) , β₀₁ : X₃(β, β', w₀₁, v₀₁) ] ≃ (using the universal property of the pullback) 1. □ Lemma C.2. Let j : A → B be in Cell(J_{left,m}). Let X be a complete Segal type. Then for any map d : B → X, the induced map X/d → X/dj is an equivalence. Proof. A standard adjointness argument using the join. □ Lemma C.3. Let X be a complete Segal type. For any finite diagram d : K → X, the forgetful map p : X/d → X lifts pullbacks. In particular, if X has pullbacks, then so does X/d. Proof. Let D = (Δ⁰ + Δ⁰) ⋆ Δ⁰ be the shape for pullbacks. Consider a diagram f : D → X/d. Assume that the induced diagram pf : D → X has a limit. We will show that it extends to a limit of f. By functoriality, p : X/d → X induces p/f : (X/d)/f → X/pf. We wish to show that p/f lifts terminal objects. Note that (X/d)/f is isomorphic to X/f where f is seen as f : D ⋆ K → X. The map p/f corresponds under this to the map X/i : X/f → X/pf induced functorially from i : D → D ⋆ K. We claim that X/i is an equivalence. This follows Lemma C.2 and i ∈ J_left. Indeed, in augmented semisimplicial types, the map i : D → D ⋆ K decomposes as the Leibniz join of - 0 → Δ⁰ + Δ⁰ - 0 → Δ⁰ - Δ^{-1} → K. Maps in J_left are stable under Leibniz join with monomorphisms on either side. Thus, it will be enough to justify that the Leibniz join of 0 → Δ⁰ and Δ^{-1} → K is in J_left. This holds by saturation: for any boundary inclusion ∂Δ^n → Δ^n with n ≥ 0, the Leibniz join of 0 → Δ⁰ and ∂Δ^n → Δ^n is Λ^{n+1}_0 → Δ^n, a map in J_left. □ Recall that a marked semisimplicial type K is /finite/ if the map 0 → K lies in Cell(I) where I_m is the family of boundary inclusions (and the marking inclusion Δ¹ → Δ¹_m). We call a marked semisimplicial type K /loop-free/ if any map Δ^n → K is monic. We can give an explicit description of what it means for a finite marked semisimplicial type K to be loop-free. In the cell complex presentation 0 = K₀ → K₁ → … -> K_n = K of K with pushouts A_i --> K_i | | B_i --> K_{i+1} for all 0 ≤ i < n where A_i → B_i is in I_m, the attaching maps A_i → K_i have to be monic. With Lemmas C.1, C.1b, and C.3 in hand, we can now show a preliminary version of the claim of the section. Lemma C.4. Let X be a complete Segal type with terminal object and pullbacks. Then X has limits of loop-free finite shapes. Proof. We show by induction on m that d : K → X has a limit for K finite and loop-free and dim K < m. Note that it does not matter here if K is a marked semisimplicial type or just a semisimplicial type. The base case m = 0 is given by the terminal object in X. In the induction step, we induct on the cellular presentation of K given by finiteness. The base case is covered by the case m = 0. In the successor case, we consider a pushout ∂Δ^n --> K | | Δ^n ---> K' and a diagram d : K' → X. By loop-freeness, the top map is monic (hence so are all maps). The above pushout induces a pullback X/d -------> X/{d|Δ^n} | (1) | X/{d|K} ---> X/{d|∂Δ^n}. where all maps are right fibrations. By induction hypothesis, X has limits of d|∂Δ^n (outer induction) and d|K (inner induction). Note that X/{d|Δ^n} → X/{d|0} is an equivalence. A slice complete Segal space always has a terminal object. Thus, also d|Δ^n has a limit. We thus get terminal objects in all but the top left corner in (1). The map X/{d|∂Δ^n} → X lifts pullbacks by Lemma C.3. From this, we get products in X/{d|∂Δ^n} by Lemma C.1b. The claim then follows by Lemma C.1. □ Lemma C.4. Every finite marked semisimplicial type K has a finite loop-free replacement. Explicitly, there is loop-free K' and a cospan of maps K → • ← K' in Cell(J_{inner,m}). Proof. We take K' = N ∫ K. Here: - ∫ X denotes the marked semicategory of elements of a marked semisimplicial type X. It produces the marked semicategory as follows. The objects are the elements of X. The maps from x : X_m to y : X_n are maps f : [m] → [n] such that x = y. A map f as above is marked if: * f preserves the terminal object, * or else the induced edge y|{f(m), n} is marked. - N C denotes the marked semisimplicial nerve of a marked semicategory C. Its underlying semisimplicial type is the nerve of C. An edge is marked if the morphism in C it came from is marked. Note that ∫ K is a finite semicategory, hence N ∫ K is a finite marked semisimplicial type. One can produce a finite marked semisimplicial type Q with maps K → Q and N ∫ K → Q that both lie in Cell(J_{inner,m}). For details on this construction, see [1]: - [1] Constructive homotopy theory of marked semisimplicial sets https://arxiv.org/abs/1809.11168. Call a semicategory /loop-free/ if it does not have any loops. Since Δ_+ is loop-free, so is ∫ K. Evidently, the nerve of a loop-free marked semisimplicial category is a loop-free marked semisimplicial type. □ Now we can finally show the main claim. Lemma C.5. Let X be a complete Segal type. Assume that X has a terminal object and pullbacks. Then X has finite limits. Proof. Let d : K → X be a finite diagram. By Lemma C.4, we have a loop-free replacement of K by a finite marked semisimplicial type K', related to K by maps u : K → Q v : K' → Q in J_{inner,m}. Since X is inner fibrant, d extends to d' : Q → X such that d' u = d. Applying Lemma C.2 twice, we have X/d ≃ X/d' ≃ X/(d'v). Thus, d has a limit if d'v has a limit. But the latter is a diagram of loop-free finite shape K'. Thus, it has a limit by Lemma C.4.