Signature cwf of Reedy fibrations
=================================

We describe briefly a generic model construction that essentially generalizes the signature cwfs of algebras, morphisms, displayed algebras, and displayed algebra sections.
Most of this is an instance of Shulman's work on inverse diagram models of type theory.

Let (D, W) be a finite marked direct category with finite slices.
We will build the /canonical signature cwf over (D, W)/ from the cwf of Reedy fibration in presheaves over D.
In particular, we have:
* The category of contexts is presheaves over D.
* Types are Reedy fibrant types in presheaves over D.
  That is, a type over X is a Reedy fibrant presheaf Y over ∫ X.
  Substitution is given by precomposition.
* We have a forgetful map from the above types to types of the presheaf model.
  This induces the rest of the basic cwf structure.
Note that global types are precisely Reedy fibrant presheaves over D.

It remains to describe the remaining signature cwf features.
The adjective "canonical" is not supposed to say that there is a natural way of fixing these, but rather that we make a particular choice that for the purpose of this note we call canonical so that we can compare other choices to it.

Universe
--------

We describe the universe U as a global type.
It is the classifier for Reedy ty-types (where ty is a fibrant universe of fibrant types) that respect the marking W.
This is a restriction of Shulman's universe (V, V-El) of small Reedy fibrant types via a Reedy fibrant-proposition.
Explicitly, we define
  IsHomotopical : Ty(V)
  IsHomotopical(A, X, _ : (M_A IsHomotopical)(X|∂A)) =
    <product over w : B → A in W of>
      is-equiv (hom)(w : yB → yA, X).
Unfolded, the map
  (hom)(w : yB → yA, X) = hom(yA, X) → hom(yB, X)
takes
  (x_f : X(f)((X(f f'))_{f' : A'' → A'}))_{f : A' → A}
and returns
  (y_g : X(f)((X(f f'))_{g' : B'' → B'}))_{g : B' → B}
given by y_g = x_{wg}.
Then the universe U is defined as
  (X : U) × IsHomotopical(X).
Recall that Shulman's universe is itself Reedy fibrant, hence this is a type.

The type El over U is just obtained by restricting V-El.
That is, El is the substitution of V-El along the projection U → V.

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

Shulman describes how dependent products work in the Reedy fibration model.
So, our cwf already has dependent products of types.
In particular, we have dependent products with domain in U.

Equality of types in U
----------------------

Types classified by U satisfy two cases of 2-out-of-3 among Reedy ty-types.
Let
  X be a presheaf over D,
  Y a Reedy ty-type over X (i.e. Y : X → V),
  Z a Reedy ty-type over Y (i.e. Z : X.Y → V).
Then also Σ_Y Z is a Reedy ty-type over X.
We suggestively denote it Y.Z (alluding to how the treatment proceeds in the absense of 1/Σ-types with η for fibrant types.)
Assume that Y is classified by U (i.e. Y : X → V lifts through U → V).
Then Z is classified by U exactly if Y.Z is classified by U.
That is, Z : X.Y → V lifts through U → V exactly if Y.Z : X → V lifts through U → V).
This follows from unfolding the definition of V and using 2-out-of-3.

Shulman explained how identity types work in the Reedy fibration model.
This descends to Reed ty-types, i.e. V-types have equality types.
Using the above pasting properties of types classified by U, equality types of U-types (which are a priori V-types) are again U-types.
See the previous notes for more detailed unfoldings of this argument.

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

Let A be a fibrant type.
Reedy fibrant types are closed under products of families indexed by A.
See the previous notes for unfoldings of this.

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

Let A : ty be a small fibrant type.
Reedy ty-types are closed under products of families indexed by A.
This is an instance of the previous subsection, but with fibrant types replaced by ty-types.
This shows that V has products of arity A.
It remains to check that the product lifts to U if the given A-indexed family lifts to U.
This comes down to closure of equivalences under A-indexed products in fibrant types.


Examples
========

We describe the choices of (D, W) giving essentially the signature cwfs described in the Ambrus-Andras paper:
- signature cwf of algebras:
    (D, W) = ({0}, ∅),
- signature cwf of morphisms:
    (D, W) = ({s, t : 0 → 1}, {s}),
- signature cwf of displayed algebras:
    (D, W) = ({0 → 1}, ∅),
- signature cwf of displayed algebra sections:
    (D, W) = ({0 → 1 → 2}, {0 → 2}).

The models are not exactly the same, only up to some notion of equivalence (to be investigated later).
This is for the following reasons.
- The definition of identity types in U is canonical only up to equivalence, not up to isomorphism.
  Different choices give non-isomorphic models.
- The definition of U is different, albeit equivalent.
  Again, this gives non-isomorphic models.
  - For algebras and displayed algebras, it is the same (because W = ∅).
  - For morphisms, it is different.
    Here, we have
      U₀ = ty
      U₁(X₀, X₁) = (X₀₁ : X₀ × X₁ → ty) × is-equiv ([x₀ : X₀, x₁ : X₁, x₀₁ : X₀₁(x₀, x₁)] → X₀).
    Since all maps in D are mono, we could just as well take
      U₁(X₀, X₁) = (X₀₁ : X₀ × X₁ → ty) × ((x₀ : X₀) → is-contr [x₁ : X₁, x₀₁ : X₀₁(x₀, x₁)]).
    Both choices denote functional relations.
    On the other hand, in their article, they take
      U₀ = ty
      U₁(X₀, X₁) = X₀ → X₁,
    i.e. functions.
    All choices are clearly equivalent (using Yoneda).
  - For displayed algebra sections, it is also different.
    Here, we have
      U₀ = ty
      U₁(X₀) = X₀ → ty
      U₁(X₀, X₁) = (X₂ : [x₀ : X₀, x₁ : X₁(x₀)] → ty) × is-equiv ([x₀ : X₀, x₁ : X₁(x₀), x₂ : X₂(x₀, x₁)] → X₀).
    Since all maps in D are mono, we could just as well take
      U₁(X₀, X₁) = (X₂ : [x₀ : X₀, x₁ : X₁(x₀)] → ty) × ((x₀ : X₀) → is-contr [x₁ : X₁, x₂ : X₂(x₀, x₁)]).
    On the other hand, in their article, they take
      U₀ = ty
      U₁(X₀) = X₀ → ty
      U₁(X₀, X₁) = (x₀ : X₀) → X₁(x₀).
    All choices are clearly equivalent (using Yoneda).

The semisimplicial structure of the complete Segal type model (forgetting about types of markings in semisimplicial types, inner fibrancy, and relative completeness) is the following instance:
  (D, W) = (Δ_+, {f : [k] → [n] | f(0) = 0}).

For the marked semisimplicial structure of the complete Segal type model (forgetting about inner fibrancy and relative completeness, it is:
  (D, W) = (Δ_{+,m}, {f : [k] → [n] | f(0) = 0 or 0 → f(0) marked in [n]}).
To understand W here, we treat Δ_{+,m} as a full subcategory of marked semi-posets (no reflexivity).
Every object has discrete marking except for [1m], which is fully marked.


Equivalence between variations
==============================

As noted above, non-isomorphic, but equivalent choices for certain constructs in the canonical signature cwf over (D, W) yield different model.
We will show that the choices do not matter, giving rise to an equivalence of signature cwfs.
This is needed to precisely e.g. relate notions of displayed algebra sections coming from our canonical signature cwfs to the concrete ones given in the paper by Ambrus-Andras.

In this section, given a cwf C, we write C_fib for the contextual core of C.
Note that in earlier sections we have already written C_fib for the more specialized cwf obtained when C admits a nice notion of global type with dependent sums (with η).
In general (for example in the absence of η for fibrant 1/Σ), the current notion of C_fib is the appropriate one.
Note that (-)_fib is an endofunctor on signature cwfs.

We introduce some notion of equivalence of signature cwf to work with.
This is not really needed for the purposes mentioned above.
But it allows us to strengthen the statements of some lemmas.
It will probably also come up later at some point anyway.
We use the notion of equivalence of cwfs of Lumsdaine-Kapulkin and Isaev.

A morphism p : D → C of signature cwfs is a /trivial fibration/ if:
- it has /type lifting/: for
    X_D ∈ D,
    Y_C ∈ Ty(p X_D),
  there is Y_D ∈ Ty(X_D) such that p Y_D = Y_C,
- it has /term lifting/: for
    X_D ∈ D,
    Y_D ∈ Ty(X_D),
    t_C ∈ Tm(p X_D, p Y_D),
  there is t_D ∈ Tm(X_D, Y_D) such that p t_D = t_b.

A morphism p : D → C of signature cwfs is a /trivial fibration on fibrants/ if the induced morphism p_fib : D_fib → C_fib is a trivial fibration.

Lemma 1.
Let p : D → C be a morphism of cwfs.
Assume that:
- C and D have identity types and that p preserves equivalences (equivalently, contractible types).
- C and D have fibrant global section functors on fibrants.
  That is, for X ∈ C_fib, hom_C(1, X) is fibrant, and similarly for D.
- Assume that p is a trivial fibration on fibrants.
Then p_fib : D_fib → C_fib induces an equivalence for X ∈ D_fib between hom_C(1, X) and hom_D(1, p X).

Proof.
Term lifting gives the inverse map and one inverse law.
For the other inverse law, use term lifting for the identity type of X in C.
Since p preserves contractible types, it preserves identity types up to equivalence.
□

An /equivalence/ between signature cwfs C₁ and C₂ is a signature cwf E with maps E → C₁ and E → C₂ that are trivial fibrations on fibrants.
[One could also additionally demand that E → C₁ × C₂ is a fibration (defined appropriately), making E Reedy fibrant.
All the equivalences we construct will be of this form.]

Definition 2.
Let (D, W) be a marked direct category with finite slices.
An /alternative signature cwf over (D, W)/ is any signature cwf C as follows.
In the following, type formers of C are always denoted with subscript C.
We also make use of the canonical signature cwf over (D, W).
We note that this signature cwf has unconstrained 1/Σ/Π-types.
Its type formers are denoted without subscript.
- The basic cwf structure is the category of presheaves over D with Reedy fibrations as types.
  Here, we allow for an arbitrary ordering of the slices of D.
- The following type/term formers satisfy universal properties.
  * Universe U_C.
    The universal type family El_C : Ty(1.U_C) is Reedy-ty and homotopical with respect to W.
    The induced classifying map U_C → U is an equivalene.
  * Dependent product with domain U_C.
    Given
      Γ ∈ C,
      X : Tm(Γ, U_C),
      Y : Ty(Γ.El_C(X)),
      Z : Ty(Γ),
    then the map from
      Tm(Γ, Z → Π_C(X, Y))
    to
      Tm(Γ.X, Z p → Y)
    given by application is an equivalence.
  * Tm(A)-indexed products of types (for a fibrant type A)
    Given
      Γ ∈ C,
      X : A → Ty(Γ),
    then the map from
      Tm(Γ, Π_A X)
    to
      (a : A) → Tm(Γ, Tm(Γ, X(a)))
    given by application is an equivalence.
  * Tm(A)-indexed products in U_C (for a fibrant type A).
    Given
      Γ ∈ Cm
      X : A → Tm(Γ, U_C),
    then the map from
      Tm(Γ, El_C(Π_A X))
    to
      (a : A) → Tm(Γ, El_C(X(a)))
    given by application is an equivalence.

Note that we add a case for equality types in U in the above definition.
The notion of signature cwf already includes sufficient rules for those to characterize them up to equivalence.

Lemma 3.
Let (D, W) be a marked direct category with finite slices.
Let C₀ and C₁ be alternative signature cwfs over (D, W).
Then there is an equivalence E of C₀ and C₁ as follows.
- The basic cwf structure is given by homotopical Reedy fibrations in presheaves over
    (D_new, W_{new,types}) = {0 → 01 ← 1, All} × (D, ∅).
  Here, the orderings on the finite slices are chosen so as to be compatible with those of C₀ on 0 and C₁ on 1.
  The morphisms E → C₀ and E → C₁ are given by projection to 0 and 1, respectively.
Furthermore, given:
- a sieve D' → D,
- an equivalence E' of the above form between the restrictions of C₀ and C₁ to D',
then the equivalence E may be chosen so that it is compatible with E':
- The orderings of the finite slices of D_new are chosen compatible with those of its sieve {0 → 01 ← 1} × D'.
  The induced restriction morphism E' → E of cwfs lifts to a trivial fibration of signature cwfs.

Proof.
Define
  (C_new, W_new) = {0 → 01 ← 1, All} × (D, W).

We describe the type formers in E.

Universe U
----------

The universe U_E is interpreted as U_{C₀}, U_{C₁}, U_{E'} on {0 → 01 ← 1} × D' ∪ {0, 1} × D.
On the remaining stages, it is interpreted as in the canonical signature cwf over (D_new, W_new).
It remains to check that U is homotopical with respect to (0, I) → (01, I) in W_{new,types} (the case 1 → 01 is dual).

By induction, one proves that a Reedy fibration Y over X is homotopical with respect to W_{new,types} exactly if
  (hom)((0 → 01) (□) (yI → ∂I), Y)
  (hom)((1 → 01) (□) (yI → ∂I), Y)
are contractible for any I ∈ C.
Here,
  □ : Presheaf(M) × Presheaf(N) → Presheaf(M × N)
denotes the box product and (□) denotes its Leibniz construction.
We will use this as the default characterization for such Reedy fibrations from now on.

Let us prove the claim at stage I for a map (0, I) → (01, I) (the case 1 → 01 is dual).
We are given
  X_(k,f) : U(k, I')(…) for k ∈ {0, 01, 1} and f : I' → non-id,
  X_(0,id_I) : U(0, I)(…).
We have to show that the dependent sum of
  X_(1,id_I) : U(1, I)(…),
  X_(01,id_I) : U(01, I)(…)
is contractible.

Let V denote the universe of Reedy-ty types.
By assumption, we have a map
  U(1, I)(…) → V(1, I)(…)
that becomes an equivalence when the target is restricted to
  X_(1,id_I) : V(1, I)(…)
that are homotopical with respect to (1, I') → (1, I) in W.

Recall that U_E classifies Reedy fibrations that are in particular homotopical with respect to W_{new,types}.
By 2-out-of-3, a Reedy fibration is homotopical with respect to W_new already if it is homotopical with respect to
  W_{new,types} ∪ {0, 1} × W.
Thus, U(01, I)(…) consists of (up to equivalence) of fibrant types X_(01,id_I) over the relevant matching object such that
  (hom)((0 → 01) (□) (yI → ∂I), X)(id, x₀)
  (hom)((1 → 01) (□) (yI → ∂I), X)(id, x₁)
are contractible for all x₀ and x₁, respectively.

We now rewrite (up to equivalence) the dependent sum
  X_(1,id_I) : U(1, I)(…),
  X_(01,id_I) : U(01, I)(…)
to the dependent sum
  X_(1,id_I) : V(1, I)(…),
  X_(1,id_I) homotopical with respect to I' → I in W,
  X_(01,id_I) : V(01, I)(…),
  (hom)((0 → 01) (□) (yI → ∂I), X)(id, x₀) contractible ∀x₀,
  (hom)((1 → 01) (□) (yI → ∂I), X)(id, x₁) contractible ∀x₁.
In turn, this is equivalent to the dependent sum
  X_(1,id_I) : V(1, I)(…),
  X_(01,id_I) : V(01, I)(…),
  (hom)((0 → 01) (□) (yI → ∂I), X)(id, x₀) contractible ∀x₀,
  (hom)((1 → 01) (□) (yI → ∂I), X)(id, x₁) contractible ∀x₁.
For this, note that the homotopicality condition of X_(1,id_I) with respect to (1, I') → (1, I) for I' → I in W follows from that of X_(0,id_I) with respect to (0, I') → (1, I) by 2-out-of-3 in a diagram of weighted limits of X induced by the following diagram of weights:
  y(0) □ yI' --> y(01) □ yI' <-- y(1) □ yI'
       |               |              |
  y(0) □ yI ---> y(01) □ yI <--- y(1) □ yI.
Here, all horizontal maps and the left vertical maps get sent to equivalences.
Now we rewrite
    V(1, I)(…),
  = hom(y(0) □ ∂I, X)(•) → ty
  ≃ hom(y(01) □ ∂I, X)(•) → ty
using that
  hom(y(01) □ ∂I, X)(•) → hom(y(0) □ ∂I, X)(•)
is a trivial fibration (here and below, • denotes the respective canonical map from the domain of the hom to the target of X, which is the domain of the Leibniz box product of y(0) → y(01) with ∂I → yI).
With this, the dependent sum
  X_(1,id_I) : V(1, I)(…),
  X_(01,id_I) : V(01, I)(…),
  (hom)((0 → 01) (□) (yI → ∂I), X)(id, x₀) contractible ∀x₀,
  (hom)((1 → 01) (□) (yI → ∂I), X)(id, x₁) contractible ∀x₁.
rewrites as
  X_(1,id_I) : hom(y(01) □ ∂I, X)(•) → ty,
  X_(01,id_I) : hom(y(0) □ I ∪ y(01) □ ∂I ∪ y(1) □ I, X)(id) → ty,
  (hom)((0 → 01) (□) (yI → ∂I), X)(id, x₀) contractible ∀x₀,
  (hom)((1 → 01) (□) (yI → ∂I), X)(id, x₁) contractible ∀x₁.
This is the product over
  x : hom(y(01) □ ∂I, X)(•)
of
  X_(1,id_I) : ty,
  X_(01,id_I) : X_(0,id_I)(x|…) × X_(1,id_I) → ty,
  [x₁ : X_(1,id_I), x₀₁ : X_(01,id_I)(x₀, x₁)] contractible ∀x₀,
  [x₀ : X_(0,id_I)(…), x₀₁ : X_(01,id_I)(x₀, x₁)] contractible ∀x₁.
Using univalence, the latter is a presentation of
  X_(1,id_I) : ty,
  X_(01,id_I) : X_(0,id_I)(…) ≃ X_(1,id_I),
hence contractible.

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

Let X be a context, A : X → U_E, and B : Ty(X.(El A)).
The dependent product Π_E(A, B) : Ty(X) is interpreted as the given one on {0 → 01 ← 1} × D' ∪ {0, 1} × D.
On the remaining stages, it is interpreted as in the canonical signature cwf over (D_new, W_new).
It remains to check that Π_E(A, B) is homotopical with respect to W_{new,types}.

We take into account the general remarks from the case of the universe.
Let us prove the claim at stage I for a map (0, I) → (01, I) (the case 1 → 01 is dual).
We are given
- x : X(01, I),
- e_(k,f) : Π_E(A, B)(x|(k,f))(…) for
  * k ∈ {0, 01, 1} and f : I' → non-id,
  * k = 0 and f = id_I.
We have to show that the dependent sum of
  e_(1,id_I) : Π_E(A, B)(x|(1,id_I))(…)
  e_(01,id_I) : Π_E(A, B)(x|(01,id_I))(…)
is contractible.

The strategy of the proof is the same as in the verification of dependent products in the complete Segal type model.
We wish to reduce to homotopicality of B.
For this, we have to show that the unfolded dependent products
  Π_E(A, B)(x|(1,id_I))(…),
  Π_E(A, B)(x|(01,id_I))(…)
have up to equivalence the same domain.
More precisely, we need to show that the projection map
  hom(y(01) □ y(I), El)(A ∘ x) → hom(y(1) □ y(I), El)(A ∘ x ∘ …).
is an equivalence.
But this is just homotopicality of El with respect to (1, I) → (01, I).

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

Again, we have now choice on the stages {0 → 01 ← 1} × D' ∪ {0, 1} × D.
On the new stages, we follow the definition of (D_new, W_new).
A pasting argument of Reedy-U types as before shows that this gives an equality type in U_E.
The new equality type satisfies the β-law strictly if the original ones in C₀, C₁, D' do.

Tm(A)-indexed products of types
-------------------------------

We have no choice on the stages {0 → 01 ← 1} × D' ∪ {0, 1} × D.
On the new stages, we follow the definition of (D_new, W_new).
Homotopicality with respect to W_{new,types} follows from the universal property of Tm(A)-indexed products in C₀ and C₁.

Tm(A)-indexed products in U
---------------------------

We have no choice on the stages {0 → 01 ← 1} × D' ∪ {0, 1} × D.
On the new stages, we follow the definition of (D_new, W_new).
A pasting argument of Reedy-U types as before shows that this is in U_E.
This uses the universal property of Tm(A)-indexed products in C₀ and C₁.

Remainder of proof
------------------

By construction, the sieves
  {0 → 01 ← 1} × D' → D_new
  {0} × D → D_new
  {1} × D → D_new,
induce restriction maps
  E → E'
  E → C₀
  E → C₁
of signature cwfs.

We now check that E is indeed equivalence between C₀ and C₁.
We only check that p₀ : E → C₀ is a trivial fibration between fibrants.
The case of p₁ : E → C₁ is dual.

Let us check that p₀ : E_fib → (C₀)_fib has type lifting.
Let X_E ∈ E_fib and A_{C₀} : Ty_{C₀}(p₀ X_E).
We need to construct A_E : Ty(X_E) such that p A_E = A_{C₀}.
We will treat X_E as a Reedy fibrant presheaf over D_new.
[This is possible only with fibrant 1/Σ-types with η.
In their absence, one needs to reason explicitly about telescopes.]
This corresponds to a span
  X₀ <-- X₀₁ --> X₁
of presheaves over D where A_{C₀} corresponds to A₀ : Ty_{C₀}(X₀).
We pull back A₀ along X₀ → X₀₁, obtaining A₀₁ : Ty_rf(X₀₁).
We postcompose (Σ-type, left adjoint to pullback) A₀₁ along X₀₁ → X₁, obtaining A₁ : Ty_{C₁}(X₁).
Together, this gives a diagram
  X₀.A₀ <-- X₀₁.A₀₁ --> X₁.A₁
  |         |           |
  X₀ <----- X₀₁ ------> X₁
in presheaves over D where the left square is a pullback.
All objects here are fibrant and the horizontal maps are equivalences.
We can see the diagram as A' : Ty(X) (not Reedy fibrant) in presheaves over D.
We construct A as the Reedy fibrant replacement of A' relative to the sieve {0} × D → D_new (the restriction to {0} × D is A₀ = A_{C₀}, which is already Reedy fibrant).
It remains to check that A is homotopical.
Since X is homotopical, this is equivalent to X.A being homotopical.
This holds since X.A is levelwise weakly equivalent to X.A' and X.A' is homotopical.

Let us check that p₀ : E_fib → (C₀)_fib has term lifting.
Let
  X_E ∈ E_fib
  A_E : Ty_E(X_E)
  t_{C₀} : Tm_{C₀}(X_E, p₀ A_E).
We need to construct t_E : Tm(X_E, A_E) such that p t_E = t_{C₀}.
As before, X_E and A_E corresponds to a Reedy fibrant diagram
  X₀.A₀ <-- X₀₁.A₀₁ --> X₁.A₁
  |         |           |
  X₀ <----- X₀₁ ------> X₁
in presheaves over D where all horizontal maps are equivalences.
We are given a section s₀ of X₀.A₀ → X₀ and wish to construct compatible sections of the other two vertical maps.
Because the horizontal maps are equivalences, we certainly obtain such sections s₁ and s₀₁ that are compatible up to homotopy.
We then use Reedy fibrancy of X₀₁.A₀₁ over the rest of the diagram to change s₀₁ to a homotopic section s₀₁' that is strictly compatible with s₀ and s₁.
□

We instantiate Lemma 3 to the cases of (D, W) considered earlier.
Let S be a HIIT signature, i.e. context of the initial signature cwf.
Then the interpretation of S in E provides us with equivalences of each level of the interpretation of S in C₀ with the corresponding level of the interpretation of S in C₁, fibred over the equivalences of earlier levels.
In particular, we obtain the following instances, assuming that all notions of algebras/algebra morphisms/etc. are defined using alternative signature cwfs (one instance, in particular, are the ones in the Ambrus-Andras paper).
- Any two notions of algebras for S are equivalent.
- Any two notions of algebra morphisms for S are equivalent over any given equivalence (of the form of Lemma 3) of the underlying notions of algebras.
- Any two notions of displayed algebras for S are equivalent over any given equivalence (of the form of Lemma 3) of the underlying notions of algebras.
- Any two notions of displayed algebra sections for S are equivalent over any given equivalences (of the form of Lemma 3) of the underlying notions of algebras and algebra morphisms.

From now on, we will simply work with
  algebras/algebra morphisms/displayed algebras/displayed algebra sections
as defined from the canonical signature cwf over the relevant marked direct category.
The above justifies that this fits with the notions in the Ambrus-Andras paper.