Finite completeness of complete Segal types of algebras of HIIT signatures
==========================================================================

Given a HIIT signature S, we show that the complete Segal type of algebras of S constructed previously has finite limits.

Recall the signature cwf CSS from before, used to give complete Segal type semantics.
It has:
- marked semisimplicial types as contexts,
- relative complete Segal types as types.
From this, one obtains a derived signature cwf CSS_fib.
It is the same as CSS, but has contexts replaced by "global types" (essentially types over the terminal context).
Here, this means that contexts are complete Segal types.
[By 2-out-of-3, one sees that the context extension of a complete Segal type with a relative complete Segal type is again a complete Segal type.]
The complete Segal type of algebras of S is obtained by applying the morphism
  !_{CSS_fib} : 0 → CSS_fib
in the category of signature cwfs to the context S of 0.

We now wish to show that the complete Segal type !_{CSS_fib}(S) is finitely complete.
For this, we build a signature cwf extending CSS (meaning with a forgetful morphism back to CSS).
For purposes of presentation, we will split this into two steps, producing extensions
  M₂ → M₁ → CSS
(diagram in the category of signature cwfs).

The model M₁ looks as follows.
- Contexts are marked semisimplicial types with additional types of markings on cones of finite diagrams.
- Types are relative complete Segal types with additional Reedy fibrant types of markings on relative cones of finite diagrams (over the marked cones in the context).
  Every marked relative cone is "relatively limiting".

The model M₂ extends the types of M₁ as follows.
- In addition to the above, a type also contains a selected relative cone over each
  * finite diagram in the (total space of the) type,
  * and marked cone of the diagram projected to the context.
  This selected relative cone is marked, in particular relatively limiting.

The global types in M₂ are in particular complete Segal types with finite limits.
We form the model (M₂)_fib.
Finally, the contexts are complete Segal types with finite limits.

These models are built to give rise to a commuting diagram
  (M₂)_fib ---> CSS_fib
  |             |
  V             V
  M₂ --> M₁ --> CSS
in the category of signature cwfs.
In particular !_{(M₂)_fib}(S) witnesses that the complete Segal type !_{CSS_fib}(S) of algebras of S is finitely complete.

The remainder of this note is devoted to a detailed description of the models M₁ and M₂ (and their variants with fibrant contexts).


Construction of the model M₁
============================

Category of contexts
--------------------

A context is a marked semisimplicial type with a selection of cones.
In detail, a context (X, I) consists of:
- a marked semisimplicial type X,
- for each finite diagram d : K → X and cone u : (X/d)₀, a type I(u).

A substitution is a map of marked semisimplicial types that preserves the selected cones.
In detail, a substitution σ : (X', I') → (X, I) consists of:
- a map σ : X' → X in SSet_m,
- for each finite diagram d' : K → X' and cone u' : (X'/d')₀, a map σ : I'(u') → I(σ u').

Composition of substitution is defined in the evident manner.
With this, contexts and substitutions form a category.

Remark.
Note that we can describe this category as a presheaf category.
Let D be the category Δ_{+,m} adjoined with, for every K, an object [t_K] glued in via the presheaf Δ⁰ ⋆ K (that is, the morphisms [n] → t_K are given by (Δ⁰ ⋆ K)_n).
Then the category of contexts is simply presheaves over D.
In fact, the entire signature cwf will be a refinement of the cwf of Reedy fibrations in presheaves over D.
That is, a type over a context
  (X, I) : Presheaf(D)
will be given by a Reedy fibration over (X, I) with further data.
This point of view gives you the following parts of the signature cwf for free:
- category,
- terms,
- terminal object,
- context extension.
If you are familiar with Reedy fibration models (or even just presheaf models), you can now skip those parts of the description of the model.

Presheaf of types
-----------------

Given Y : Ty_{SSet_m,rf}(X) with
- a finite diagram d : K → X,
- a lift e : Tm_{SSet_m}(K, Y d) of d to Y,
- a cone u : (X/d)₀ of d,
- and a lift v : (Y/e)₀(u) of u to Y,
call v /relatively limiting/ if Y is orthogonal against ∂Δ¹ → Δ¹ whenever 1 is sent to v.
Explicitly, this means that for
  f : Δ¹ → X/d restricting to u on 1,
  y : (Y/e)₀(f|0),
the fibrant type
  (hom)(∂Δ¹ → Δ¹, Y)(f, [y, v]) = (Y/e)₁(f, y, v)
is contractible.

Unfolding the cone adjunction, this means given
- u : Δ⁰ ⋆ K → X (restricting to d on K),
- v : Tm_{SSet_m}(Δ⁰ ⋆ K, Y u) (restricting to e on K),
we call v relatively limiting if Y has contractible fillers against
  ∂Δ¹ ⋆ K → Δ¹ ⋆ K
whenever the restriction to {1} ⋆ K is v.
Explicitly, this means that for
  f : Δ¹ ⋆ K → X restricting to d on {1} ⋆ K,
  y : Tm_{{0} ⋆ K, Y f | ({0} ⋆ K)},
the fibrant type
  (hom)(∂Δ¹ ⋆ K → Δ¹ ⋆ K, Y)(f, [y, v])
is contractible.

A type (Y, J) over (X, I) consists of:
- relative complete Segal Y : Ty_{SSet_m,rf}(X), i.e. inner fibrant and relatively complete.
  This is the same as in the complete Segal type model.
- A choice of relative finite limiting cones in Y over the selected cones in X.
  That is, given
  * a finite diagram d : K → X,
  * a cone u : (X/d)₀,
  * a lift e : Tm_{SSet_m}(K, Y d) of d to Y,
  * a lift v : (Y/e)₀(u) of u to Y,
  * and i : I(u),
  we have a fibrant type J(i, v).
  Furthermore, whenever J(i, v) is inhabited, then v is relatively limiting.

The substitution (Y', J') of a type (Y, J) along a morphism σ : (X', I') → (X, I) is defined as follows.
- Y' = Y σ : Ty_{SSet_m,rf}(X').
- The selected relative limiting cones v' for Y' are induced from the ones v for Y.
  In detail, consider
  * a finite diagram d' : K → X',
  * a cone u' : (X'/d')₀,
  * a lift e' : Tm_{SSet_m}(K, Y' d') of d' to Y',
  * a lift v' : (Y'/e')₀(u') of u' to Y' that is relatively limiting,
  * and i' : I'(u').
  Defining d = σ σ', functoriality of the cone object gives σ : X'/d' → X/d.
  We have u = σ u' : (X/d)₀.
  We have a lift e = e' : Tm_{SSet_m}(K, Y d) of d to Y.
  Note that Y'/e' = (Y/e) σ.
  We have v = v' : (Y/e)₀(u).
  We define J'(i', v') = J(i, v).
  If J'(I', v') is inhabited, then so is J(i, v).
  Then v : (Y/e)₀(u) is relatively limiting, hence so is v' : (Y'/e')₀(u').
  Explicitly, let
    f' : Δ¹ → X'/d' restricting to u'_{i'} on 1,
    y' : (Y'/e')₀(f'|0).
  Then
      (hom)(∂Δ¹ → Δ¹, Y')(f', [y', v'_{j'}])
    = (Y'/e')₁(f', y', v'_{j'})
    = (Y/e)₁(f, y, v_j)  [where f = σ f' and y = y' : (Y/e)₀(f|0)]
    = (hom)(∂Δ¹ → Δ¹, Y')(f, [y, v_j])
  is contractible.

Substitution of types is evidently functorial.

Remark.
This continues the previous remark on the relation to the Reedy model over D.
The extra data on a type (Y, J) over (X, I) in addition to Reedy fibrancy structure is as follows:
- Y is inner fibrant and relatively complete,
- if J(i, v) is inhabited, then v is relatively terminal.
Both of these constitute families of h-propositions.

Presheaf of terms
-----------------

A term t in context (X, I) of type (Y, J) consists of:
- a section t : Tm_{SSet_m}(X, Y),
- Consider
  * a finite diagram d : K → X,
  * a cone u : (X/d)₀ over d.
  Note that t induces
  * t d : Tm_{SSet_m}{K, Y d},
  * a section t : Tm_{SSet_m}(X/d, Y/(t d)),
  * t₀(u) : (Y/(t d))₀(u).
  We then require a map
    t : (i : I(u)) → J(i, t₀(u)).

Substitution of terms is evidently functorial.

Terminal context
----------------

The terminal context 1 = (X, I) has:
- X = 1 : SSet_m,
- for each finite diagram d : K → X and cone u : (X/d)₀, I(u) = 1.

Note that a section of the presheaf of types is the same as a type over 1.
This we can further simplify to the following.
A /global type/ (X, I) consists of
- a complete Segal type X,
- for each finite diagram d : K → X and cone u : (X/d)₀, a fibrant type I(u).
  If I(u) is inhabited, then u is limiting.

Any global type has an evident underlying context.
Terms of a global type A in context Γ correspond naturally to substitutions from Γ to the underlying context of A, also denoted A.

Context extension
-----------------

The extension of a context (X, I) with a type (Y, J) is defined as (X.Y, I.J) where:
- The context extension X.Y is computed as in SSet_{m,rf}.
- A finite diagram (d, e) : K → X.Y corresponds to:
  * a map d : K → X
  * with a section e : Tm_{SSet_m}(K, Y d).
  A cone (u, v) : ((X.Y)/(d, e))₀ corresponds to:
  * u : (X/d)₀,
  * v : (Y/e)₀(u).
  Under these notational identifications, we define
    (I.J)((u, v)) = (i : I(u)) × (j : J(i, v)).

We define a projection substitution
  p : (X, I).(Y, J) → (X, I)
as follows.
- On marked semisimplicial types, this p : X.Y → X is as in SSet_{m,rf}.
- Given (d, e) : K → X.Y with a cone (u, v) : ((X.Y)/(d, e))₀, we let p : (I.J)(u, v) → I(u) send (i, j) to i.

Given additionally a substitution σ : (X', I') → (X, I), we check that extensions of σ to
  τ : (X', I') → (X, I).(Y, J)
satisfying p τ = σ are in natural correspondence with terms t of (Y, J) σ.
On the first component, this correspondence is implemented as in SSet_{m,rf}, whence we denote τ = (σ, t).
Given a finite diagram d' : K → X' and a cone u' : (X'/d')₀, the data
  τ : I'(u') → (I.J)(τ u')
is constrained because its composite with the map
  p : (I.Y)(τ u') → I(p τ u')
sending (i, j) to i is prescribed to be
  σ : I'(d') → I(σ d').
This data then exactly amounts to
  t : (i' : I'(d')) → J(σ(i'), t u') = (J σ)_{i', t u'}.

Given a global type (X, I) and a type (Y, J) over (X, I), we check that the context extension (X.Y, I.J) again has the structure of a global type.
[This assumes that fibrant types have 1/Σ with η.
We can work around this by working with telescopes.]
- The extension of a complete Segal type with a relative complete Segal type is again a complete Segal type.
  This is the same as in the complete Segal type model.
- (I.J)((u, v)) = (i : I(u)) × (j : J(i, v)) is fibrant.
- Given
  * a finite diagram (d, e) : K → X.Y,
  * a cone (u, v) : ((X.Y)/(d, e))₀,
  * (i, j) : (I.J)((u, v)),
  we check that (u, v) is limiting.
  Let (x, y) : ((X.Y)/(d, e))₀.
  Then
    ((X.Y)/(d, e))₁((x, y), (u, v))
  ≃ (f : (X/d)₁(x, u)) × (Y/e)₁(f, y, v)
  ≃ (X/d)₁(x, u)
  using that v is relatively limiting since j : J(i, v)
  ≃ 1
  using that u is relatively limiting since i : I(u).

Universe
--------

The universe type should exist in any context, naturally in the context.
Recall the description of global types from the subsection on the terminal context.
It will thus suffice to define the universe as a global type as defined there.

Recall the universe (U, El) of left fibrations in SSet_{m,rf}.

The universe is the global type (U, U_I) where:
- U is the universe of left fibrations in SSet_{m,rf}.
  As before, it is a complete Segal type.
- Given a finite diagram d : K → U and a cone u : (U/d)₀, we define
    U_I(u) = [ J : (e : Tm_{SSet_m}(K, El d)) (v : (El/e)₀(u)) → ty_contr
             , w : (e : Tm_{SSet_m}(K, El d)) → is-contr (El/e)₀(u)
             ].
  That is, an element (J, w) of U_i(u) consists of
  * a small contractible fibrant type J,
  * for each section e of El d, a witness w_e that (El/e)₀(u) is contractible.
  To see that u is limiting if U_I(u) is inhabited, we refer to the lemma at the end of this subsection.

Remark.
This is a restriction of the universe of Reedy fibrant types in presheaves over D by a Reedy fibrant-proposition.
This explains the seemingly useless component J.
In the presence of 1-types/Σ-types with η in the fibrant layer, one can get away with omitting J, treating it as a constantly 1.

The type (El, El_J) over (U, U_I) is defined as follows:
- El : Ty_{SSet_m,rf}(U) is the universal left fibrant object in SSet_{m,rf}.
  In particular, it is left fibrant.
- Given
  * a finite diagram d : K → U,
  * a cone u : (U/d)₀,
  * a lift e : Tm_{SSet_m}(K, El d) of d,
  * a relative cone v : (El/e)₀(u),
  * and (J, w) : U_I(u),
  we set (El_J)((J, w), v) = J(e, v) (note that this is contractible).
  To check that v is relatively limiting, we fix
    f : Δ¹ → U/d with f|1 = u,
    y : (El/e)₀(f|0).
  Since El/e is left fibrant, the fibrant type
    (v : (El/e)₀(u)) × (El/e)₁(f, y, v)
  is contractible.
  But w_e says that (El/e)₀(u) is contractible.
  By 2-out-of-3, it follows that
    (El/e)₁(f, y, v)
  is contractible as required.

Lemma.
Let d : K → U be a finite diagram and u : (U/d)₀ a cone.
Then u is limiting exactly if for all e : Tm_{SSet_m}(K, El d), the fibrant type (El/e)₀(u) is contractible.

Proof.
Abbreviate L = Tm_{SSet_m}(K, El d).
Recall the equivalence f : U/d → U/L from the first proof of Lemma B.1.
Recall that f₀(u) = (A, B) : (U/L)₀  where
  A : U₀
  A = u|Δ⁰
and
  B : U₁(A, L)
  B(a, l) = (hom)(Δ⁰ + K → Δ⁰ ⋆ K, El)(u, (a, l)).
Since f is an equivalence, u : (U/d)₀ is terminal exactly if f₀(u) : (U/L)₀ is terminal.
This holds exactly if B is marked in U.
This means that for l : L,
  (hom)(K → Δ⁰ ⋆ K, El)(u, l)
is contractible.
But this is (El/e)₀(u).
□

Dependent products with domain in U
-----------------------------------

Given a context (X, I) with
  a substitution A : (X, I) → (U, U_I)
  a type (B, J) : Ty((X, I).(El, El_J) A),
we have to define
  Π(A, (B, J)) = (P, M) : Ty(X, I).
Following previous remarks on the relation of the current model to the Reedy fibration model over D, this is just defined as the Reedy fibrant dependent product:
- The component
    P = Π(El A, B) : Ty_{SSet_m,rf}(X) is defined as in SSet_{m,rf}.
- The component M is defined as follows.
  Consider
  * a finite diagram d : K → X,
  * a cone u : (X/d)₀,
  * a lift e : Tm_{SSet_m}(K, Π(El A, B) d) of d,
  * a lift w : (Π(El A, B)/e)₀(u) of u,
  * and i : I(u),
  Then we define
    M(i, w) = [ e_A : Tm_{SSet_m}(K, El A d)
              , v_A : ((El A)/e_A)₀(u)
              , * : El_J(A(i), v_A)
              ] → J((i, *), app(w, v_A) : (B/(d, e_A))₀(u, v_A)).
  Here, we denote the element of El_J(A(i), v_A) by * to remind the reader that this fibrant type is contractible.
  To make sense of app(w, v_A), unfold the cone adjunction and note that
    u : Δ⁰ ⋆ K → X
    w : Tm_{SSet_m}(Δ⁰ ⋆ K, Π(El A, B) u)
    v_A : Tm_{SSet_m}(Δ⁰ ⋆ K, El A u),
  hence
    app(w, v_A) : Tm_{SSet_m}(Δ⁰ ⋆ K, B (u, v_A)).
  Unfolding the cone adjunction, we can also write
    M(i, w) = [ v_A : Tm_{SSet_m}(Δ⁰ ⋆ K, El A u)
              , * : El_J(A(i), v_A)
              ] → J((i, *), app(w, v_A)).

In the situation of the M component, it remains to justify that w is relatively limiting given
  m : M(i, w).
For this, fix
  f : Δ¹ ⋆ K → X restricting to u on {1} ⋆ K,
  y : Tm_{{0} ⋆ K, Π(El A, B) f | ({0} ⋆ K)}.
We have to show that
    (hom)(∂Δ¹ ⋆ K → Δ¹ ⋆ K, Π(El A, B))(f, [y, w])
  = (hom)(∂Δ¹ ⋆ K → Δ¹ ⋆ K, Π(El A f, B f))(id, [y, w])
is contractible.

Since El is a left fibration, we have Δ⁰ → Δ⁰ ⋆ H ⊥ El for all finite H.
By 2-out-of-3, the restriction map 
  Tm_{SSet_m}(Δ⁰ ⋆ H₂, El …) → Tm_{SSet_m}(Δ⁰ ⋆ H₁, El …)
is an equivalence for any map H₁ → H₂ of finite marked simplicial types over U.

Let us define a levelwise fibrant
  A' : Ty_{SSet_m}(Δ¹ ⋆ K)
by setting
  A'_n(σ) = Tm_{SSet_m}(Δ¹ ⋆ K, El A f)  for σ ∈ (Δ¹ ⋆ K)_n having first vertex {0},
  A'_n(σ) = Tm_{SSet_m}({1} ⋆ K, El A f) for σ ∈ (Δ¹ ⋆ K)_n having first vertex {1},
  A'_n(σ) = Tm_{SSet_m}(Δ^n, El A f σ)   for σ living in K,
with evident restriction maps.
Note that A' is levelwise fibrant, but not in Reedy fibrant.
We have a canonical map c : A' → El A f.
By the previous paragraph, it is levelwise an equivalence of fibrant types.
Note that the construction of Reedy fibrant Π-types only depends on the domain being levelwise fibrant (and the codomain being Reedy fibrant).
By contravariant functoriality of Π-types in the domain, we obtain an equivalence
  Π(El A f, B f) → Π(A', B f c)
between Reedy fibrant types that restricts to an isomorphism on K.

Instead of showing that
  (hom)(∂Δ¹ ⋆ K → Δ¹ ⋆ K, Π(El A f, B f))(id, [y, w])
is contractible, we may equivalently show that
  (hom)(∂Δ¹ ⋆ K → Δ¹ ⋆ K, Π(A', B f c))(id, [c^{-1} y, c^{-1} w])
is contractible.
This is an iterated fibrant Σ-type all of whose components start with a fibrant Π-type over Tm_{SSet_m}(Δ¹ ⋆ K, El A f) (because all the simplices of Δ¹ ⋆ K missing in ∂Δ¹ ⋆ K have first vertex {0}).
By distributivity, it writes as fibrant Π-type over
  a : Tm_{SSet_m}(Δ¹ ⋆ K, El A f)
of
  (hom)(∂Δ¹ ⋆ K → Δ¹ ⋆ K, B f (id, a))(id, [app(y, a|({0} ⋆ K)), app(w, a|({1} ⋆ K))]).
We will thus be finished if we can show that
  app(w, a|({1} ⋆ K)) : Tm_{SSet_m}({1} ⋆ K, B (u, a|({1} ⋆ K))) = (B/(d, a|K))₀(u, a|({1} ⋆ K))
is relatively limiting.
But this is the case since we have
  m(a|({1} ⋆ K), *) : J((i, *), app(w, a|({1} ⋆ K)))
(finally using m : M(i, w)).

The entire construction is evidently stable under substitution in the context (X, u).

Equality in U
-------------

To model equality in U, we need to provide a substitution
  Id : U.El.El → U
together with a lift
  refl : U.El → U.El.El.(El Id)
of the diagonal over U together with an interpretation of the elimination rule.
Recall that El is Reedy fibrant.
To model the elimination rule, it thus suffices to make refl Reedy anodyne (i.e. levelwise anodyne).

Let (V, V-El) denote the universe of Reedy fibrant types in presheaves over D.
Recall that (U, U-El) is a restriction of (V, V-El) along a Reedy fibrant-proposition.
Hence both universes are univalent in the model of Reedy fibrations over D.
Call a Reedy fibrant telescope Y over X in presheaves over D /essentially in U/ if there is f : X → V with X.Y ≃ X.(El f) over X.
Since U is a Reedy fibrant-proposition over V and using univalence, given f : X → V, if V-El f is essentially in U, then f lifts through U → V.
We note some closure properties of essentially being in U:
(1) Given Reedy fibrant telescopes Y₁, Y₂ over X with X.Y₁ ≃ X.Y₂ over X, then
    Y₁ is essentially in U
  exactly if
    Y₂ is essentially in U.
  This follows from homotopy invariance.
(2) Given a Reedy fibrant telescopes Y over X and Z over X.Y such that Y is essentially in U, then
    Z is essentially in U
  exactly if
    the concatenated telescope Y.Z is essentially in U.
  This follows from 2-out-of-3 after phrasing being essentially in U as certain maps (described by weighted limits) being equivalences.

We now use the (anodyne, V)-factorization to factor the diagonal
  U.El → U.El.El
over U into
  (3) U.El → U.El.El.(V-El f) → U.El.El
where
  f : U.El.El → V
and the first factor is Reedy anodyne.
Here, we make sure to use the same Reedy factorization in the restriction to Δ_{+,m} as in the complete Segal type model.
This is possible as Δ_{+,m} → D is a sieve.
It remains to lift f through U → V.

Of course, El itself is essentially in U.
By the forward direction of (2), the telescope [El, El] is essentially U.
The first map in (3) is an equivalence.
By (1), the telescope [El, El, V-El f] is essentially in U.
By the backward direction of (2), V-El f is essentially in U.
Thus, f lifts through U → V.

Using that Δ_{+,m} → D is a sieve and that U is a Reedy fibrant-proposition over V, we modify f on Δ_{+,m} so that it agrees with the equality type in U of the complete Segal type model.
Alternatively, we can make sure to follow the same process for the construction of equality types in the complete Segal type model.
Then f will restrict to the equality types in the complete Segal type model.

Remark.
Some of the above complexity (speaking about telescopes rather than types) is only really necessary if ty is not closed under 1/Σ-types with η.
If ty is not closed under 1/Σ-types with η and Π-types with η, we need to anyway be a bit careful because we need to distinguish between ty-Reedy types (i.e. Reedy types where the fibers are types in ty) and maps into V, which are no longer in bijection.

Products of arity Tm(A) of types
--------------------------------

Let A be a fibrant type.
Consider a family of types (Y_a, J_a) for a : Tm(A) (or just a : A, as we have written countless times for fibrant types already) in context (X, I).
We define the product (P, K) together with projection substitutions
  π_a : (X, I).(P, K) → (X, I).(Y_a, J_a)
over (X, I), i.e. terms π_a of (Y_a, J_a) p_{(P, K)}, for a : A, naturally in (X, I).

By Reedy induction over t : D, we define
  (P, K)_t(x, p : (M_t (P, K))(x)) = (a : A) → (Y_a, J_a)_t(x, (M_t π_a)(p)),
  (π_a)_t(x, p) = p_{id_t}(a).
Note that these are "real" products of arity Tm(A) in presheaves over D:
- we can define a pairing constructor,
- the β-law holds,
- the η-law only holds if fibrant Π-types have η.

Let us make this definition more explicit by separating D into Δ_{+,m} and the objects for cones:
- On n : Δ_{+,m}, this becomes
    P_n(x, p : (M_n P)(x)) = (a : A) → (Y_a)_n(x, (M_n π_a)(p)),
    (π_a)_n(x, p) = p_{id_n}(a).
  In this Reedy induction, we make sure to define P as in the complete Segal type model.
  In particular, we take the same witnesses that it is inner fibrant and relatively complete.
- Consider now
    * a finite diagram d : K → X,
    * a cone u : (X/d)₀,
    * a lift e : Tm_{SSet_m}(K, P d),
    * a lift v : (P/e)₀(u),
    * and i : I(u).
  Then
    K(i, v) = (a : A) → J_a(i, π_a v)
  and
    π_a : K(i, v) → J_a(i, π_a v)
  sends k to k(a).
  Given k : K(i, v), we check that v is limiting.
  For this, fix
    f : Δ¹ → X/d with f|1 = u,
    y : (P/e)₀(f|0).
  Then
      (hom)(∂Δ¹ → Δ¹, P)(f, [y, v])
    = (P/e)₁(f, y, v)
    ≃ (a : A) → (Y_a/(π_a e))₁(f, π_a y, π_a v)
  is contractible as
    (Y_a/(π_a e))₁(f, π_a y, π_a v)
  is contractible since
    π_a k = k(a) : J_a(i, π_a v)
  witnesses that π_a v is relatively limiting.

The entire construction is evidently stable under substitution in the context (X, u).

Products of arity Tm(A) in U
----------------------------

Let A be a fibrant type.
Given family of substitutions
  f_a : (X, I) → (U, U_I)
for a : A, we define their product
  p : (X, I) → (U, U_I)
and projection substitutions
  π_a : (X, I).((El, El_J) g) → (X, I).((El, El_J) f_a)
over (X, I), i.e. terms π_a of (El, El_J) f_a p_{El g}, for a : A, naturally in (X, I).

By Reedy induction over t : D, we define
  p_t(x)(y_{t' → t non-id}) = (a : A) → (f_a)_t((y_{t' → t}(a))_{t' → t non-id})
  (π_a)_t(x, y) = y_{id_t}(a).

Let us make this definition more explicit by separating D into Δ_{+,m} and the objects for cones:
- On n : Δ_{+,m}, this becomes
    p_n(x)(y_{n' → n non-id}) = (a : A) → (f_a)_n((y_{n' → n}(a))_{n' → n non-id})
    (π_a)_n(x, y) = y_{id_n}(a).
  In this Reedy induction, we make sure to define p as in the complete Segal type model.
  In particular, we take the same witnesses for showing that we have contractible filling against {0} → Δ^n.
- Consider now
    * a finite diagram d : K → X,
    * a cone u : (X/d)₀,
    * i : I(u).
  Then
    p(i) : U_I(p u)
    p(i) = (J, w)
  where
    J : (e : Tm_{SSet_m}(K, El p d)) (v : (El/e)₀(p u)) → ty_contr
    J(e, v) = (a : A) → (f_a(i))_J((d^* π_a) e, (d^* π_a) v)
  is contractible as a product of contractible fibrant types and
    w(e) : is-contr (El/e)₀(p u)
  is derived from
      (El/e)₀(p u)
    ≃ (a : A) → (El/((d^* π_a) e))₀(f_a u)
  and (f_a(i))_w((d^* π_a) e) witnessing contractibility of (El/((d^* π_a) e))₀(f_a u).

The entire construction is evidently stable under precomposition in (X, u).


Construction of the model M₂
============================

We build a new model M₂ over the previous model M₁.
Almost everything is the same, only we add a new component to types.

A type (Y, J, v, j) in context (X, I) consists of Y and J as before.
Addtionally, given
- a finite diagram d : K → U,
- a cone u : (U/d)₀,
- i : I(u),
- a lift e : Tm_{SSet_m}(K, El d) of d,
we have
- a relative cone v(i, e) : (El/e)₀(u),
- and j(i, e) : J(i, v(u, e)).
In particular, this witnesses the existence of a relatively limiting cone over e lifting u.

Given a substitution σ : (X', I') → (X, I), the substitution (Y', J', v', j') of (Y, J, v, j) has Y' and J' as before.
For the new components, we take
- v'(i', e') = v(σ(i'), e),
- j'(i', e') = j(σ(i'), e).
To make sense of this, recall that (Y'/e')₀(u') = (Y/e')₀(u σ) and J'(i', v) = J(σ(i'), v) for all v.
This is evidently functorial.

We only have to update the interpretation for rules involving the formation of types:
- Universe,
- Dependent products with domain in U,
- Products of types of arity Tm(A).

Universe
--------

We have a new notion of global type corresponding to a section of the presheaf of types.
Before, a global type (X, I) consisted of
- a complete Segal type X,
- for each finite diagram d : K → X and cone u : (X/d)₀, a type I(u).
  If I(u) is inhabited, then u is limiting.
Now, a global type (X, I, u, i) consists additionally of, for each diagram d : K → X,
- a cone u(d) : (X/d)₀,
- and i(d) : I(u(d)).

Assume that I(u) is a contractible fibrant type equivalent to u being limiting.
Such is the case for I = U_I.
Then the new components u and i are equivalent to the existence of limiting cones over finite diagrams.
We know that U is finitely complete, hence (U, U_I) extends to a global type (U, U_I, U_u, U_i) in the new sense.

Let us extend (El, El_J) to a type (El, El_J, El_v, El_j) over (U, U_I) in the new sense.
Consider
- a finite diagram d : K → U,
- a cone u : (U/d)₀,
- i = (J, w) : U_I(u) consisting of
  * J : (e : Tm_{SSet_m}(K, El d)) (v : (El/e)₀(u)) → ty_contr
  * w : (e : Tm_{SSet_m}(K, El d)) → is-contr (El/e)₀(u)
- e : Tm_{SSet_m}(K, El d).
From w_e, we get a relative cone El_v(i, e) : (El/e)₀(u).
Since El_J(i, El_v(i, e) = J(e, El_v(i, e) is contractible, we get j(i, e) : El_J(i, El_v(i, e).

Dependent products with domain in U
-----------------------------------

Consider a context (X, I) with
  a substitution A : (X, I) → (U, U_I)
  a type (B, J, v, j) : Ty((X, I).(El, El_J) A),
We have previously constructed a type
  Π(A, (B, J)) = (P, M)
in the model M₁ over (X, I).
To lift it to a type in M₂, consider
- a finite diagram d : K → U,
- a cone u : (X/d)₀,
- i : I(u),
- a lift e : Tm_{SSet_m}(K, P d).
We wish to construct
- a relative cone w(i, e) : (P/e)₀,
- m(i, e) : M(i, w(i, e)).

We unfold the cone adjunction.
We have
  u : Δ⁰ ⋆ K → X restricting to d on K
and wish to construct
  w(i, e) : Tm_{SSet_m}(Δ⁰ ⋆ K, Π(El A u, B u)) restricting to e on K
  m(i, e) : M(i, w(i, e)).

We follow a similar strategy as before.
We define a levelwise fibrant
  A' : Ty_{SSet_m}(Δ⁰ ⋆ K)
by setting
  A'_n(σ) = Tm_{SSet_m}(Δ⁰ ⋆ K, El A u)  for σ ∈ (Δ⁰ ⋆ K)_n having first vertex Δ⁰,
  A'_n(σ) = Tm_{SSet_m}(Δ^n, El A u σ)   for σ living in K,
with evident restriction maps.
Note that A' is levelwise fibrant, but not in Reedy fibrant.
We have a canonical map c : A' → El A u that is levelwise an equivalence of fibrant types.
We obtain an equivalence
  c^* : Π(El A u, B u) → Π(A', B u c)
between Reedy fibrant types that restricts to an isomorphism on K.

Under this equivalence, note that
  M(i, w) ≃ (v_A : Tm_{SSet_m}(Δ⁰ ⋆ K, El A u)) → J((i, *), app(w, v_A))
          ≃ (v_A : Tm_{SSet_m}(Δ⁰ ⋆ K, A')) → J((i, *), app(c^* w, v_A))
where * : El_J(A(i), v_A) is the center of contraction (El_J is a family of contractible fibrant types).
Thus, it will suffice to construct
  w'(i, e) : Tm_{SSet_m}(Δ⁰ ⋆ K, Π(A', B u c)) restricting to e on K
  m'(i, e) : (v_A : Tm_{SSet_m}(Δ⁰ ⋆ K, A')) → J((i, *), app(w'(i, e), v_A)).
Note that we have crucially used that J is a fibrant family of types.
(There is a transport of J over (c^*)^{-1} c^* ≃ id occurring under the hood!)

[Note.
This was the point that caused me to switch to a fibrant notion of marking of cones for types.
I was only thinking about strict selections of cones before.
In retrospect, the fibrant notion feels like an obvious choice.
]

Given σ : (Δ⁰ ⋆ K)_n having first vertex Δ⁰ and
  v_A : Tm_{SSet_m}(Δ⁰ ⋆ K, El A u),
we have
  app(v_A|K, e) : Tm_{SSet_m}(K, B (d, v_A|K)).
From B, we get
  v((i, *), app(v_A|K, e)) : Tm_{SSet_m}(Δ⁰ ⋆ K, B (u, v_A)) restricting to app(v_A|K, e) on K
  j((i, *), app(v_A|K, e)) : J(i, v(i, app(v_A|K, e))).
We define
  w'(i, e)([n], σ)(v_A) = v((i, *), app(v_A|K, e))([n], σ)
  m'(i, e)(v_A) = j((i, *), app(v_A|K, e)).

It is straightforward to check stability of the construction under substitution in (X, I).

Products of types of arity Tm(A)
--------------------------------

Let A be a fibrant type.
Consider a family of types (Y_a, J_a, v_a, j_a) for a : A in context (X, I).
We extend the old product type (P, K) to a type (P, K, w, k).
Fix
- a finite diagram d : K → X,
- a cone u : (X/d)₀,
- i : I(u),
- e : Tm_{SSet_m}(K, P d).
Note that 
    (P/e)₀(u)
  ≅ Tm_{SSet_m}(Δ⁰ ⋆ K, P u) restricting to e on d
  ≃ (a : A) → Tm_{SSet_m}(Δ⁰ ⋆ K, Y_a u) restricting to 
  ≃ (a : A) → (Y_a/((d^* π_a) e))₀(u).
Under this equivalence, we define
- w(i, e)(a) = v_a(i, (d^* π_a) e),
- j(i, e)(a) = j_a(i, (d^* π_a) e).

The entire construction is evidently stable under substitution in the context (X, u).


Construction of the model (M₂)_fib
==================================

The global types in the model M₂ are tuples (X, I, u, i) where:
- (X, I) is a global type in M₁.
  In particular, X is a complete Segal type with a selection I of limiting cones of finite diagrams.
- For each finite diagram d : K → U, we have a cone u(d) : (X/d)₀ with i(d) : I(u(d)).
  Thus, every finite diagram has a limiting cone.
In particular, this is a complete Segal type with finite limits.

The terminal context clearly has the structure of a global type.

Given
- a global type (X, I, u, i),
- a type (Y, J, v, j) over (X, I),
the context extension (X.Y, I.J) of (X, I) with (Y, J) again has the structure (X.Y, I.J, u.v, i.j) of a global type:
- given a finite diagram (d, e) : K → X.Y, we have
  * a cone u(d) : (X/d)₀ with i(d) : I(u(d)),
  * a cone v(i(d), e) : (Y/e)₀(u(d)) with j(i(d), e) : J(i(d), v(i(d), e)).
  This gives (u(d), v(i(d), e)) : ((X.Y)/(d, e))₀ with (i(d), j(i(d), e)) : (I.J)(u(d), v(i(d), e)).

This justifies the model (M₂)_fib.