﻿Sections in complete Segal types ================================ Let X be a complete Segal type. Defining sections usually requires the notion of identity, which is not a primitive notion for complete Segal types. Instead, we define Sect(f) as the Σ-type of A' : X₀ a : X₁(A', A) equivalence/marked. s' : X₁(A', B) u : X₂(s', f, a). This is equivalent to the definition of first picking an identity on A, but much more compact once one takes the notion of edges that are equivalences as primitive (just a marked edge). The definition using an identity on A would instead need two triangles. In fact, this exactly mirrors the structure of the marked direct category that encodes the walking section (0 → 1 → 2 with 0 → 2 marked). Note that the first two components A' and a form a contractible type (by completeness). So one could equivalently define Sect(f) by taking a Π-type over (A', a) instead of a Σ-type. We can phrase this more abstractly by working in the slice complete Segal type X/A. An object (M, f) : X/A (consisting of M : X₀ and f : X₁(M, A)) is terminal exactly if f is an equivalence. Recall that X/A has a terminal object (in fact, a contractible type of such). Then a section of an object (B, f) : X₀ is just a map from the terminal object into (B, f): (A', a) : (X/A)₀ terminal (s', u) : (X/A)₁((A', a), (B, f)). Equivalence of initiality and weak initiality in slice ------------------------------------------------------ Let X be a complete Segal type X with finite limits. (Just the existence of cones over finite diagrams is enough.) Exactly as for ordinary categories with finite limits, one proves that A : X₀ is initial exactly if any terminal object of X/A is weakly initial. Lemma. For any object A : X₀, the following are equivalent: (1) A is initial, (2) for any B : X₀ and f : X₁(B, A), the type Sect(f) is contractible, (3) for any B : X₀ and f : X₁(B, A), an element of Sect(f). (All of these statements are propositions.) We can rephrase (2) and (3) using X/A: (2') for any B : (X/A)₀, Π/Σ_{1 : (X/A)₀ terminal}, (X/A)₁(1, B) is contractible, (3') for any B : (X/A)₀, Π/Σ_{1 : (X/A)₀ terminal}, an element of (X/A)₁(1, B). Proof of Lemma. For (1) ⇒ (2), we show (1) ⇒ (2') in the Π-variant. We are given A' : X₀ with an equivalence a : X₁(A', A). Initial objects are invariant under equivalence, hence since A is initial so is A'. The map X/A → X lifts initial objects, hence (A', a) : (X/A)₀ is initial. Given B : (X/A)₀, we thus have (X/A)₁((A', a), B) contractible. (2) ⇒ (3) is trivial. So the interesting part is only (3) ⇒ (1). Let B : X₀; we have to show that X₁(A, B) is contractible. We show separately that it is inhabited and propositional. For inhabitation, let P : X₀ be the product of A and B. This comes with maps π₁ : X₁(P, A) and π₂ : X₁(P, B). By (2), the map π₁ has a section (A', a, s', u). We take a Λ²₂-filler where the critical edge is the equivalence a: s : X₁(A, P) _ : X₂(a, s, s'). We take a Λ²₁-filler to get f : X₁(A, B) _ : X₂(s, π₂, f). For propositionality, let f₁, f₂ : X₁(A, B). We will show f₁ = f₂. We take the equalizer E : X₀, coming with p : X₁(E, A) q : X₁(E, B) u₁ : X₂(p, f₁, q) u₂ : X₂(p, f₂, q). By (3), we have a section of p: A' : X₀ a : X₁(A', A) equivalence s' : X₁(A', E) u : X₂(s', p, a). We introduce the Λ²₁-filler h : X₁(A', B) v : X₁(s', q, h). For i ∈ {1, 2}, we introduce the Λ³₁-filler w_i : X₂(a, f_i, h) _ : X₃(u, v, w_i, u_i). Since a is an equivalence, the type of Λ²₀-fillers f : X₁(A, B) w : X₂(a, f, h) is contractible. Both (f₁, w₁) and (f₂, w₂) are elements, hence f₁ = f₂. □