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₂.
□