1. Generalized algebraic homotopy theories
==========================================

Definition 1.1.
A *generalized algebraic homotopy theory* (GAHT) is a generalized algebraic theory with:
* some derived sorts marked as *fibrant*,
* some of the fibrant derived sorts marked as *trivial fibrant*.
□

Equivalently, we have three kinds of sorts: ordinary sorts and (trivially) fibrant ones.
There are morphisms of derived sorts from (trivially) fibrant to ordinary and from fibrant to trivially fibrant.

In many applications, the fibrant sorts will agree with the ordinary sorts.

The ordinary sorts may not be so important.
We have a similar notion of essentially algebraic homotopy theory (EAHT) that omits them.
This could be defined as a finitely complete category with two classes of maps closed under pullback and composition.

Example 1.2.
We have the GAHT of a single fibrant sort Obj.
Many of the GAHTs below are extensions of this GAHT.
□

Example 1.3.
The GAHT of homotopy propositions has:
* fibrant sort Obj,
* given x : Obj, the sort Obj is trivially fibrant.
□

Example 1.4.
The GAHT of homotopy posets has:
* fibrant sorts Obj and Hom as usual,
* operations id, ∘,
* given x, y : Obj and f : Hom(x, y), the sort Hom(x, y) is trivially fibrant,
* given x : Obj, the telescope of y : Obj and f : Hom(x, y) and g : Hom(y, x) is trivially fibrant.
□

Example 1.5.
The GAHT of homotopy sets extends the GAHT of homotopy posets with an operation inv.
The last trivial fibrant sort can then be simplified to:
* given x : Obj, the telescope of y : Obj and f : Hom(x, y) is trivially fibrant.
□

Example 1.6.
The GAHT of strict univalent categories has:
* GAT as usual,
* a sortification HomEq(f, g) of equality for f, g : Hom(x, y),
* all sorts fibrant (including HomEq),
* given x : Obj, the telescope of
  - y : Obj
  - f : Hom(x, y)
  - g : Hom(y, x)
  - p : HomEq(g ∘ f, id)
  - q : HomEq(f ∘ g, id)
  is trivially fibrant.

One could also add the following.
But they are redundant because HomEq has been introduced as isomorphic to equality:
* given f : Hom(x, y), the telescope of g : Hom(x, y) and HomEq(f, g) is trivially,
* given p : HomEq(f, g), the sort HomEq(f, g) is trivially fibrant.
□ 

Example 1.7.
The *naive* GAHT Martin-Löf type theory has:
* GAT as usual,
* the sort of elements of a (contractible) type is (trivially) fibrant.

In particular, the sorts of contexts and substitutions are not fibrant.

This makes sense as soon as Martin-Löf type theory includes an identity type.
The example evidently extends to extensions of this with arbitrary type formers.

This homotopy theory is weaker than the one defined in the following example.
However, it seems to be the correct homotopy theory to use for homotopy canonicity of homotopy type theory.
In that application, we are interested in canonicalizing global elements of positive type formers.
We are not interested in canonicalizing global types.
□

Remark 1.8.
The *true* GAHT Martin-Löf type theory extends the previous example with the following:
* given Γ : Ctx, the sort Ty(Γ) is fibrant,
* given Γ : Ctx and A : Ty(Γ), the telescope of B : Ty(Γ) with a homotopy equivalence between A and B is trivially fibrant.

I am note sure what the best version to state the last item is.
In particular, what notion of homotopy equivalence is best in this context.

This homotopy theory corresponds to the homotopy theory of type theories defined by Kapulkin and Lumsdaine.
□

Example 1.9.
The GAHT of semi-path objects has:
* fibrant sort Obj,
* fibrant sort Hom(x, y) for x, y : Obj,
* for x : Obj, the telescope of y : Obj and f : Hom(x, y) is trivially fibrant,
* for y : Obj, the telescope of x : Obj and f : Hom(x, y) is trivially fibrant,
□

Example 1.10.
The GAHT of pseudo-path objects extends the GAHT of semi-path objects with:
* sort Refl(f) for f : Hom(x, x),
* for x : Obj, the telescope of f : Hom(x, x) and is-refl : Refl(f) is trivially fibrant.
□

Example 1.11.
The GAHT of path objects extends the GAHT of semi-path objects with:
* operation refl(x) : Hom(x, x) for x : Obj.
□


2. Cwfs with (trivial) fibrancy
===============================

GAHTs have sematics in cwfs with (trivial) fibrancy.

Definition 2.1.
A *cwf with (trivial) fibrancy* is a cwf with addditional sorts Ty_{(triv) fib}.
We have sort morphisms
  Ty_{triv fib} → Ty_fib → Ty.
All sorts have dependent sums.
The extensions of (trivially) fibrant types are called *(trivial) fibrations*.
□

Remark 2.2.
Let C be a cwf with dependent sums.
Then C forms a cwf with fibrancy in a default way.
For this, we just consider every type of C fibrant.
□

Remark 2.3.
Let C be a cwf with fibrancy.
Then C forms a cwf with trivial fibrancy in two canonical ways:
* A fibrant type in C_{split epi} is trivially fibrant if we have an element.
* A type in C_iso is trivially fibrant if it has a unique element.

We take C_{split epi} as default when regarding C as a cwf with (trivial) fibrancy.
In case C already forms a cwf with (trivial) fibrancy, we may forget the original trivially fibrant types.
We then explicitly write C_{split epi} to indicate the new choice of trivially fibrant types.
□

Remark 2.4.
Consider a cwf with (trivial) fibrancy M.
We have another cwf with (trivial) fibrancy M_{forget fib}:
* The types and trivially fibrant types are those of M.
* The fibrant types are the types of M.

This construction will play a role in the strict Rezk completion.
It will correspond to fibrant replacement in Alg_T(M_{forget fib}).
□

Definition 2.5.
Let C be a cwf with (trivial) fibrancy.
A map in C is:
* a *cofibration* if it left lifts against trivially fibrant types,
* a *trivial cofibration* if it left lifts against fibrant types.

This has an extension to *(trivially) cofibrant* objects.
In the presence of an initial object, an object is (trivially) cofibrant exactly if the induced map from the initial object is a (trivial) cofibration.
□

Remark 2.6.
In sufficiently rich cwfs with (trivial) fibrancy, we have weak factorization systems
* (cofibration, trivial fibration),
* (trivial cofibration, fibration).
This is called a *premodel structure*.
□

Example 2.7.
The category Set of sets is a cwf with (trivial) fibrancy following Remarks 2.2 and 2.3.
Concretely, every set is fibrant, and a set is trivially fibrant if we have an element.
This will recover the ordinary notions of (trivial) fibrations of models.

Note that Set forms a premodel structure:
* the cofibrations are the complemented monomorphisms (i.e., decidable inclusions),
* the trivial cofibrations are the isomorphisms.
□

Example 2.8.
Every model M of Martin-Löf type theory is a cwf with (trivial) fibrancy.
For this, we need at least dependent sums and identity types.
We regard M as a cwf with fibrancy via Remark 2.2 (that is, every type is fibrant).
The trivially fibrant types are the contractible types.

This does not quite form a premodel structure.
We only have a (trivial cofibration, fibration) factorization, and only for maps between fibrant objects.
□

Example 2.9.
The category of cubical sets is a cwf with (trivial) fibrancy as follows:
* the types are the presheaf families,
* the fibrations have composition,
* the trivial fibrations have extension.

This extends the previous example by extending the sort of types.
More generally, any cofibration-interval setting forms a cwf with (trivial) fibrancy.
Here, a *cofibration-interval setting* is a presheaf category cSet = Psh(□) with a class of cofibrations and an interval object satisfying certain axioms.
These axioms (CCHM- or ABCFHL-style) allow for the construction of a cubical model of type theory.

This induces not just a premodel structure, but an actual model structure.
The cofibrations are a subclass of levelwise complemented monomorphisms.
They are classified by a cofibration classifier and are closed under composition and finite unions and intersections.
In particular, all maps from the initial object are cofibrations.

Note that cSet_{split epi} also forms a premodel structure.
Since the map 0 → 1 is a cofibration, trivial fibrations are in particular split epic.
Therefore, the identity functor lifts to
  id : cSet → cSet_{split_epi}.

We make the following further assumptions for our development:
* The category □ has a terminal object.

As for any presheaf category, we have a string of adjunctions
  colim ⊣ const ⊣ lim
relating cSet to Set.
Since □ has a terminal object, lim is given by evaluation 1^* at 1.
Right Kan extension then provides another right adjoint 1^* ⊣ 1_*.

Which of these right adjoints lift to morphisms of cwf with (trivial) fibrancy?
For the constant functor, we have
  const : Set → cSet_{split epi}.
For the limit functor, we have
  lim : cSet_{split epi} → Set
since split epimorphisms are preserved by any functor.
By adjointness,
  const : Set → cSet_{split epi}
preserves (trivial) cofibrations as well.
It thus forms a left and right Quillen functor of premodel structures.

We can strengthen this slightly.
First note that constant presheaf families in cSet have a unique fibrancy structure.
This is a consequence of tinyness of the interval.
Therefore,
  const : Set → cSet
forms a morphism of cwfs with fibrancy.

Let cSet_{weak triv fib} denote the modified cwf with (trivial) fibrancy that has trivially fibrant types given by fibrant types with an element.
This mix of cSet and cSet_{split epi} will be of importance later.
Pullback exponential with (trivial) cofibrations sends fibrations to (trivial) fibrations.
However, pullback exponential with cofibrations does not preserve trivial fibrations.
Note that
  const : Set → cSet_{weak triv fib}.
forms a morphism of cwfs with (trivial) fibrancy.

Note that lim = 1^* preserves cofibrations.
Therefore, 1_* preserves trivial fibrations.
We hence have
  1_* : Set → cSet_{forget fib}.
This will also be of importance later.
□

Example 2.11.
Generalizing the previous example, we can consider a model of two-level type theory where:
* the outer type theory is extensional Martin-Löf type theory,
* the inner type theory is Martin-Löf type theory.
The underlying cwf is the outer model.
The (trivially) fibrant types come from the inner model.
□


3. Semantics of GAHTs
=====================

Now consider a GAHT T.
Given a cwf with (trivial) fibrancy M, we write Alg_T(M) for the collection of models of T in M.
This again forms a cwf with (trivial) fibrancy, as follows.
* The underlying (democratic) cwf is given by the cwf of models of the GAT T in M.
  We call its types *relative models* and its global types *models*.
* A relative model is fibrant if (trivially) fibrant sorts are interpreted as (trivially) fibrant types in M.
* A relative model is trivially fibrant if fibrant sorts are interpreted as trivially fibrant types in M.

This setup is suitable for democratic cwfs M.
See Remarks 3.6 and 3.7 for extensions to the general case.

Example 3.1.
Let T be the GAT with a single sort.
Then Alg_T(M) is the category of types of M.
We can make it the category of (trivially) fibrant types by marking the sort as (trivially) fibant when seeing T as a GAHT.
□

We have functorial semantics for GAHTs.
Every GAHT T is classified by a contextual cwf with (trivial) fibrancy C_T.
Fibrant models of T in M correspond to morphisms of cwfs with (trivial) fibrancy from C_T to M.

We may then identify Alg_T(M) with the category CwF_{(triv) fib}(C_T, M) of morphisms of cwfs with (trivial) fibrancy.
This clarifies that Alg_T(M) is natural in M and T.

Concretely, consider a type A ∈ Ty(Γ) in Alg_T(M), which we see as a full subcategory of [C_T, M].
The extension p_A : Γ.A → Γ is:
* a fibration if pullbacks evaluation of p_A at (trivial) fibrations of C_T gives (trivial) fibrations in M,
* a trivial fibration if pullback evaluation of p_A at fibrations of C_T gives trivial fibrations in M.
The actions here are understood to be natural with respect to base change, i.e., compatible with substitution.

Remark 3.2.
Consider GATs S and T and a cwf with dependent sums M.
We have an equivalence Alg_S(Alg_T(M)) ≃ Alg_T(Alg_S(M)) natural in S, T, M.
In fact, we have a GAT S ⊗ T, the tensor product of S and T, such that these cwfs are naturally equivalent to Alg_{S ⊗ T}(M).
The generating sorts of S ⊗ T are given by pairs of a generating sort of S and a generating sort of T.
This makes GATs into a symmetric monoidal category.
The unit is given by the GAT of a single sort.

This extends to GAHTs.
A generating sort of S ⊗ T is:
* fibrant just if each of the generating sorts in S and T are fibrant,
* trivially fibrant if additionally one of the generating sorts in S and T is trivially fibrant.

The unit is given by Example 1.2.

This can also be developed at the level of classifying cwfs with (trivial) fibrancy.
Then we work with contextual cwfs with (trivial) fibrancy. 
But I do not know how to do it nicely without contextuality.
This probably becomes easier with EAHTs.
□

Remark 3.3.
Any "translation" from a GAHT S to a GAHT T induces a morphism of cwfs with (trivial) fibrancy from Alg_T(M) to Alg_S(M).
This is clear from the functorial semantics since the translation corresponds to a model of S in C_T.
In particular, we have this for any extension T of S.
□

Remark 3.4.
A GAT T with no operations corresponds to a direct category D with finite slices.
The classifying cwf C_T is the opposite category Psh_fin(D)^op of finite presheaves over D.
Here, we mean finite in the sense of finite presentation, not the sense of being valued in finite sets.
The (fibrant) types are the finite cell complexes of latching maps.

For example:
* The GAT underlying the GAHT of a single fibrant sort has D = 1,
* The GAT underlying the GAHT of semi-path objects has D = Δ₊^{<2} = {0, 1 : [0] → [1]},
* The GAT underlying the GAHT of pseudo-path objects has
    D = Δ^{<2}_{dir repl} = Δ₊^{<2} * 1 = {0, 1 : [0] → [1], i : [0] → [0]', r : [1] → [0'], i = r 0, i = r 1}.

TODO: rename i (see later TODO).

Furthermore, the trivially fibrant sorts in these examples correspond to an extension of D to a *homotopical category*.
This consists of a chosen class of *weak equivalences* in D.
The trivially fibrant types in C_T are the finite cell complexes of the weak equivalences under Yoneda.

For example:
* For semi-path objects, we take 0, 1 as weak equivalences,
* For pseudo-path objects, we take 0, 1, r as weak equivalences.

In these examples, the closure of weak equivalences under 2-out-of-3 consists of all maps of D.
□

Remark 3.5.
In the previous remark, we may generalize from a direct category D to a Reedy category R.
This captures a larger class of GA(H)Ts.

For example, the GAHT of path objects has R = Δ^{<2} = {0, 1 : [0] → 1, r : [1] → [0], r 0 = r 1}.
We take 0, 1 as weak equivalences.
Again, the closure under 2-out-of-3 gives all maps.
We have a canonical functor D → R where D is the direct category D for pseudo-path objects.
This functor creates weak equivalences.
Moreover, it presents R as the localization of D at the unique map from [0] to [0'].
In fact, this statement remains true in the world of higher categories.
□

Remark 3.6.
In the situation of the previous two remarks, we may extend the cwf with (trivial) fibrancy of models Alg_T(M).
We generalize the underlying category to M-valued presheaves over D/R.
* The types are given by presheaf families.
* The fibrant types are the Reedy fibrant presheaf families.
* A fibrant type is trivially fibrant if its pullback application to each weak equivalence is a trivial fibration.

For example, consider the GAHT of a single fibrant sort.
The extended cwf with (trivial) fibrancy of models in M is just M.

We also make use of this for the GAHTs of (semi/pseudo-)path objects.
We write SemiPathObj(M), PseudoPathObj(M), PathObj(M) for the extended cwfs with (trivial) fibrancy of models in M.

Remark 3.3 extends to this generalization.
For example, GAHT theory of semi-path objects extends the GAHT of a single fibrant sort.
Therefore, we obtain a map SemiPathObj(M) → M of cwfs with (trivial) fibrancy natural in M.
Similarly, we have a map (Pseudo)PathObj(M) → SemiPathObj(M) natural in M.
□

Remark 3.7.
There is an extension of Alg_T(M) to a cwf structure with (trivial) fibrancy on the functor category [C_T, M].
One may then obtain Alg_T(M) by taking the contextual core.

TODO: find use of this.
□

Remark 3.8.
Suppose that M is "cubically enriched".
Then Alg_T(M) inheirts a cubical enrichment.
TODO: flesh out.
□

Remark 3.9.
Let C be a cwf with fibrancy.
We consider C_{split epi} as per Remark 2.3.


4. A special property of GAHTs
==============================

The GAHTs we are going to target with our strict Rezk completion share one important property.

Definition 4.1.
A GAHT T has *inhabited trivially fibrant sorts* if every trivially fibrant sort has a derived operation that constructs an element of it.
□

Remark 4.2.
Examples 1.2 to 1.8 have inhabited trivially fibrant sorts.
* Example 1.2 does not have any trivially fibrant sorts.
* Example 1.3 has an element of trivially fibrant Obj given as an assumption.
* Examples 1.4 to 1.6 have elements of the single trivially fibrant sort given by identities in Hom.
  For Example 1.6, this additionally uses reflexivity in HomEq.
* Example 1.7 has elements of contractible types given by their center.
* Example 1.8 has identity homotopy equivalences as elements of the additional trivially fibrant sort.

More generally, theories that admit identity- or reflexivity-like structure have a chance of having inhabited trivially fibrant sorts.
For example, the GAHT of path object from Example 1.11 has inhabited trivially fibrant sorts, while the GAHTs of semi/pseudo-path object from Examples 1.9 and 1.10 do not.
Another counterexample is the GAHT of strict univalent semi-categories.
A more interesting counterexample is the GAHT of simplicial sets.
While it has degeneracies (that behave like identities), this allows us only to fill 1-dimensional horns, not higher ones.
□

Remark 4.3.
Every GAHT T freely generates a GAHT with inhabited trivially fibrant sorts by just adding operations constructing elements of trivially fibrant sorts to the theory.
If we apply this construction to the GAHT of simplicial sets, we move from the geometric homotopy theory of simplicial sets to the equivalent homotopy theory of algebraic Kan complexes.
This seems to be a general pattern.
TODO: cite relevant article (Dmitry Ara?).
□

We can phrase Definition 4.1 in terms of the classifying cwf C_T with (trivial) fibrancy of T.
T has inhabited trivially fibrant sorts exactly if every trivially fibrant type of C_T has an element (optionally compatible with substitution and dependent sums).

Lemma 4.4.
Let T be GAHT with inhabited trivially fibrant sorts.
Consider a model X of the GAT underlying T in a cwf C.
The type X_S has an element for every trivially fibrant sort of T.
Furthermore, this is natural in C and X.

Proof.
We use functorial semantics of GAHTs to see X as a cwf morphism from C_T to C.
Every cwf morphism preserves elements of types.
□

Corollary 4.5.
Let T be GAHT with inhabited trivially fibrant sorts.
Every model of T in Set is fibrant.

Proof.
Every type of Set is fibrant.
The trivially fibrant types are precisely those with an element.
□


5. Path object functors
=======================

Definition 5.1.
Let C be a cwf with (trivial) fibrancy.
A *semi-path object functor* on C is a section P of the map SemiPathObj(C) → C from Examples 1.2 and 1.9 and Remark 3.3.
We have similar notions of *path object functor* and *pseudo-path object functor*.
□

Some notation and unfolding:

* Let Γ be an object of C.
  We write PΓ with δ₀, δ₁ : PΓ → Γ for the relation induced P.
  Note that P forms a functor and δ₀, δ₁ form natural transformations.

* Let X be a type over Γ in C.
  We write PX(x₀, x₁) for the type over [PΓ, x₀ : X δ₀, x₁ : X δ₁] induced by P.
  If X is (trivially) fibrant, then so is PX.
  Moreover, if X is fibrant, then the dependent sum of x₁ : X δ₁ and p : PX(x₀, x₁) is trivially fibrant (and similarly for the other endpoint).
  Note that the extension of this type is the pullback applications of δ₀ to the extension of X.
  All of this is stable under substitution.

* In case of a path object functor, δ₀ and δ₁ have a common section refl : Γ → P Γ.
  We also write refl_x : (PX refl)(x, x) for x : X.

* In case of a pseudopath object functor, we have an additional endofunctor R with a map r : RΓ → PΓ such that i := δ₀ r = δ₁ r : RΓ → Γ.
  We also have a family RX(f) over x : X i and f : (PX r)(x, x) that is (trivially) fibrant if X is.
  For fibrant X, the dependent sum of f : (PX r)(x i, x i) and is-refl : RX(f) is trivially fibrant.

Remark 5.2.
Assume that C is democratic.
Then every path object functor on C induces a pseudo-path object functor.
We take RX(x, f) = (PPX ⟨refl_x, refl_x⟩)(refl_x, f).

TODO: write out.
□

Remark 5.3.
Assume that C is democratic.
Assume that C forms a premodel structure as in Remark 2.6.
Suppose that C has a path object functor and the induced endofunctor on C has a left adjoint.
Then we have a *cylindrical premodel structure* [TODO: link my note].
This is a good setting for homotopy theory.
Simon Henry has generalized this to pseudo-path objects (and furthermore weakened the functoriality) and calls it a *weak model structure* [TODO: link paper].
Essentially all the usual theory of model structures works out (e.g., Quillen equivalences).

TODO.
Relate this to the notion of weak equivalence of type theories.
Does it differ on non-cofibrant objects?
□

Definition 5.4.
A GAHT T has *(semi/pseudo-)path objects* if C_T has a (semi/pseudo)-path object functor.
□

Consider a GAHT T and a cwf with (trivial) fibrancy M.
Note that Alg_T(M) can inherit a (semi/pseudo-)path object functor from either of M and C_T.

* If M has a (semi/pseudo-)path object functor, then so does Alg_T(M).
  For this, we take the functorial action of Alg_T on (Semi/Pseudo)PathObj(M) → M and commute
    Alg_T((Semi/Pseudo)PathObj(M)) ≃ (Semi/Pseudo)PathObj(Alg_T(M))
  according to Remark 3.2.

* If T has (semi/pseudo-)path objects, then Alg_T(M) has a (semi/pseudo-)path object functor.
  Here is a sketch.
  Write S for the GAHT of (semi/pseudo-)path objects.
  The section of (Semi/Pseudo)PathObj(C_T) → C_T gives a retraction of C_T → C_{S ⊗ T}.
  Applying the functorial action of Alg_{-}(M) gives a section of Alg_{S ⊗ T}(M) → Alg_T(M).
  Using Remark 3.2, this rewrites as a section of Alg_S(Alg_T(M)) → Alg_T(M), i.e. (Semi/Pseudo)PathObj(Alg_T(M)) → Alg_T(M).

TODO: clean up and make explicit.

Furthermore, this is natural in T and M.

Example 5.5 (continuing Example 1.3).
The GAHT of homotopy propositions has trivial path objects.
We simply take P(Obj)(-, -) = 1.
□

Example 5.6 (continuing Examples 1.4 and 1.5).
The GAHTs of homotopy (po)sets have path objects as follows:
* P(Obj)(a₀, a₁) = [f : Hom(a₀, a₁), g : Hom(a₁, a₀)],
* P(Hom)(-) = 1.

Reflexivity is interpreted by identities.
□

Example 5.7 (continuing Example 1.6).
The GAHT of strict univalent categories has path objects given by PC = C^I where I is the walking isomorphism.
* Obj_PX(a₀, a₁) = [f : Hom_X(a₀, a₁), g : Hom_X(a₁, a₀), p : HomEq(g ∘ f, id), q : Hom(f ∘ g, id)].
* Hom_PX(…) = commuting square expressed using HomEq.

Reflexivity is interpreted by identities.
□

All the examples above have the following in common.
The trivially fibrant sorts of T are created from the fibrant sorts via the endpoints of the path functor.

Example 5.8 (continuing Example 1.7).
The naive GAHT Martin-Löf type theory has pseudo-path objects given by the homotopical Reedy presheaf model construction.
The action of P is given by the homotopical Reedy presheaf model over {0 → 01 ← 1} (with all maps marked as weak equivalences).
The action of R is given by the homotopical Reedy presheaf model over Δ^{<2}_{dir repl}.

Concretely:
* The contexts of PX are spans: over Γ₀, Γ₁ : Ctx_X, we have a context Γ with substitution γ₀ : Subst(Γ, Γ₀) and γ₁ : Subst(Γ, Γ₁).
* The substitutions are morphisms of spans.
  Technically, this needs a sortified equality (which we can always add).
  This bit may be nicer in the EAHT setting.
* The types of PX are homotopical Reedy fibrant displayed spans.
* The elements of PX are sections of displayed spans.

This extends to homotopy type theory, including:
* function extensionality,
* univalence,
* higher inductive types such as pushouts.

TODO: there should be a second-order GAHT perspective on this.
□

Remark 5.9.
I tried to have pseudo-path objects for the true GAHT Martin-Löf type theory.
However, things got messy.
It depends on what notion of homotopy equivalence one works with.
One may have to choose a very general notion to get pseudo-path objects to work.
□

Remark 5.10.
The GAHTs of (semi/pseudo)-path objects do not have semi-path objects.
There is no suitable choice for P(Hom).
However, one can envision extensions that do have this.
For example, we can consider the GAHT of semisimplicial types.
This admits a pseudo-path object built using the geometric product of semisimplicial sets.
□


6. Generalized paths
====================

Consider a cwf with (trivial) fibrancy C.
Recall that (pseudo/semi)-path objects
  (Pseudo/Semi)PathObj(C)
in C are given by homotopical Reedy presheaves over a fully marked Reedy category R:
* for semi-path objects:
    R_{semi path} = Δ₊^{<2} = {0, 1 : [0] → [1]},
* for path objects:
    R_path = Δ^{<2} = {0, 1 : [0] → [1], r : [1] → [0], r 0 = r 1},
* for pseudo-path objects:
    R_{pseudo path} = {0, 1 : [0] → [1], i : [0] → [0]', r : [1] → [0'], i = r 0, i = r 1}.

TODO: rename i; it is used later on for elements of the interval.

The Reedy categories for semi- and pseudo-path objects are direct.
We have functors
  R_{semi path} → R_{pseudo path} → R_path.
The functors
  R_{semi path} → R_{(pseudo) path}
are sieves.
In particular, every (pseudo-)path object has an underlying semi-path object.

The sieve [0] : 1 → R_{semi path} selects the object of *objects*.
In particular, every (semi/pseudo-)path object has an underlying object.

Remark 6.1.
Let X be a pseudo-path object in C.
Assume that X(i) : X_{0'} → X₀ is split epic.
Then the semi-path object underlying X extends to a path object.
This is functorial in X together with the section of X(i).
□

For the remainder of this section, we suppose that C is a cubical setting.
This could be a cubical model as in Example 2.9.
Or it could be models of a GAHT in a cubical setting.

TODO: move discussion of cubical settings to earlier section.

We mainly use the following aspects:
* The (trivial) fibrations enjoy closure properties of right classes of weak factorization systems.
  For example, they are closed under retracts.
* C is enriched over some kind of cubical sets cSet, which includes an interval I ∈ cSet.
  We have tensors and powers for this enrichment.
* Pullback power with cofibrations preserves (trivial) fibrations.
  Pullback power with trivial cofibrations sends fibrations to trivial fibrations.
  We use the second part only for certain "monoidally generating" trivial cofibrations as in the next paragraph.

*CCHM-style* and *ABCFHL-style* fibrations are created from trivial fibrations via pullback power with a trivial cofibration i : 1 → I for certain choices of i : I.
* For CCHM-style fibrations, we use i = 0 and i = 1.
* For ABCFHL-style models, we work in the slice over I (seen in C via the tensor with the terminal object [TODO: check]) and let i : I be the generic element.

Remark 6.2.
Let R be one of R_{semi/pseudo path}.
Below, we will consider limits
  Psh_cSet(R) × Psh_C(R) --[lim]-> C
of (semi/pseudo)-path objects weighted with respect to the cubical enrichment.
In the path object case, the weighted limit uses the extensional identity types in C to form the coherence condition for reflexivity.

The weighted limit is cocontinuous in its first argument in continuous in its second argument.
For example, tensors with cubical sets in the first argument are sent to powers in C.

Note that pullback weighted limit sends:
* Reedy cofibrations in Psh_cSet(R) and Reedy (trivial) fibrations in Psh_C(R) to (trivial) fibrations in C,
* Reedy trivial cofibrations in Psh_cSet(R) and Reedy fibrations in Psh_C(R) to trivial fibrations in C.

When is a morphism of weights m : A → B in Psh_cSet(R_{semi/pseudo path}) a Reedy (trivial) cofibration?
* In the (semi/pseudo)-path cases, the Reedy category is direct.
  So Reedy (trivial) cofibrations coincide with levelwise (trivial) cofibrations.
* In the path case, we additionally need that pushout evaluation at r : [1] → [0] is a (trivial) cofibration.

As a special case, when is a weight W ∈ Psh_cSet(R_{semi/pseudo path}) Reedy cofibrant?
* In the (semi/pseudo)-path cases, every weight is cofibration.
  This is because every object of C is is cofibrant (the false proposition is a cofibration in cSet).
* In the path case, we need that W(r) : W₀ → W₁ is a cofibration.
□

Generalized paths
-----------------

Define a weight
  W ∈ Psh_cSet(R)
by right Kan extending I along the inclusion of the object of objects.
Concretely, we have:
* W₀ = I,
* W₁ = I × I, with W(0) and W(1) the two projections.

We have a map I × y[0] → W selecting the component at level [0].
This induces a map lim_W X → X₀^I natural in X.

If the diagonal I → I × I is a cofibration, then W is Reedy cofibrant and the map I × y[0] → W is a Reedy cofibration.

Definition 6.3.
Consider a (semi/pseudo)-path object X in C.
*Generalized paths* for X consist of a section of the map lim_W X → X₀^I.
□

You call this coercion.
In my note from May, I called it generalized paths, but there is probably a better name. 
Evan Cavallo replied with a refinement that also works for the CCHM universe (avoiding a use of connection) and called it a δ-contractor.
The generalized i-paths below are an abstract development of that.
With this, we can sidestep generalized paths / coercion.

Generalized i-paths
-------------------

Consider i : I in cSet. [TODO: make external]
Define another weight
  W^i ∈ Psh_C(R_{pseudo path})
as:
* W^i_0 = I,
* W^i_1 = I with W^i(0) constantly i and W^i(1) the identity,
* W^i_{0'} = 1 with W^i(r) constantly i.

TODO: is there a version of this for path objects?

Again, we have a map I × y[0] → W^i selecting the component at level [0].
If i : 1 → I is a cofibration, then W^i is Reedy cofibrant and the map I × y[0] → W^i is a Reedy cofibration.

Definition 6.4.
Consider a pseudo-path object X in C.
*Generalized i-paths* for X consist of a section of the map lim_{W^i} X → X₀^I.
□

Generalized paths and generalized i-paths
-----------------------------------------

We have categories
  PseudoPathObj_{gen. (i-)paths}}(C)
of pseudo-path objects with generalized (i-)paths.

Lemma 6.5.
Consider a pseudo-path object P in C.
Generalized paths for P induce generalized i-paths for P for all i : I.
Furthermore, this is natural in P.

Proof.
The map I × y[0] → W factors via I × y[0] → W^i.
The claim follows by functoriality of weighted limits.
□

Generalized i-paths from fibrancy
---------------------------------

In this subsection, we remove the assumption that pullback power with cofibrations preserves (trivial) fibrations in C.
This allows us to apply the results in more general situations (concretely, Alg_T(cSet_{weak triv fib})).

TODO.
Alternatively, we could work with another structure of a cwf with (trivial) fibrancy on the cwf C that we denote C'.
Every (trivially) fibrant type in C is (trivially) fibrant in C'.
This allows us to apply the results in more general situations (concretely, with C = Alg_T(cSet) the trivially fibrant types in Alg_T(cSet_{split epi})).

The following statements have versions also for generalized paths.
However, it seems to be more useful to state them at the level of generalized i-paths.
This avoids using that the diagonal I → I × I is a trivial cofibration.

Lemma 6.6.
Let i : 1 → I be a trivial cofibration.
Let p : Y → X be a Reedy fibration in Psh_C(R_{pseudo path}) at level [1].
Assume that the pullback evaluation of p at i : [0] → [0'] is a trivial fibration.
Then the pullback weighted limit of p with I × y[0] → W^i is a trivial fibration.
Furthermore, this is functorial in p.

Proof.
The weight map I × y[0] → W^i writes as a composite of:
* a cobase change of y(i) : y[0] → y[0]',
* a cobase change of the pushout tensor with i : 1 → I of the boundary ∂[1] : 2 × y[0] → y[1].
□

If p is a Reedy fibration of path objects, then the assumption on the pullback evaluation of p at i is vacuous.

Corollary 6.7.
Assume that C has a pseudo-path object functor.
Let i : 1 → I be a trivial cofibration.
Let p : Y → X be a fibration in C.

Assume that P(p) : PY → PX is a Reedy fibration at level [1].
Assume that the pullback evaluation of P(p) at i : [0] → [0'] is a trivial fibration.


Then the pullback weighted limit of P(p) : PY → PX with I × y[0] → W^i is a trivial fibration.
Furthermore, this is functorial in p.
□

The previous two relative statements have evident absolute versions (with X terminal).
For the preceding statement, this goes as follows.

Corollary 6.8.
Assume that C has a pseudo-path object functor.
Let i : 1 → I be a trivial cofibration.
Let X be a fibrant object.
Then lim_{W^i} PX → X^I is a trivial fibration.
In particular, if X^I is cofibrant, then PX has generalized i-paths.
□

Remark 6.9.
The absolute version of Lemma 6.6 is used to prove fibrancy of a universe U_fib of fibrant types from equivalence extension in cubical models.
There, we choose for Y the path object on U_fib given by homotopy equivalences (maps whose homotopy fibers are contractible).
This is Reedy fibrant at level [1] because homotopy equivalences are defined using fibrant dependent products, dependent sums, and identity types.
We obtain generalized i-paths from Corollary 6.8 since U_fib^I is cofibrant.
Then U_fib is fibrant by Corollary 6.12 using equivalence extension (glue types).
□

Transferring generalized i-paths across fibrant replacement
-----------------------------------------------------------

In this subsection, we remove the assumption that pullback power with trivial cofibrations sends fibrations in C to trivial fibrations.
This allows us to apply the results in more general situations (concretely, Alg_T(cSet_{forget fib})).

We call A → X a fibrant replacement if X is fibrant and A → X is a trivial cofibration.

Lemma 6.10.
Assume that power with I preserves trivial cofibrations in C.
Assume that C has a pseudo-path object functor P.
Let X be a fibrant replacement of A in C.
Let i : 1 → I be any map.
If PA has generalized i-paths, then so does PX.

Proof.
Consider the square
  lim_{W^i} PA ---> lim_{W^i} PX
  |                 |
  A^I ------------> X^I
given by functoriality of weighted limits.
Since X is fibrant, PX is Reedy fibrant.
Therefore, the right map is a fibration.
Since A → X is a trivial cofibration, so is the bottom map.
Hence, sections of the left map extend to sections of the right map.
□

Fibrancy from generalized (i-)paths
-----------------------------------

Lemma 6.11.
In Psh_cSet(R_{pseudo path}), we have a commuting diagram
  y[0] ----> I × y[0]
  |          |
  y[0'] ---> W^i
where:
* the top map is the pushout tensor i (×) (0 → y[0]) where i : 1 → I,
* the bottom map is a cobase change of i (×) (y(0) : y[0] → y[1]).
□

Corollary 6.12.
For a class of maps M in cSet, write D(M) for the category of arrows in PseudoPathObj_{gen i-paths}(C) created from trivial fibrations in C by pullback weighted limits with weight map in M.
We have a morphism of categories of arrows from
  D(i (×) y(0), y[0] → y[0]')
to
  D(i (×) (0 → y[0])).

Proof.
In the category of pseudo-path objects with generalized i-paths, the action of weighted limit on the weight map I × y[0] → W^i is naturally split epic.
Therefore, the action on weight map y[0] → I × y[0] is naturally a retract of the action on the composite with I × y[0] → W^i.
Pullback application is functorial, hence preserves retracts in the natural transformation argument; thus, we have the same retract for pullback weighted limits.
The claim now follows by Lemma 6.11, standard preservation properties of weighted limits, and closure of trivial fibrations in C under pullback, composition, and retract.
□

Corollary 6.13.
Assume that C has CCHM-style or ABCFHL-style fibrations.
Then evaluation at level [0]
  ev₀ : PseudoPathObj(C_{forget fib}) → C
lifts to a morphism of cwfs with (trivial) fibrancy when we restrict the source to pseudo-path objects with generalized i-paths for i = 0, 1 (CCHM) or variable i (ABCFHL).

Proof.
Preservation of trivial fibrations is immediate.
Let p : Y → X be a fibration in PseudoPathObj(C_{forget fib}).
This means that the pullback evaluations at 0, 1 : [0] → [1] and r : [0] → [0'] are trivial fibrations in C.
In particular, the pullack evaluation at 0 : [0] → [1] is a fibration in C.

Suppose p lifts to a map of path objects with generalized i-paths as in the statement.
By Corollary 6.12, the evaluation at [0] is a fibration.
Furthermore, everything is functorial.
□


7. Strict Rezk completion of models of GAHTs
============================================

We begin by recollecting some things in cubical sets.
Recall the following Quillen adjunctions from Example 2.9:
(1) colim ⊣ const between cSet_{weak triv fib} and Set,
(2) const ⊣ lim between Set and cSet_{split epi},
(3) lim ⊣ 1_* betwen cSet_{forget fib} and Set.

Let R denote the right adjoint to exponentiating with I.

Lemma 7.1.
The adjunction (-)^I ⊣ R is a Quillen endo-adjunction on cSet_{forget fib}.

Proof.
We check that exponentiation with I preserves cofibrations.
This is a reformulation of the following axiom.
Universal quantification over the interval preserves cofibrations.
□

Lemma 7.2.
The adjunction (-)^I ⊣ R is a Quillen endo-adjunction on cSet_{split epi}.

Proof.
Split epimorphisms are preserved by any functor, in particular R.
□

TODO: move the above to earlier.

For the rest of this section, we fix a GAHT T.
Recall that Alg_T forms a functor on cwfs with (trivial) fibrancy.
Using functorial semantics, the above Quillen adjunctions lift to models of T in the respective cwfs with (trivial) fibrancy.
Note that the lift of exponentiation with I is power with I.

We assume that T has pseudo-path objects.
By Section 5, this induces a shared path object functor for Alg_T(cSet_{(split epi / weak triv fib / forget fib)}).

Lemma 7.4.
Let A be cofibrant in Alg_T(cSet_{split epi}) and fibrant in Alg_T(cSet_{weak triv fib}).
Then any fibrant replacement of X in Alg_T(cSet_{forget fib}) is fibrant in Alg_T(cSet).

Proof.
Note that all the involved cwfs are cubically enriched.
By Lemma 7.2, A^I is cofibrant in Alg_T(cSet_{split epi}).
In particular, it is cofibrant in Alg_T(cSet_{weak triv fib}).

We apply Corollary 6.8 to Alg_T(cSet_{weak triv fib}).
For this, we need to check that pullback power with a trivial cofibration sends fibrations to trivial fibrations.
This follows from functorial semantics since pullback power with a trivial cofibrations sends fibrations to trivial fibrations in cSet_{weak triv fib} (see Example 2.9).
We get that PA has generalized i-paths (i = 0, 1 for CCHM; i generic for ABCHL).

We apply Lemma 6.10 to the fibrant replacement A → X in Alg_T(cSet_{forget fib}).
For this, we note that Alg_T(cSet_{forget fib}) inherits from Alg_T(cSet) closure of (trivial) fibrations under pullback power with cofibrations.
By Lemma 7.1, power with I preserves (trivial) cofibrations in Alg_T(cSet_{forget fib}).
We get that PX has generalized i-paths.

Since X is fibrant in Alg_T(cSet_{forget fib}), PX is fibrant in PseudoPathObj(Alg_T(cSet_{forget fib})).
The identity forms a map from Alg_T(cSet_{forget fib}) to Alg_T(cSet)_{forget fib}.
So PX is also fibrant in PseudoPathObj(Alg_T(cSet)_{forget fib}).
Then X is fibrant in Alg_T(cSet) by Corollary 6.13.
□

Corollary 7.5.
Let A be a fibrant and cofibrant model of T in Set.
Then we have a fibrant replacement
  Alg_T(const)(A) --[j]-> X
in Alg_T(cSet) such that the transpose
  A → Alg_T(lim)(X)
is a trivial cofibration in Alg_T(Set).

Proof.
Take a fibrant replacement
  Alg_T(const)(A) --[j]-> X
in Alg_T(cSet_{forget fib}).
By Quillen adjunction (1), Alg_T(const)(A) is fibrant in cSet_{weak triv fib}.
By Quillen adjunction (2), Alg_T(const)(A) is cofibrant in cSet_{split epi}.
Using Lemma 7.4, we thus conclude that X is fibrant in Alg_T(cSet).
Note that every trivial cofibration in Alg_T(cSet_{forget fib}) is in particular a trivial cofibration in Alg_T(cSet).
Therefore, j constitutes a fibrant replacement in Alg_T(cSet).

Since the functor 1 : 1 → □ is fully faithful, the adjunction const ⊣ lim (which is 1_! ⊣ 1^*) is coreflective.
This extends to the lifted adjunction between categories of models of T.
Therefore, the transpose of j coincides with the application of Alg_T(lim).
By Quillen adjunction (3), Alg_T(lim)(j) is a trivial cofibration in Alg_T(Set).
□

Remark 7.6.
Suppose T has inhabited trivially fibrant sorts.
Then the fibrancy assumption on A ∈ Alg_T(Set) in Corollary 7.5 is redundant by Corollary 4.5.
□

Recall that the identity forms a Quillen adjunction between cSet_{split epi} and cSet.
Therefore, the Quillen adjunction (2) also forms a Quillen adjunction between Set and cSet.
In terms of weak model structures, the previous statement then implies the following.

Corollary 7.7.
The Quillen adjunction Alg_T(const) ⊣ Alg_T(lim) between Alg_T(Set) and Alg_T(cSet) is a Quillen coreflection.

Proof.
By homotopy invariance, the fibrancy assumption in Corollary 7.5 is redundant.
(In general, we may first take a fibrant replacement of A in Set.)
□

That is, the homotopy theory of models of T in Set embeds coreflectively in the homotopy theory of models of T in cSet.


8. Application: homotopy canonicity for HoTT
============================================

We consider the naive GAHT T_HoTT of Martin-Löf type theory from Example 1.7 extended with:
* function extensionality,
* univalence,
* higher inductive types such as pushouts.

By Example 5.8, this has pseudo-path objects.
By Remark 4.2, it has inhabited trivially fibrant sorts.

Recall the following.

Lemma 8.1 (gluing for Martin-Löf type theory).
Let C and D be models of Martin-Löf type theory.
Let F : C → D be a weak morphism of cwfs.
Then the projection F ↓ D → C extends to a fibration Glue(F) → C of models.
□

This extends as follows.

Lemma 8.2 (gluing for HoTT).
Let C and D be models of T_HoTT in Set.
We consider C and D as cwfs with (trivial) fibrancy as per Example 2.8.
Let F : C → D be a weak morphism of cwfs with (trivial) fibrancy.
Then Glue(F) → C from Lemma 8.1 extends to a fibration of models of T_HoTT.

Proof.
I checked this a long time ago.
See also Shulman's article on inverse diagrams.
□

Definition 8.3.
A model of T_HoTT in Set satisfies *homotopy canonicity* if every closed boolean is homotopic to a canonical boolean.
That is, given v ∈ Tm(1, Bool), we have El(1, Id(v, true)) or El(1, Id(v, false)).
□

Lemma 8.4.
Homotopy canonicity is invariant under homotopy equivalences of models of T_HoTT.
□

Lemma 8.5 (homotopy canonicity).
The initial model of T_HoTT in Set satisfies homotopy canonicity.

Proof.
Let C be the initial model.
In particular, it is cofibrant.
By Corollary 7.5 with Remark 7.6, we obtain fibrant C' ∈ Alg_T(cSet) together with a trivial cofibration j : C → Alg_T(lim)(C').
Every fibration with base C has a section, hence so does every fibration with base Alg_T(lim)(C').
Since j goes between fibrant-cofibrant objects, it is a homotopy equivalence.
By Lemma 8.4, it suffices to show that Alg_T(lim)(C') satisfies homotopy canonicity.

Externally, since C' is fibrant, the cubical global sections functor lifts to a weak morphism
  Alg_T(lim)(C') --[F]-> cSet_fib
of cwfs with (trivial) fibrancy.
Applying Lemma 8.2, this induces a fibration Glue(F) → Alg_T(lim)(C').
By the previous paragraph, this has a section.
Note that the booleans are a fibrant cubical set.
Applying the section to some v ∈ El(1, Bool), we get a path in C' in El(1, Bool) from v to true or false.
Since C' is fibrant, we may transport across this path to construct an element of El(1, Id(v, true)) or El(1, Id(v, false)).
□