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(<representing object of P>)) → 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). <fibrant type of extensions of (a, l) : Tm_{SSet_m}(Δ⁰ + K, El A) to Tm_{SSet_m}(Δ⁰ ⋆ K, El A)>.
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₁)
    = <fibrant type of extensions of … : Tm(∂Δ¹ ⋆ K ∪ Δ¹, El A) to Tm(Δ¹ ⋆ K, El A)>
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)
    = <fibrant type of extensions of a : Tm(∂Δ^n ⋆ K ∪ Δ^n, El A) to Tm(Δ^n ⋆ K, El A).
We check that given a₀ : A|0, (hom)({0} → Δ^n ⋆ K, El A) is contractible.
This is an instance of {0} → Δ^n ⋆ K ⊥ El, which holds since
- {0} → {0} ⋆ K ∈ Cell(J_left),
- {0} ⋆ K → Δ^n ⋆ K ∈ Cell(J_left) ({0} ⋆ Δ^n is in J_left and J_left is stable under - ⋆ K).

Since U is inner fibrant, both U/d → U and U/L → U are right fibrations.
Thus, to show that f is an equivalence, it suffices to show that f₀ : (U/d)₀ → (U/L)₀ is an equivalence over U₀.
That is, given A : ty, the map f₀(A) : (U/d)₀(A) → (U/L)₀(A) should be an equivalence.
This map is equivalent to
  g ∘ - : (A → S) → (A → T)
where
  S = ( (R_x : [ (l_f : d(x f)((l_{fg})_{g : [k'] → [k] non-id}))_{f : [k] → [n]}
               , (r_f : R_{x f}((u_{fg})_{g : [k'] → [k]}, (r_{fg})_{g : [k'] → [k] non-id}))_{f : [k] → [n] non-id}
               ] → ty)
        × (∀ … → is-contr (z : d(x)(…)) × R_x (…, z))
      )_{x ∈ K_n}

  T = (R : Tm(K, El A) → ty) × (is-contr (z : _) × R z)

  g : S → T
  g(R)(l) = (r_x : R_x((l_{xf})_{f : [k] → [n]}, (r_{xf})_{f : [k] → [n] non-id}))_{x ∈ K_n}.
The witness of contractibility for the image for g(R) is given by:
    (l : Tm(K, El A)) × g(R)(l)
  ≃ (l_x : …, r_x : …)_{x ∈ K_n}
  ≃ 1_{x ∈ K_n}
  ≃ 1.
It suffices to show that g is an equivalence.
(Note that the claim no longer depends on A.)
By iterated applications of Yoneda, we have
  S ≃ (l_x : d(x)((l_{xf})_{f : [k] → [n] non-id}))_{x ∈ K_n}
    = Tm(K, El A).
By a single application of Yoneda, we have
  T ≃ Tm(K, El A).
Under these equivalences, the map g corresponds to the identity on Tm(K, El A).
This can be seen by looking at what happens under these equivalences to the center of contractbility for the image of g(R) we have recalled above.
□

Second approach
---------------

Proof of Lemma B.1.
By Lemma A.5, U is a Reedy fibrant replacement of the nerve of the semicategory of small fibrant types.
We can manually construct a more efficient Reedy fibrant replacement of the first few levels:
- U₀ = ty
- U₁(A₀, A₁)
    = A₀ → A₁
- U₂( A_i for 0 ≤ i ≤ 2,
    , f_ij : A_i → A_j for 0 ≤ i < j ≤ 2
    ) = (a₀ : A₀) → f₁₂(f₀₁(a₀)) = f₀₂(a₀)
- U₃( A_i for 0 ≤ i ≤ 3
    , f_ij : A_i → A_J for 0 ≤ i < j ≤ 3
    , p_ijk : (a_i : A_i) → f_{jk}(f_{ij}(a_i)) = f_{ik}(a_i) for 0 ≤ i < j < k ≤ 3
    ) = (a₀ : A₀) → ap f₂₃ (p₀₁₂ a₀) • p₀₂₃ a₀ = p₁₂₃ (f₀₁ a₀) • p₀₁₃ a₀.
This is enough to determine if U has terminal objects and pullbacks.
We then appeal to Lemma C.5: U has finite limits already if it has terminal objects and pullbacks.

Terminal objects are easy enough.
It is just 1 : ty.
We have U₁(A₀, 1) = A₀ → 1 = 1.

For pullbacks, we let K = Δ^{0,2} ∪ Δ^{1,2} be two edges glued along their target and consider a diagram d : K → U.
The diagram d amounts to
  A B C : U₀, f : A → C, g : B → C.
We have to show that U/d has a terminal object.
We unfold
- (U/d)₀ = [ X : U₀
           , a : X → A
           , b : X → B
           , c : X → C
           , p : (x : X) → f(a(x)) = c(x)
           , q : (x : X) → g(b(x)) = c(x)
           ]
- (U/d)₁( (X₀, a₀, b₀, c₀, p₀, q₀)
        , (X₁, a₁, b₁, c₁, p₁, q₁)
        ) = [ x₀₁ : X₀ → X₁
            , a₀₁ : (x₀ : X₀) → a₁(x₀₁(x₀)) = a₀(x₀)
            , b₀₁ : (x₀ : X₀) → b₁(x₀₁(x₀)) = b₀(x₀)
            , c₀₁ : (x₀ : X₀) → c₁(x₀₁(x₀)) = c₀(x₀)
            , (x₀ : X₀) → ap f (a₀₁ x₀) • p₀ x₀ = p₁ (x₀₁ x₀) • c₀₁ x₀
            , (x₀ : X₀) → ap g (b₀₁ x₀) • q₀ x₀ = q₁ (x₀₁ x₀) • c₀₁ x₀
            ]
          ≃ (x₀ : X₀) →
              [ x₀₁ : X₁
              , a₀₁ : a₁(x₀₁) = a₀(x₀)
              , b₀₁ : b₁(x₀₁) = b₀(x₀)
              , c₀₁ : c₁(x₀₁) = c₀(x₀)
              , ap f a₀₁ • p₀ x₀ = p₁ x₀₁ • c₀₁
              , ap g b₀₁ • q₀ x₀ = q₁ x₀₁ • c₀₁
              ].
We claim that a terminal object T : (U/d)₀ is given by
  T = ( [a : A, b : B, c : C, p : f(a) = c, q : g(b) = c]
      , λ(a, b, c, p, q). a
      , λ(a, b, c, p, q). b
      , λ(a, b, c, p, q). c
      , λ(a, b, c, p, q). p
      , λ(a, b, c, p, q). q
      ).
For this, fix an element (X, a, b, c, p, q) of (U/d)₀.
We compute
  (U/d)₁((X, a, b, c, p, q), T)
≃ (x₀ : X) →
    [ x₀₁ : [a : A, b : B, c : C, p : f(a) = c, q : g(b) = c]
    , a₀₁ : (λ(a, b, c, p, q). a)(x₀₁) = a
    , b₀₁ : (λ(a, b, c, p, q). b)(x₀₁) = b
    , c₀₁ : (λ(a, b, c, p, q). c)(x₀₁) = c
    , ap f a₀₁ • p x₀ = (λ(a, b, c, p, q). p) x₀₁ • c₀₁
    , ap g b₀₁ • q x₀ = (λ(a, b, c, p, q). q) x₀₁ • c₀₁
    ]
≃ (x₀ : X) →
    [ a' : A
    , b' : B
    , c' : C
    , p' : f(a') = c'
    , q' : g(b') = c'
    , a₀₁ : a' = a
    , b₀₁ : b' = b
    , c₀₁ : c' = c
    , ap f a₀₁ • p x₀ = p' • c₀₁
    , ap g b₀₁ • q x₀ = q' • c₀₁
    ]
≃ (x₀ : X) →
    [ p' : f(a) = c
    , q' : g(b) = c
    , refl • p x₀ = p' • refl
    , refl • q x₀ = q' • refl
    ]
≃ (x₀ : X) →
    [ p' : f(a) = c
    , q' : g(b) = c
    , p x₀ = p'
    , q x₀ = q'
    ]
≃ X → 1
≃ 1.


C. Finite limits from terminal objects and pullbacks
====================================================

In this subsection, we will show that a complete Segal type is finitely complete already if it has terminal objects and pullbacks.
The following is the core lemma of this reduction.
It is also a showcase of how easy it is to reason in complete Segal types compared to quasicategories, with many arguments reduced to rewriting with singleton contractibility.

Lemma C.1.
Let
  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.