The main focus of this paper is the conservativity of the extension
$\mathcal{T}\to\mathcal{T}_{E}$, but we also need a way to prove that
$\mathcal{T}_{0}\to\mathcal{T}$ is a conservative extension. In general, we
would need a proof of the following conjecture.

######  Conjecture 5.0.

Let $\mathcal{T}$ be a cofibrant SOGAT that satisfies external univalence. Let
$(\Gamma\vdash Y\ \mathsf{type})\in\mathcal{T}$ be a sort of $\mathcal{T}$
that is contractible (with respect to the weakly stable identity types arising
from external univalence). Then the extension
$\mathcal{T}\to\mathcal{T}[\gamma:\Gamma\vdash\bm{y}(\gamma):Y(\gamma)]$ is a
Morita equivalence, and
$\mathcal{T}[\gamma:\Gamma\vdash\bm{y}(\gamma):Y(\gamma)]$ also satifies
external univalence (with the same homotopy relations as $\mathcal{T}$).
$\lrcorner$

Proving section 5.3 or any special case would require some more tools
(including section 4.6), so we leave any proof to future work.

It should not too difficult to prove the special case of section 5.3 for
_closed_ contractible sorts, using the fact that $\mathcal{T}[\bm{y}:Y]$ is
isomorphic to the contextual slice $(\mathcal{T}\sslash 1_{\mathcal{T}}.Y)$,
that is the contextual core (in $\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$) of
the slice model $(\mathcal{T}/1_{\mathcal{T}}.Y)$.

The general case is more complicated. However, if we consider
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs instead of SOGATs with
external univalence (which are
$(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Id}_{ws})$-CwFs), then the analogous
result follows from section 4.6, applied to the SOGAT
$\mathcal{T}_{\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}}}$ that classifies
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs. This means that section 5.3
should follow from a coherence theorem providing a way to strictify
$(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Id}_{ws})$-CwFs into
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs. This strictification is
likely only possible for $(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Id}_{ws})$-CwFs
which satisfy some cofibrancy condition, e.g. which are cofibrant in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$.

##  6\. Partial saturation

This section introduces partially saturated
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs with respect to a family $E$
of homotopies, and the initial such CwF
$\mathcal{T}^{\infty}_{{\widehat{E}}}$. The main theorem of the paper reduces
the conservativity of the equational extension $\mathcal{T}\to\mathcal{T}_{E}$
to properties of $\mathcal{T}^{\infty}_{{\widehat{E}}}$.

###  6.1. Definitions

Let $\mathcal{C}$ be a $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF
equipped with an internal model of $\mathcal{T}$. For every generating sort
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}\in\mathsf{GenTy}_{\mathcal{T}}$,
we have a comparison map going from outer identifications ($\simeq$) to
homotopies ($\sim$), defined by sending the outer reflexivity $\mathsf{refl}$
to the constant homotopy $\mathsf{hrefl}$.

$\displaystyle{\mathsf{id}\text{-}\mathsf{to}\text{-}\mathsf{hpty}}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}:(x\simeq_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y)\to(x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y),$
$\displaystyle{\mathsf{id}\text{-}\mathsf{to}\text{-}\mathsf{hpty}}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\mathsf{refl})\simeq\mathsf{hrefl}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}.$

The CwF $\mathcal{C}$ is _saturated_ in the sense of section 4.6 exactly when
these maps are equivalences for every generating sort. Accordingly, we will
say that $\mathcal{C}$ is partially saturated with respect to a family of
homotopies when the restriction of
${\mathsf{id}\text{-}\mathsf{to}\text{-}\mathsf{hpty}}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
to these homotopies are all equivalences.

######  Definition 6.0.

Let $\mathcal{C}$ be a $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF
equipped with an internal model of $\mathcal{T}$, i.e. a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism $\mathcal{T}\to\mathcal{C}$. We say
that $\mathcal{C}$ is partially saturated with respect to $E$ if for every
homotopy $(\gamma:\Gamma\vdash
p(\gamma):x(\gamma)\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y(\gamma))\in
E$, the following contractibility condition holds:

$\gamma:\Gamma\vdash\mathrm{isContr}((q:x(\gamma)\simeq_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y(\gamma))\times({\mathsf{id}\text{-}\mathsf{to}\text{-}\mathsf{hpty}}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(q(\gamma))\simeq
p(\gamma))).$

In that case, we have the following center of contraction:

$\displaystyle\gamma:\Gamma\vdash\widehat{p}(\gamma):x(\gamma)\simeq_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y(\gamma),$
$\displaystyle\gamma:\Gamma\vdash\widetilde{p}(\gamma):{\mathsf{id}\text{-}\mathsf{to}\text{-}\mathsf{hpty}}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\widehat{p}(\gamma))\simeq
p(\gamma).$ $\lrcorner$

In particular, $\mathcal{C}$ is saturated exactly when it is partially
saturated with respect to all generic homotopies:

$\\{(\sigma:\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}},x:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma),y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma),p:x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y\vdash
p:x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y)\mid{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}\in\mathsf{GenTy}_{\mathcal{T}}\\},$

or equivalently with respect to all homotopies.

We write $\mathcal{T}^{\infty}_{{\widehat{E}}}$ for the initial object among
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs equipped with an internal
model of $\mathcal{T}$ that is partially saturated with respect to $E$. The
superscript $-^{\infty}$ indicates that $\mathcal{T}^{\infty}_{{\widehat{E}}}$
is morally an $\infty$-category, up to the conjectured correspondence between
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF and representable map
$\infty$-categories. The subscript $-_{{\widehat{E}}}$ indicates that
$\mathcal{T}^{\infty}_{{\widehat{E}}}$ includes lifts of every marked homotopy
in $E$.

We write $\mathcal{T}^{1}_{E}$ for the initial object among
$(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Eq})$-CwFs equipped with an internal model
of $\mathcal{T}_{E}$. The superscript $-^{1}$ now indicates that
$\mathcal{T}^{1}_{E}$ is morally a representable map $1$-category. Note that
$\mathcal{T}^{1}_{E}$ can be seen as a
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs equipped with an internal
model of $\mathcal{T}$. It is then saturated with respect to $E$, because the
equations of $E$ hold definitionally in $\mathcal{T}_{E}$. By the universal
property of $\mathcal{T}^{\infty}_{{\widehat{E}}}$, we therefore have a
morphism $\mathcal{T}^{\infty}_{{\widehat{E}}}\to\mathcal{T}^{1}_{E}$, such
that the following square commutes:

${\mathcal{T}}$${\mathcal{T}_{E}}$${\mathcal{T}^{\infty}_{{\widehat{E}}}}$${\mathcal{T}^{1}_{E}\hbox
to0.0pt{\ .\hss}}$

###  6.2. Properties of the vertical maps

We now discuss the properties of the two vertical maps in the above square.

Under some assumptions, these two morphisms should be seen as embeddings; at
the level of categories or $\infty$-categories they would correspond to fully
faithful functors or $\infty$-functors.

######  Proposition 6.0.

The $(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism
$\mathcal{T}_{E}\to\mathcal{T}^{1}_{E}$ is bijective on terms. ∎

We omit the proof; it follows from somewhat standard gluing constructions or
logical relation interpretations, very similar to the adequacy proof of [GS20]
or to the full proof of conservativity of two-level type theory of [Kov22].
From a more syntactic point of view, it is a canonicity proof, where the
canonical form of a term $(F(\Gamma)\vdash a:F(A))\in\mathcal{T}_{E}^{1}$ is a
term $(\Gamma\vdash a_{0}:A)\in\mathcal{T}_{E}$ such that $F(a_{0})=a$.

Alternatively, we don’t need to use $\mathcal{T}^{1}_{E}$, because we never
need to use its universal property in this paper. We can use the presheaf
category $\widehat{\mathcal{T}_{E}}$ instead, which is a
$(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Eq})$-CwF. The Yoneda embedding
$\mathbbm{y}:\mathcal{T}_{E}\to\widehat{\mathcal{T}_{E}}$ is a pseudo-morphism
of $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs, meaning that the terminal object,
context extensions and type-formers are only preserved up to isomorphism. The
action of $\mathbbm{y}$ on terms is bijective. Relying on the fact that
$\mathcal{T}_{E}$ is
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cellular,
we can replace the Yoneda embedding by a strict morphism
$y:\mathcal{T}_{E}\to\widehat{\mathcal{T}_{E}}$ along with a natural
isomorphism $\alpha:y\cong\mathbbm{y}$. Informally, the contexts and types of
$\mathcal{T}_{E}$ are freely closed under the operations of a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF, so we can redefine the actions of $y$ on
contexts and types by induction over them. Formally, we construct the iso-
gluing $\mathcal{G}(\mathbbm{y})$ of the Yoneda embedding, equip it with the
structure of a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF, and show that the projection
$\mathcal{G}(\mathbbm{y})\to\mathcal{T}_{E}$ has the right lifting property
with respect to
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$.
We then obtain a section $\mathcal{T}_{E}\to\mathcal{G}(\mathbbm{y})$, which
can be decomposed into $y$ and $\alpha$.

We only conjecture the analogous result for the other vertical map.

######  Conjecture 6.0.

If $\mathcal{T}$ satisfies external univalence and is cofibrant in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$, then
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$ is a weak equivalence in
$\mathbf{Mod}_{\mathcal{T}}$.  $\lrcorner$

This conjecture is discussed in more details in section 9.

###  6.3. Applications to conservativity

We now explain how the partially saturated model
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ can be used to establish that
$\mathcal{T}\to\mathcal{T}_{E}$ is a Morita equivalence. The idea is that
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ is seen as an $\infty$-congruence over
$\mathcal{T}$ (although we don’t formally define $\infty$-congruences).

An ordinary congruence consists of equivalence relations over the terms
$\mathcal{T}$. Equivalently, a congruence is an embedding of a set-valued
model into a setoid-valued model. Similarly, a $\infty$-congruence should be
an embedding of a set-valued model into a space-valued model, or a model
valued in $\infty$-groupoids.

Here we adopt the point of view that an $\infty$-groupoid is a type in a model
of type theory with identity types: the point of the $\infty$-groupoid are the
terms of that type, and the higher morphisms are the terms of the iterated
identity types. All higher composition operations can be derived from the
identity type eliminator. The identity types of
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ equip its terms with the structure of
$\infty$-groupoids. The higher structure of these $\infty$-groupoids is freely
generated by lifts of all homotopies in $E$.

Given a $1$-congruence, it is natural to consider its quotient. In order to
prove the conservativity of the extension $\mathcal{T}\to\mathcal{T}_{E}$, we
want consider the quotient of $\mathcal{T}_{{\widehat{E}}}^{\infty}$. To
ensure the existence of the quotient, we need to assume that the
$\infty$-congruence $\mathcal{T}_{{\widehat{E}}}^{\infty}$ can actually be
restricted to a $1$-congruence.

We first need to define the notion of $0$-truncated
$(\Sigma,{\mathsf{Id}})$-CwF.

######  Definition 6.0.

A $(\Sigma,{\mathsf{Id}})$-CwF $\mathcal{C}$ is said to be (merely)
$0$-truncated if for every self-identification $(\gamma:\Gamma\vdash
p(\gamma):x(\gamma)\simeq_{A(\gamma)}x(\gamma))$ in $\mathcal{C}$, there
(merely) exists an identification
$(\gamma:\Gamma\vdash\mathsf{uip}_{p}(\gamma):p(\gamma)\simeq\mathsf{refl})$
in $\mathcal{C}$.  $\lrcorner$

######  Definition 6.0.

A $(\Sigma,{\mathsf{Id}})$-CwF $\mathcal{C}$ is said to be (merely)
$0$-truncated relatively to a functor $F:\mathcal{A}\to\mathcal{C}$ if for
every self-identification $(\gamma:F(\Gamma)\vdash
p(\gamma):x(\gamma)\simeq_{A(\gamma)}x(\gamma))$ in $\mathcal{C}$, there
(merely) exists an identification
$(\gamma:F(\Gamma)\vdash\mathsf{uip}_{p}(\gamma):p(\gamma)\simeq\mathsf{refl})$
in $\mathcal{C}$.  $\lrcorner$

Our main result, which will be eventually proven in section 8, is then the
following:

######  Theorem 6.0.

If $\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$ is a weak equivalence
in $\mathbf{Mod}_{\mathcal{T}}$ and $\mathcal{T}^{\infty}_{{\widehat{E}}}$ is
merely $0$-truncated relatively to
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$, then
$\mathcal{T}\to\mathcal{T}_{E}$ is a Morita equivalence.

If $\mathcal{T}^{\infty}_{{\widehat{E}}}\to\mathcal{T}^{1}_{E}$ were a weak
equivalence in $\mathbf{Mod}_{\mathcal{T}}$, we could conclude using $2$-out-
of-$3$ for weak equivalences. However,
$\mathcal{T}^{\infty}_{{\widehat{E}}}\to\mathcal{T}^{1}_{E}$ is almost never a
weak equivalence in $\mathbf{Mod}_{\mathcal{T}}$ because of contexts that are
not in the image of $\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$, such
as
$\Gamma\triangleq(\sigma:\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}},x:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma),p:x\simeq_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}x)$.
Indeed,
${\mathsf{id}\text{-}\mathsf{to}\text{-}\mathsf{hpty}}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(p)\sim\mathsf{hrefl}$
is provable in $\mathcal{T}^{1}_{E}$, but cannot usually be proven in
$\mathcal{T}^{\infty}_{{\widehat{E}}}$. But
$\mathcal{T}^{\infty}_{{\widehat{E}}}\to\mathcal{T}^{1}_{E}$ doesn’t need to
be a full weak equivalence, it suffices that it satisfies the weak lifting
conditions only over contexts that are in the image of
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$.

We need a way to avoid contexts that are not in the image of
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$. We accomplish this by
computing the factorization (in $\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$) of
$\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}$ as a
$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cofibration
$\mathcal{T}\to{\mathcal{T}_{{\widehat{E}}}}$ followed by a
$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-fibration
${\mathcal{T}_{{\widehat{E}}}}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$. Here
$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-fibrations are the right class of maps
in the orthogonal factorization system generated by $I^{\mathsf{tm}}$, that is
maps whose action on terms is bijective.

######  Construction 6.0.

The $(\Sigma,\Pi_{\mathsf{rep}})$-CwF $\mathcal{T}_{{\widehat{E}}}$ is the
unique (up to isomorphism) $(\Sigma,\Pi_{\mathsf{rep}})$-CwF fitting in a
factorization

$\mathcal{T}\xrightarrow{}\mathcal{T}_{{\widehat{E}}}\xrightarrow{}\mathcal{T}_{{\widehat{E}}}^{\infty}$

where $\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}$ is a
$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cofibration and
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ is a
$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-fibration.  $\lrcorner$

The CwF ${\mathcal{T}_{{\widehat{E}}}}$ then plays the role of the image of
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$. It can also be
identified with the subCwF of $\mathcal{T}_{{\widehat{E}}}^{\infty}$ spanned
by the context and types that do not contain any identity types (because they
are freely generated by the type formers of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs).

The subscript $-_{{\widehat{E}}}$ still indicates that
$\mathcal{T}_{{\widehat{E}}}$ includes lifts of all marked homotopies in $E$,
or more precisely all transports and higher-dimensional transports over these
lifts. The absence of the superscript $-^{\infty}$ indicates that
$\mathcal{T}_{{\widehat{E}}}$ can no longer be seen as an $\infty$-category.

######  Lemma 6.0.

The map $\mathcal{T}\to{\mathcal{T}_{{\widehat{E}}}}$ is a
$\\{I^{\mathsf{ty}},E^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},E^{\mathsf{ty}_{\mathsf{rep}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cofibration.

###### Proof.

The map $\mathcal{T}\to{\mathcal{T}_{{\widehat{E}}}}$ is a
$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cofibration by definition and

$\\{I^{\mathsf{tm}},E^{\mathsf{tm}}\\}\subseteq\\{I^{\mathsf{ty}},E^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},E^{\mathsf{ty}_{\mathsf{rep}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}.$

######  Lemma 6.0.

The map ${\mathcal{T}_{{\widehat{E}}}}\to\mathcal{T}_{{\widehat{E}}}^{\infty}$
is a contextual isomorphism in $\mathbf{Mod}_{\mathcal{T}}$.

###### Proof.

Since that map is bijective on terms in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$, it is in particular bijective on
the elements of any sort, i.e. a contextual isomorphism. ∎

######  Lemma 6.0.

If $\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$ is a weak equivalence
in $\mathbf{Mod}_{\mathcal{T}}$, then
$\mathcal{T}\to{\mathcal{T}_{{\widehat{E}}}}$ is also a weak equivalence in
$\mathbf{Mod}_{\mathcal{T}}$.

###### Proof.

By $2$-out-of-$3$, since
${\mathcal{T}_{{\widehat{E}}}}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$ is a
weak equivalence in $\mathbf{Mod}_{\mathcal{T}}$ as a consequence of section
6.3. This direction of $2$-out-of-$3$ in $\mathbf{Mod}_{\mathcal{T}}$ was
proven in section 4.5. ∎

The lifting property of the
$\\{I^{\mathsf{ty}},E^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},E^{\mathsf{ty}_{\mathsf{rep}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cofibration
$\mathcal{T}\to{\mathcal{T}_{{\widehat{E}}}}$ against the contextual
isomorphism $\mathcal{T}_{E}\to\mathcal{T}_{E}^{1}$ provides a morphism
${\mathcal{T}_{{\widehat{E}}}}\to\mathcal{T}_{E}$ of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs. The following diagram commutes:

${\mathcal{T}}$${\mathcal{T}_{E}}$${\mathcal{T}_{{\widehat{E}}}}$${\mathcal{T}^{\infty}_{{\widehat{E}}}}$${\mathcal{T}^{1}_{E}\hbox
to0.0pt{\
.\hss}}$$\scriptstyle{\sim}$$\scriptstyle{L}$$\scriptstyle{\sim}$$\scriptstyle{K}$$\scriptstyle{F}$$\scriptstyle{G}$

The remainder of the paper develops tools used to prove that
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ is a non-split trivial
fibrations whenever $\mathcal{T}_{{\widehat{E}}}^{\infty}$ is merely
$0$-truncated relatively to
$\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}^{\infty}$.

##  7\. Quotients of models of first-order GATs

In this section we discuss congruences over models of (first-order) GATs and
quotients of such congruences. In this paper, we only need applications to the
GAT of $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs, but it is easier to present them in
full generality.

For ordinary algebraic theories, congruences and quotients are very well-
behaved. A congruence simply consists of equivalence relations for every sort,
preserving all operations in the theory. The quotient of a model is computed
by taking the quotient of every sort by the specified equivalence relation.

For generalized algebraic theories, matters are more complicated, because of
the presence of dependent sorts. We still have a general notion of congruence,
but quotients can no longer be computed sortwise. In other words, the quotient
inclusion is not necessarily a _trivial fibration_.

For example, we can consider the quotient of the category
${a}$${b}$${c}$${d}$$\scriptstyle{f}$$\scriptstyle{g}$ by the congruence that
identifies $b$ and $c$. In the quotient, it is possible to compose $f$ and
$g$, but there is no morphism corresponding to their composition in the
original category. The quotient inclusion functor is not full.

However, by adding additional fibration condition to the definition of
congruence, it becomes possible to compute the quotient pointwise. The
quotient inclusion of any “fibrant” congruence is then a non-split trivial
fibration. Furthermore, every non-split trivial fibration arises (up to
isomorphism) as the quotient of a fibrant congruence.

###  7.1. Functorial semantics of GATs

We start by briefly recalling the functorial semantics of GATs in
$\mathbf{CwF}_{\Sigma}$, in the same style as for the semantics of SOGATs
developed in section 4.

######  Definition 7.0.

A generalized algebraic theory (GAT) is a
$\\{I^{\mathsf{ty}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cellular $\Sigma$-CwF.
$\lrcorner$

Any SOGAT without representable sorts is also a GAT (this can be proven by
induction over the
$\\{I^{\mathsf{ty}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cellular presentation
of the SOGAT). This includes the GATs of categories (section 4.1), monoidal
categories (section 4.1), etc.

######  Example 7.0.

The GAT $\mathcal{T}_{\mathbf{CwF}}$ of CwFs extends the GAT of categories
with two new sorts

$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}\to\mathbb{T}_{\mathbf{CwF}},$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}:(\Gamma:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}})\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}(\Gamma)\to\mathbb{T}_{\mathbf{CwF}},$

six operations

$\displaystyle\\_[\\_]:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}(\Gamma)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(\Delta,\Gamma)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}(\Delta),$
$\displaystyle\\_[\\_]:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(\Gamma,A)\to(\gamma:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(\Delta,\Gamma))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}(\Delta,A[\gamma]),$
$\displaystyle\\_.\\_:(\Gamma:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}})\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}(\Gamma)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}},$
$\displaystyle\bm{p}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(\Gamma.A,\Gamma),$
$\displaystyle\bm{q}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(\Gamma.A,A[\bm{p}]),$
$\displaystyle{\left\langle\\_,\\_\right\rangle}:(\gamma:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(\Delta,\Gamma))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(\Delta,A[\gamma])\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(\Delta,\Gamma.A)$

and some equations expressing the functoriality and naturality of these
operations.

Similarly, there is a GAT
$\mathcal{T}_{\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}}$ of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs, which extends $\mathcal{T}_{\mathbf{CwF}}$
by a new sort of representable types, a substitution operation for
representable types, an operation for every type-theoretic operation of a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF, and equations expressing the functoriality
and naturality of the operations.  $\lrcorner$

We now fix a GAT $\mathcal{T}$ for most of the section. A closed sort of
$\mathcal{T}$ is an object $X\in\mathcal{T}$ (or equivalently a closed type).
A dependent sort of $\mathcal{T}$ is a type $(X\vdash Y\
\mathsf{type})\in\mathcal{T}$.

######  Definition 7.0.

A model of $\mathcal{T}$ is a $\Sigma$-CwF morphism
$\mathcal{T}\to\mathbf{Set}$. A morphism between two models
$\mathcal{M},\mathcal{N}:\mathcal{T}\to\mathbf{Set}$ is a natural
transformation $\mathcal{M}\Rightarrow\mathcal{N}$.  $\lrcorner$

Given a closed sort $X\in\mathcal{T}$ and morphism
$F:\mathcal{M}\to\mathcal{N}$, the component

$F_{X}:\mathcal{M}_{X}\to\mathcal{N}_{X}$

of the natural transformation is the action of $F$ on elements of the sort
$X$.

For any dependent sort $(X\vdash Y\ \mathsf{type})\in\mathcal{T}$ and morphism
$F:\mathcal{M}\to\mathcal{N}$, there is an action

$F_{Y}:\mathcal{M}_{Y}(x)\to\mathcal{N}_{Y}(F_{X}(x))$

of $F$ on elements of $Y$, uniquely specified by the fact that

$F_{X.Y}:\mathcal{M}_{X.Y}\to\mathcal{N}_{X.Y}$

should send $(x,y)$ to $(F_{X}(x),F_{Y}(y))$.

######  Definition 7.0.

A morphism $F:\mathcal{M}\to\mathcal{N}$ in $\mathbf{Mod}_{\mathcal{T}}$ is a
trivial fibration if for every dependent sort $(X\vdash Y\
\mathsf{type})\in\mathcal{T}$, the map

$F_{Y}:\mathcal{M}_{Y}(x)\to\mathcal{N}_{Y}(F_{X}(x))$

is surjective.  $\lrcorner$

As in earlier definitions of weak equivalences and trivial fibrations, we
actually have two notions of trivial fibrations: split trivial fibrations and
non-split trivial fibrations.

######  Remark 7.0.

When applied to the GAT $\mathcal{T}_{\mathbf{CwF}}$ of CwFs, trivial
fibrations as defined in section 7.1 are not exactly the same as trivial
fibrations as defined in section 2.4, which could be called local trivial
fibrations. Indeed, section 7.1 includes additional lifting conditions for
context and substitutions. Fortunately, any trivial fibration is a local
trivial fibration, which is the direction needed for our constructions.
$\lrcorner$

###  7.2. Congruences

Given an equivalence relation $\widetilde{X}$ over a set $X$, we write
$(x_{1}\sim x_{2})\in\widetilde{X}$ to indicate that $x_{1}$ and $x_{2}$ . We
use the same notation for dependent equivalence relations. Given a dependent
equivalence relation $\widetilde{Y}$ over $\widetilde{X}$, writing $(y_{1}\sim
y_{2})\in\widetilde{Y}$ presupposes that $(x_{1}\sim x_{2})\in\widetilde{X}$
(when $y_{1}:Y(x_{1})$ and $y_{2}:Y(x_{2})$).

The $\Sigma$-CwF $\mathbf{Setoid}$ of setoids is a CwF over the category of
setoids in which types are dependent (or displayed) setoids, i.e. families of
sets equipped with a dependent equivalence relation.

######  Definition 7.0.

A congruence over a model $\mathcal{M}:\mathcal{T}\to\mathbf{Set}$ is a
$\Sigma$-CwF morphism $\widetilde{\mathcal{M}}:\mathcal{T}\to\mathbf{Setoid}$
such that $U\circ\widetilde{\mathcal{M}}=\mathcal{M}$.  $\lrcorner$

Given a congruence $\widetilde{\mathcal{M}}$ and a closed sort
$X\in\mathcal{T}$, we have an equivalence relation
$\widetilde{\mathcal{M}}_{X}$ on $\mathcal{M}_{X}$. For a dependent sort
$(X\vdash Y\ \mathsf{type})\in\mathcal{T}$, we have a dependent equivalence
relation $\widetilde{\mathcal{M}}_{Y}$ over $\widetilde{\mathcal{M}}_{X}$.
Given any morphism or term in $\mathcal{T}$, the action of
$\widetilde{\mathcal{M}}$ on morphisms and terms implies that the
corresponding operation of $\mathcal{M}$ preserves the (dependent) equivalence
relations.

Given two congruences $\widetilde{\mathcal{M}}$ and $\overline{\mathcal{M}}$
over the same model $\mathcal{M}$, we write
$\widetilde{\mathcal{M}}\subseteq\overline{\mathcal{M}}$ when
$\widetilde{\mathcal{M}}_{X}\subseteq\overline{\mathcal{M}}_{X}$ as relations
for every closed sort or dependent sort $X$.

######  Definition 7.0.

The kernel of a morphism $F:\mathcal{M}\to\mathcal{N}$ of models is the
congruence $\ker_{F}:\mathcal{T}\to\mathbf{Setoid}$ over $\mathcal{M}$ defined
by:

$((x_{1}\sim x_{2})\in\ker_{F}(X))\overset{\triangle}{\iff}F(x_{1})=F(x_{2})$

for any closed sort $X\in\mathcal{T}$ and

$((y_{1}\sim y_{2})\in\ker_{F}(Y))\overset{\triangle}{\iff}F(y_{1})=F(y_{2})$

for any dependent sort $(X\vdash Y\ \mathsf{type})\in\mathcal{T}$.
$\lrcorner$

######  Definition 7.0.

A quotient of a congruence $\widetilde{\mathcal{M}}$ is a model $\mathbf{Q}$
along with a morphism $\mathbf{q}:\mathcal{M}\to\mathbf{Q}$ such that
$\widetilde{\mathcal{M}}\subseteq\ker_{\mathbf{q}}$ and satisfying the
following universal property: for every other morphism
$F:\mathcal{M}\to\mathcal{N}$ such that
$\widetilde{\mathcal{M}}\subseteq\ker_{F}$, there is a unique morphism
$\widetilde{F}:\mathbf{Q}\to\mathcal{N}$ such that
$\widetilde{F}\circ\mathbf{q}=F$.  $\lrcorner$

######  Lemma 7.0.

A quotient of a congruence always exists.

###### Proof.

The quotient can be expressed as a coequalizer and the category of models of
$\mathcal{T}$ is cocomplete. ∎

###  7.3. Fibrant congruences and quotients

######  Definition 7.0.

A dependent equivalence relation $\widetilde{Y}$ over an equivalence relation
$\widetilde{X}$ is fibrant if it satisfies the following lifting condition:
for every $(x_{1}\sim x_{2})\in\widetilde{X}$ and $y_{1}:Y(x_{1})$, there
merely exists some $y_{2}:Y(x_{2})$ such that $(y_{1}\sim
y_{2})\in\widetilde{Y}$.  $\lrcorner$

We can restrict the types of $\mathbf{Setoid}$ to fibrant dependent
equivalence relations. This provides a sub-CwF
$\mathbf{Setoid}_{\mathsf{fib}}\subseteq\mathbf{Setoid}$ over the same base
category.

######  Definition 7.0.

A congruence $\widetilde{\mathcal{M}}:\mathcal{T}\to\mathbf{Setoid}$ is
fibrant if it factors through the inclusion
$\mathbf{Setoid}_{\mathsf{fib}}\subseteq\mathbf{Setoid}$, i.e. if for every
dependent sort $(X\vdash Y\ \mathsf{type})\in\mathcal{T}$, the dependent
equivalence relation $\widetilde{\mathcal{M}}_{Y}$ is fibrant.  $\lrcorner$

######  Lemma 7.0.

The quotient functor $Q:\mathbf{Setoid}_{\mathsf{fib}}\to\mathbf{Set}$ extends
to a $\Sigma$-CwF morphism.

###### Proof.

We have to prove that $Q$ preserves context extensions. This boils down to the
fact that $Q$ preserves pullback squares when at least one of the maps of the
cospan is a setoid fibration.

Take a pullback square in $\mathbf{Setoid}$.

${B}$${Y}$${A}$${X\hbox to0.0pt{
,\hss}}$${\lrcorner}$$\scriptstyle{p}$$\scriptstyle{f}$

where $Y\twoheadrightarrow X$ is a setoid fibration. We write $[-]$ for the
inclusions into the quotients of the setoids. Our goal is to prove that the
canonical map $Q(B)\to Q(A)\times_{Q(X)}Q(Y)$ is an isomorphism.

We define the inverse $Q(A)\times_{Q(X)}Q(Y)\to Q(B)$ using the universal
properties of the quotients. Take a pair $([a],[y])$ in
$Q(A)\times_{Q(X)}Q(Y)$. We have $[f(a)]=[p(y)]$, i.e. $f(a)\sim p(y)$ in the
setoid $X$. Since $p:Y\twoheadrightarrow X$ is a fibration, we can find
$y^{\prime}\in Y$ such that $p(y)=f(a)$ and $y^{\prime}\sim y$. We send the
pair $([a],[y])$ to the element $[(a,y^{\prime})]$ of $Q(B)$. It can be shown
that element does not depend on the choices of $a$, $y$ and $y^{\prime}$, thus
the candidate inverse is well-defined.

It is then straightforward to show that the defined map is an inverse. ∎

######  Lemma 7.0.

Given a fibrant congruence $\widetilde{\mathcal{M}}$, the model
$\mathbf{Q}(\widetilde{\mathcal{M}})\triangleq(Q\circ\widetilde{\mathcal{M}}):\mathcal{T}\to\mathbf{Set}$
is the quotient of $\widetilde{\mathcal{M}}$. The quotient inclusion
$\mathbf{q}:\mathcal{M}\Rightarrow\mathbf{Q}(\widetilde{\mathcal{M}})$ is the
natural transformation $\widetilde{\mathcal{M}}\cdot q$, where $q:U\Rightarrow
Q$ is the natural transformation that maps the underlying sets of setoids to
their quotients.

###### Proof.

Let $\mathcal{N}$ be any model of $\mathcal{T}$, along with a morphism
$F:\mathcal{M}\to\mathcal{N}$ such that
$\widetilde{\mathcal{M}}\subseteq\ker_{F}$. We define a natural transformation
$\widetilde{F}:\mathbf{Q}(\widetilde{\mathcal{M}})\Rightarrow\mathcal{N}$.

For any closed sort $X\in\mathcal{T}$, we define
$\widetilde{F}_{X}:Q(\widetilde{\mathcal{M}}_{X})\to\mathcal{N}_{X}$ using the
universal property of $Q(\widetilde{\mathcal{M}}_{X})$, as the unique lift of
$F_{X}:\mathcal{M}_{X}\to\mathcal{N}_{X}$.

For any morphism $f:X\to Y$, the commutation of the square

${Q(\widetilde{\mathcal{M}}_{X})}$${Q(\widetilde{\mathcal{M}}_{Y})}$${\widetilde{\mathcal{N}}_{X}}$${\widetilde{\mathcal{N}}_{Y}}$$\scriptstyle{Q(\widetilde{\mathcal{M}}_{f})}$$\scriptstyle{\widetilde{F}_{X}}$$\scriptstyle{\widetilde{F}_{Y}}$$\scriptstyle{\mathcal{N}_{f}}$

follows from the universal property of the quotient
$Q(\widetilde{\mathcal{M}}_{X})$.

The uniqueness of $\widetilde{F}$ as a lift of $F$ follows from the uniqueness
of every component $\widetilde{F}_{X}$ as a lift of $F_{X}$. ∎

######  Corollary 7.0.

If $\widetilde{\mathcal{M}}$ is a fibrant congruence, then
$\mathbf{q}:\mathcal{M}\to\mathbf{Q}(\widetilde{\mathcal{M}})$ is a non-split
trivial fibration in $\mathbf{Mod}_{\mathcal{T}}$.

###### Proof.

By section 7.3, all components of $\mathbf{q}$ are quotient inclusions, which
are all non-split surjections. ∎

######  Lemma 7.0.

If $F:\mathcal{M}\to\mathcal{N}$ is a non-split trivial fibration in
$\mathbf{Mod}_{\mathcal{T}}$, then $\ker_{F}$ is a fibrant congruence and
$\mathcal{N}$ is a quotient of $\ker_{F}$.

###### Proof.

We first prove the fibrancy of $\ker_{F}$.

Let $(X\vdash Y\ \mathsf{type})\in\mathcal{T}$ be a dependent sort of
$\mathcal{T}$. Take $x_{1},x_{2}:\mathcal{M}_{X}$ such that
$F(x_{1})=F(x_{2})$ and $y_{1}:\mathcal{M}_{Y}(x_{1})$. Then
$F(y_{1}):\mathcal{N}_{Y}(F(x_{2}))$. Since $F$ is a trivial fibration, there
exists a lift $y_{2}:\mathcal{M}_{Y}(x_{2})$ such that $F(y_{2})=F(y_{2})$.
This proves exactly that $\ker_{F}$ is fibrant.

We can now construct the quotient $\mathbf{Q}(\ker_{F})$ (which could be
called the coimage of $F$), and we know that the quotient inclusion is a non-
split trivial fibration. The map $F$ factors through the quotient inclusion.

${\mathcal{M}}$${\mathcal{N}}$${\mathbf{Q}(\ker_{F})}$$\scriptstyle{F}$$\scriptstyle{\sim}$$\scriptstyle{\mathbf{q}}$$\scriptstyle{\sim}$$\scriptstyle{G}$

Since $F$ is a non-split trivial fibration, $G$ is also a non-split trivial
fibration, surjective on every sort. To prove that $G$ is an isomorphism, it
suffices to show that $G$ is injective on every sort.

Let $(X\vdash Y\ \mathsf{type})\in\mathcal{T}$ be a dependent sort. Take
$x:{\mathbf{Q}(\ker_{F})}_{X}$ and $y_{1},y_{2}:{\mathbf{Q}(\ker_{F})}_{Y}(x)$
such that $G(y_{1})=G(y_{2})$. Since $\mathbf{q}$ is a non-split trivial
fibration there exists lifts $x^{\prime}:\mathcal{M}_{X}$ and
$y_{1}^{\prime},y_{2}^{\prime}:\mathcal{M}_{Y}(x^{\prime})$ of $x$, $y_{1}$
and $y_{2}$. We then have $F(y^{\prime}_{1})=F(y^{\prime}_{2})$, i.e.
$(y^{\prime}_{1}\sim y^{\prime}_{2})\in\ker_{F}$. Therefore,
$\mathbf{q}(y^{\prime}_{1})=\mathbf{q}(y^{\prime}_{2})$, that is
$y_{1}=y_{2}$.

This proves that the actions of $G$ on every sort are injective. Therefore,
$G$ is an isomorphism and $\mathcal{N}$ is a quotient of $\ker_{F}$. ∎

##  8\. Trivial fibrations as retracts of quotient inclusions

Fix a SOGAT $\mathcal{T}$ equipped with homotopy relations and an equational
extension $\mathcal{T}\to\mathcal{T}_{E}$. Recall from section 6 that we have
the following commutative diagram in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$:

${\mathcal{T}}$${\mathcal{T}_{E}}$${\mathcal{T}_{{\widehat{E}}}}$${\mathcal{T}^{\infty}_{{\widehat{E}}}}$${\mathcal{T}^{1}_{E}\hbox
to0.0pt{\
.\hss}}$$\scriptstyle{\sim}$$\scriptstyle{L}$$\scriptstyle{\sim}$$\scriptstyle{K}$$\scriptstyle{F}$$\scriptstyle{G}$

The goal of this section is to prove the following theorem:

######  Theorem 8.0.

Let $\mathcal{T}$ be a SOGAT with homotopy relations, and let $E$ be a set of
homotopies of $\mathcal{T}$. If $\mathcal{T}^{\infty}_{{\widehat{E}}}$ is
merely $0$-truncated relatively to
$K:\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$, then
$F:\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ is a trivial fibration in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$.

We follow the structure of Hofmann’s proof of the conservativity of
Extensional Type Theory over Intensional Type Theory. We will construct a
quotient $\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})$ in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$ of $\mathcal{T}_{{\widehat{E}}}$ by
a fibrant congruence $\widetilde{\mathcal{T}_{{\widehat{E}}}}$, and prove that
the map $\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ becomes a retract of
the quotient inclusion
$\mathbf{q}:\mathcal{T}_{{\widehat{E}}}\to\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})$.
The results then follows from the closure of non-split trivial fibrations
under retracts.

${\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})}$${\mathcal{T}_{{\widehat{E}}}}$${\mathcal{T}_{E}}$$\scriptstyle{R}$$\scriptstyle{F}$$\scriptstyle{\mathbf{q}}$$\scriptstyle{S}$

###  8.1. Equivalences and dependent equivalences

For this proof we need to consider some equivalences over the contexts and
types of $\mathcal{T}_{{\widehat{E}}}^{\infty}$. It is most convenient to work
with relational equivalences, also known as one-to-one correspondences. A
relational equivalence between two types $A$ and $B$ is a type-valued relation
that is functional in both directions. The advantage of this definition is
that is easy to show that the standard type structures ($\mathbf{1}$, $\Sigma$
and $\Pi$) preserve equivalences.

Let $\mathbb{C}$ be a family equipped with $\Sigma$-types and weak identity
types.

######  Definition 8.0.

Let $A_{1},A_{2}:\mathbb{C}$ be two types. An equivalence $\alpha:A_{1}\simeq
A_{2}$ is a type-valued relation

$\alpha:A_{1}\to A_{2}\to\mathbb{C}$

satisfying the following two contractibility conditions

$\displaystyle(a_{1}:A_{1})\to\mathrm{isContr}((a_{2}:A_{2})\times\alpha(a_{1},a_{2})),$
$\displaystyle(a_{2}:A_{2})\to\mathrm{isContr}((a_{1}:A_{1})\times\alpha(a_{1},a_{2})).$
$\lrcorner$

The elements of $\alpha(a_{1},a_{2})$ will be called identifications between
$a_{1}$ and $a_{2}$.

######  Definition 8.0.

Let $B_{1}:A_{1}\to\mathbb{C}$ and $B_{2}:A_{2}\to\mathbb{C}$ be two dependent
types. A dependent equivalence $\beta:B_{1}\simeq_{\alpha}B_{2}$ over an
equivalence $\alpha:A_{1}\simeq A_{2}$ is a family

$\beta:\forall a_{1}\ a_{2}\to\alpha(a_{1},a_{2})\to B_{1}(a_{1})\simeq
B_{2}(a_{2})$

of equivalences.  $\lrcorner$

######  Definition 8.0.

Let $\alpha_{1},\alpha_{2}:A_{1}\simeq A_{2}$ be two parallel equivalences. A
homotopy $H:\alpha_{1}\simeq\alpha_{2}$ between $\alpha_{1}$ and $\alpha_{2}$
is a family

$H:\forall a_{1}\
a_{2}\to\alpha_{1}(a_{1},a_{2})\simeq\alpha_{2}(a_{1},a_{2})$

of equivalences.  $\lrcorner$

######  Definition 8.0.

Let $\beta_{1}:B_{1}\simeq_{\alpha_{1}}B_{2}$ and
$\beta_{2}:B_{1}\simeq_{\alpha_{2}}B_{2}$ be two parallel dependent
equivalences, and $H:\alpha_{1}\simeq\alpha_{2}$ be a homotopy between
$\alpha_{1}$ and $\alpha_{2}$. A dependent homotopy $G$ between $\beta_{1}$
and $\beta_{2}$ is a family

$\displaystyle G:\forall a_{1}\ a_{2}\ (a_{e1}:\alpha_{1}(a_{1},a_{2}))\
(a_{e2}:\alpha_{2}(a_{1},a_{2}))\ (a_{ee}:H(a_{e1},a_{e2}))$
$\displaystyle\quad\to\forall b_{1}\
b_{2}\to\beta_{1}(a_{e1},b_{1},b_{2})\simeq\beta_{2}(a_{e2},b_{1},b_{2})$

of equivalences.  $\lrcorner$

These notions come with various composition operations, including identity
equivalences, inverse equivalences, etc.

###  8.2. Construction of the fibrant congruence

We now assume that $\mathcal{T}^{\infty}_{{\widehat{E}}}$ is merely
$0$-truncated relatively to
$K:\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$.

We want to construct a quotient of $\mathcal{T}_{{\widehat{E}}}$ by a fibrant
congruence. This congruence should identify terms of
$\mathcal{T}_{{\widehat{E}}}$ when there is an identification between them in
$\mathcal{T}_{{\widehat{E}}}^{\infty}$, and it should identify types of
$\mathcal{T}_{{\widehat{E}}}$ when they are equivalent in
$\mathcal{T}_{{\widehat{E}}}^{\infty}$. Since
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ is $0$-truncated relatively to $K$, the
choice of identifications won’t matter. However, there may be multiple
parallel equivalences in $\mathcal{T}_{{\widehat{E}}}^{\infty}$. Because of
that, we need to consider a restricted class of equivalences, built from
transport over identifications. This is analogous to the partial families
$\mathsf{co}_{\Gamma,\Delta}$ and $\mathsf{ty}_{\Gamma,\Delta,\sigma,\tau}$ of
propositional isomorphisms that are used in Hofmann’s conservativity proof
[Hof95].

######  Construction 8.0.

We define the following set-valued relations and families of equivalences by
induction over the structure of contexts and types of
$\mathcal{T}_{{\widehat{E}}}$.

$\displaystyle({\approx}):\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{{\widehat{E}}}\to\mathrm{Set},$
$\displaystyle({\approx}):(\Gamma_{1}\approx\Gamma_{2})\to\mathcal{T}_{{\widehat{E}}}.\mathsf{Ty}\to\mathcal{T}_{{\widehat{E}}}.\mathsf{Ty}\to\mathrm{Set},$
$\displaystyle({\approx})^{\mathsf{rep}}:(\Gamma_{1}\approx\Gamma_{2})\to\mathcal{T}_{{\widehat{E}}}.\mathsf{Ty}_{\mathsf{rep}}\to\mathcal{T}_{{\widehat{E}}}.\mathsf{Ty}_{\mathsf{rep}}\to\mathrm{Set},$
$\displaystyle\alpha:(\Gamma_{1}\approx\Gamma_{2})\to(K(\Gamma_{1})\simeq
K(\Gamma_{2})),$
$\displaystyle\beta:(p:\Gamma_{1}\approx\Gamma_{2})\to(A\approx_{p}B)\to(K(A)\simeq_{\alpha_{p}}K(B)),$
$\displaystyle\beta^{\mathsf{rep}}:(p:\Gamma_{1}\approx\Gamma_{2})\to(A\approx^{\mathsf{rep}}_{p}B)\to(K(A)\simeq_{\alpha_{p}}K(B)).$

Empty context:

We pose $(\diamond\approx\diamond)\triangleq\\{\star\\}$. Given
$p:\diamond\approx\diamond$, we let $\alpha_{p}$ be the identity equivalence,
that is

$\alpha_{p}(\\_,\\_)\triangleq\mathbf{1}.$

Context extension:

We pose
$((\Gamma_{1}.A_{1})\approx(\Gamma_{2}.A_{2}))\triangleq(p:\Gamma_{1}\approx\Gamma_{2})\times(q:A_{1}\approx_{p}A_{2})$.
Given $(p,q):(\Gamma_{1}.A_{1})\approx(\Gamma_{2}.A_{2})$, we let
$\alpha_{(p,q)}$ be the equivalence obtained by lifting the equivalences
$\alpha_{p}$ and $\beta_{q}$ to extended contexts, i.e.

$\alpha_{(p,q)}((\gamma_{1},a_{1}),(\gamma_{2},a_{2}))\triangleq(\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2}))\times(a_{e}:\beta_{q}(\gamma_{e},a_{1},a_{2})).$

Basic types:

We let
$({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1})\approx_{p}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{2}))$
be the set of identifications between $K(\sigma_{1})$ and $K(\sigma_{2})$ over
the equivalence $\alpha_{p}$, that is an element of
$({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1})\approx_{p}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{2}))$
is an element

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
q(\gamma_{e}):K(\sigma_{1})(\gamma_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}K(\sigma_{2})(\gamma_{2}))\in\mathcal{T}_{{\widehat{E}}}^{\infty}$

Given such an identification $q$, we let $\beta_{q}$ be the dependent
equivalence defined by transport over $q$, namely

$\beta_{q}(\gamma_{e},a_{1},a_{2})\triangleq\mathsf{transport}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(-)}(a_{1},q(\gamma_{e}))\simeq_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(K(\sigma_{2})(\gamma_{2}))}a_{2}.$

$\mathbf{1}$-types:

We pose $(\mathbf{1}\approx_{p}\mathbf{1})\triangleq\\{\star\\}$. Given
$q:\mathbf{1}\approx_{p}\mathbf{1}$, we let $\beta_{q}$ be the identity
equivalence, that is

$\beta_{q}(\gamma_{e},\\_,\\_)\triangleq\mathbf{1}.$

$\Sigma$-types:

We pose
$(\Sigma(A_{1},B_{1})\approx_{p}\Sigma(A_{2},B_{2}))\triangleq(q_{A}:A_{1}\approx_{p}A_{2})\times(q_{B}:B_{1}\approx_{p,q_{A}}B_{2})$.
Given $q:\Sigma(A_{1},B_{1})\approx_{p}\Sigma(A_{2},B_{2})$, we let
$\beta_{q}$ be the equivalence obtained by lifting the equivalences
$\beta_{q_{A}}$ and $\beta_{q_{B}}$ to $\Sigma$-types, that is

$\beta_{q}(\gamma_{e},(a_{1},a_{2}),(b_{1},b_{2}))\triangleq(a_{e}:\beta_{q_{A}}(\gamma_{e},a_{1},a_{2}))\times(b_{e}:\beta_{q_{B}}((\gamma_{e},a_{e}),b_{1},b_{2})).$

$\Pi_{\mathsf{rep}}$-types:

We pose
$(\Pi_{\mathsf{rep}}(A_{1},B_{1})\approx_{p}\Pi_{\mathsf{rep}}(A_{2},B_{2}))\triangleq(q_{A}:A_{1}\approx^{\mathsf{rep}}_{p}A_{2})\times(q_{B}:B_{1}\approx_{p,q_{A}}B_{2})$.
Given
$q:\Pi_{\mathsf{rep}}(A_{1},B_{1})\approx_{p}\Pi_{\mathsf{rep}}(A_{2},B_{2})$,
we let $\beta_{p}(q)$ be the equivalence obtained by lifting the equivalences
$\beta_{q_{A}}$ and $\beta_{q_{B}}$ to $\Pi_{\mathsf{rep}}$-types, namely

$\beta_{q}(\gamma_{e},f_{1},f_{2})\triangleq(a_{1}:A_{1}(\gamma_{1}))\
((a_{2},a_{e}):=\overrightarrow{\beta_{q_{A}}}(a_{1}))\to\beta_{q_{B}}((\gamma_{e},a_{e}),f_{1}(a_{1}),f_{2}(a_{2})).$

Here $a_{2}:K(A_{2})(\gamma_{2})$ and
$a_{e}:\beta_{q_{A}}(\gamma_{e},a_{1},a_{2})$ are defined by transporting
$a_{1}$ over the equivalence $\beta_{q_{A}}$. It would not be possible to
quantify over $(a_{2},a_{e})$ instead, because
$a_{e}:\beta_{q_{A}}(a_{1},a_{2})$, but $\beta_{q_{A}}(a_{1},a_{2})$ is
assumed to be representable.

Representable types:

The relation ${\approx}^{\mathsf{rep}}$ and the function
$\beta^{\mathsf{rep}}$ are defined analogously to ${\approx}$ and $\beta$.
Given two representable types $A$ and $B$, we pose $A\approx_{p}B\triangleq
A\approx^{\mathsf{rep}}_{p}B$. Given $q:A\approx_{p}B$, we pose
$\beta_{q}\triangleq\beta_{q}^{\mathsf{rep}}$.

Remaining cases:

In any other case, i.e. when the two contexts or types have different shapes,
they are not related by ${\approx}$, i.e. we pose

$(A\approx B)\triangleq\emptyset.$

We will use induction on the structure of context and types of
$\mathcal{T}_{{\widehat{E}}}$ in multiple proofs. In all of those, we view
basic types (of the form
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)$)
as the base cases of the induction, and all other cases as recursive cases of
the induction.

We now prove that the relations $(\approx)$ are reflexive, transitive and
symmetric up to homotopy.

######  Lemma 8.0.

For every $\Gamma\in\mathcal{T}_{{\widehat{E}}}$, there is an element
$r_{\Gamma}:\Gamma\approx\Gamma$ and a homotopy between the equivalence
$\alpha_{r_{\Gamma}}:K(\Gamma)\simeq K(\Gamma)$ and the identity equivalence.

For every $(\Gamma\vdash A\ \mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$,
there is an element $r_{A}:A\approx_{r_{\Gamma}}A$ and a homotopy between the
dependent equivalence $\beta_{r_{A}}:K(A)\simeq_{\alpha_{r_{\Gamma}}}K(A)$ and
the identity equivalence.

The analogous statement also holds for representable types.

###### Proof.

By mutual induction on the structures of $\Gamma$ and $A$. In every case we
have to use the fact that the corresponding construction of $\alpha$ or
$\beta$ preserves identity equivalences. ∎

We can prove both symmetry and transitivity in a single step.

######  Lemma 8.0.

For every $\Gamma_{1},\Gamma_{2},\Gamma_{3}:\mathcal{T}_{{\widehat{E}}}$ and
elements $p_{1}:\Gamma_{1}\approx\Gamma_{2}$ and
$p_{2}:\Gamma_{3}\approx\Gamma_{2}$, there is an element
$t(p_{1},p_{2}):\Gamma_{1}\approx\Gamma_{3}$ and a homotopy between
$\alpha(t(p_{1},p_{2})):K(\Gamma_{1})\simeq K(\Gamma_{3})$ and the composed
equivalence $\alpha(p_{1})\cdot{\alpha(p_{2})}^{-1}$.

Given types $(\Gamma_{1}\vdash A_{1}\ \mathsf{type})\in\mathcal{T}$,
$(\Gamma_{2}\vdash A_{2}\ \mathsf{type})\in\mathcal{T}$ and $(\Gamma_{3}\vdash
A_{3}\ \mathsf{type})\in\mathcal{T}$, and elements
$q_{1}:A_{1}\approx_{p_{1}}A_{2}$ and $q_{2}:A_{3}\approx_{p_{2}}A_{2}$, there
is an element $t(q_{1},q_{2}):A_{1}\approx_{t(p_{1},p_{2})}A_{3}$ and a
homotopy between $\beta(t(q_{1},q_{2}))$ and the composed equivalence
$\beta(q_{1})\cdot{\beta(q_{2})}^{-1}$.

The analogous statement also holds for representable types.

###### Proof.

By mutual induction on the structures of the contexts and types. In every case
we have to use the fact that the corresponding construction of $\alpha$ or
$\beta$ preserves inverse equivalences and compositions of equivalences. ∎

Symmetry for $p:\Gamma\approx\Delta$ can then be recovered as
$t(r_{\Gamma},p)$, and transitivity for $p:\Gamma\approx\Delta$ and
$q:\Delta\approx\Theta$ can be reconstructed as $t(p,t(r_{\Delta},q))$.

######  Lemma 8.0.

Given two elements $p_{1},p_{2}:\Gamma_{1}\approx\Gamma_{2}$, there merely
exists a homotopy between the equivalences $\alpha_{p_{1}}$ and
$\alpha_{p_{2}}$.

Given two elements $q_{1}:A_{1}\approx_{p_{1}}A_{2}$ and
$q_{2}:A_{1}\approx_{p_{2}}A_{2}$, there merely exists a homotopy $h$ between
the equivalences $\alpha_{p_{1}}$ and $\alpha_{p_{2}}$ and a dependent
homotopy between $\beta_{q_{1}}$ and $\beta_{q_{2}}$, over the homotopy $h$.

###### Proof.

By induction on the structure of the contexts and types. In the base case
(${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1})\approx{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{2})$),
we use the fact that $\mathcal{I}_{E}^{\infty}$ is merely $0$-truncated
relatively to $K$. In other cases we use the fact that the $\mathbf{1}$-,
$\Sigma$\- and $\Pi_{\mathsf{rep}}$\- type formers have actions on homotopies
between equivalences. ∎

We can then consider the equivalence relations $(\sim)$ obtained by taking the
propositional truncation of $(\approx)$. The above lemmas approximately say
that $\alpha$ is the functorial action of a $1$-groupoid morphism from the
setoid $(\mathsf{Ob}_{\mathcal{T}_{{\widehat{E}}}},\sim)$ to the $1$-groupoid
of objects of $\mathcal{T}_{{\widehat{E}}}^{\infty}$ and homotopy classes of
equivalences, and analogous statements for $\beta$ and $\beta^{\mathsf{rep}}$.

We will also need the following additional lemmas.

######  Lemma 8.0.

Given elements $p_{1},p_{2}:\Gamma_{1}\approx\Gamma_{2}$ and
$q:A_{1}\approx_{p_{1}}A_{2}$ and a homotopy $h$ between $\alpha_{p_{1}}$ and
$\alpha_{p_{2}}$, we can construct an element of $A_{1}\approx_{p_{2}}A_{2}$.

###### Proof.

By induction over the structure of $A_{1}$ and $A_{2}$.

In the base case,
$q:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1})\approx_{p_{1}}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{2})$,
i.e.

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{1}}(\gamma_{1},\gamma_{2})\vdash
q(\gamma_{e}):K(\sigma_{1})(\gamma_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}K(\sigma_{2})(\gamma_{2}))\in\mathcal{T}_{{\widehat{E}}}^{\infty}.$

By transporting over the homotopy between $\alpha_{p_{1}}$ and
$\alpha_{p_{2}}$, we can construct

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{2}}(\gamma_{1},\gamma_{2})\vdash
q^{\prime}(\gamma_{e}):K(\sigma_{1})(\gamma_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}K(\sigma_{2})(\gamma_{2}))\in\mathcal{T}_{{\widehat{E}}}^{\infty},$

which is an element of
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1})\approx_{p_{2}}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{2})$.

In other cases we use the fact that the $\mathbf{1}$-, $\Sigma$\- and
$\Pi_{\mathsf{rep}}$\- type formers have actions on homotopies between
equivalences. ∎

######  Lemma 8.0.

Given $p:\Gamma_{1}\approx\Gamma_{2}$ and $(\Gamma_{1}\vdash A_{1}\
\mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$, we construct a type $A_{2}$ and
an element $q:A_{1}\approx_{p}A_{2}$.

###### Proof.

By induction over the structure of $A_{1}$.

In the base case,
$A_{1}(\gamma_{2})={\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1}(\gamma_{1}))$
where
$(\Gamma_{1}\vdash\sigma_{1}(\gamma_{1}):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})$.
By transporting $K(\sigma_{1})$ over $\alpha_{p}$, we can find
$(\gamma_{2}:K(\Gamma_{2})\vdash\sigma_{2}(\gamma_{2}):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})$
and

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash\sigma_{e}(\gamma_{e}):K(\sigma_{1})(\gamma_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}\sigma_{2}(\gamma_{2}).$

We then pose
$A_{2}(\gamma_{2})\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(K^{-1}(\sigma_{2})(\gamma_{2}))$,
and we have $\sigma_{e}:A_{1}\approx_{p}A_{2}$.

The recursive cases are straightforward. ∎

######  Lemma 8.0.

Take two types $(\Delta_{1}\vdash A_{1}\ \mathsf{type}),(\Delta_{2}\vdash
A_{2}\ \mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$ and two morphisms
$f_{1}:\Gamma_{1}\to\Delta_{1}$ and $f_{2}:\Gamma_{2}\to\Delta_{2}$. Given
elements $p_{\Gamma}:\Gamma_{1}\approx\Gamma_{2}$,
$p_{\Delta}:\Delta_{1}\approx\Delta_{2}$ and
$q:A_{1}\approx_{p_{\Delta}}A_{2}$ and an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{\Gamma}}(\gamma_{1},\gamma_{2})\vdash
r(\gamma_{e}):\alpha_{p_{\Delta}}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}},$

we can construct an element
$q[r]:A_{1}[f_{1}]\approx_{p_{\Gamma}}A_{2}[f_{2}]$ and a homotopy between
$\alpha_{q[r]}$ and the equivalence $\alpha_{q}[r]:K(A_{1}[f])\simeq
K(A_{2}[f])$.

###### Proof.

By induction over the structure of the types $A_{1}$ and $A_{2}$.

In the base case, we have

$(\delta_{1}:K(\Delta_{1}),\delta_{2}:K(\Delta_{2}),\delta_{e}:\alpha_{p}(\delta_{1},\delta_{2})\vdash
q(\delta_{e}):K(\sigma_{1})(\delta_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}K(\sigma_{2})(\delta_{2}))\in\mathcal{T}_{{\widehat{E}}}^{\infty},$

and we can simply pose $q[r](\gamma_{e})\triangleq q(r(\gamma_{e}))$. It is
then clear that $\alpha_{q[r]}$ and $\alpha_{q}[r]$ are homotopic.

The recursive cases use the fact that the type formers $\Sigma$ and
$\Pi_{\mathsf{rep}}$ preserve homotopies between equivalences. ∎

We now show that these equivalence relations assemble into a fibrant
congruence over $\mathcal{T}_{{\widehat{E}}}$. We start by defining the
equivalence relations, we will prove that the
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF operations are preserved in a second step.

######  Construction 8.0.

We define the data $\widetilde{\mathcal{T}_{{\widehat{E}}}}$ of equivalence
relations and dependent equivalence relations on the objects, morphisms, types
and terms of the CwF $\mathcal{T}_{{\widehat{E}}}$.

  * •

Given $\Gamma_{1},\Gamma_{2}\in\mathcal{T}_{{\widehat{E}}}$, we have
$(\Gamma_{1}\sim\Gamma_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if
there merely exists $p:\Gamma_{1}\approx\Gamma_{2}$.

  * •

Given $(\Gamma_{1}\vdash A_{1}\ \mathsf{type}),(\Gamma_{2}\vdash A_{2}\
\mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$, we have $(A_{1}\sim
A_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if there merely exists
$p:\Gamma_{1}\approx\Gamma_{2}$ and $q:A_{1}\approx_{p}A_{2}$. The relation on
representable types is defined similarly.

  * •

Given $(\Gamma_{1}\vdash a_{1}:A_{1}),(\Gamma_{2}\vdash
a_{2}:A_{2})\in\mathcal{T}_{{\widehat{E}}}$, we have $(a_{1}\sim
a_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if there merely exists
$p:\Gamma_{1}\approx\Gamma_{2}$, $q:A_{1}\approx_{p}A_{2}$ and an
identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
r(\gamma_{e}):\beta_{q}(\gamma_{e},K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

  * •

Given $f_{1}:\Gamma_{1}\to\Delta_{1}$ and $f_{2}:\Gamma_{2}\to\Delta_{2}$, we
have $(f_{1}\sim f_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if there
merely exists $p:\Gamma_{1}\approx\Gamma_{2}$, $q:\Delta_{1}\approx\Delta_{2}$
and an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
r(\gamma_{e}):\alpha_{q}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

The reflexivity, symmetry and transitivity of these relations follow from
section 8.2 and section 8.2.

######  Lemma 8.0.

The dependent equivalence relations of
$\widetilde{\mathcal{T}_{{\widehat{E}}}}$ are fibrant.

###### Proof.

The fibrancy of the relation on types follows from section 8.2. Fibrancy of
the relations on terms and morphisms is proven by transport over the
equivalences $\alpha_{p}$, $\beta_{q}$ and $\alpha_{q}$, along with the fact
that the actions of $K$ on terms are bijective. ∎

######  Lemma 8.0.

Take $p:\Gamma_{1}\approx\Gamma_{2}$ and types $(\Gamma_{1}\vdash A_{1}\
\mathsf{type}),(\Gamma_{2}\vdash A_{2}\
\mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$. Then $(A_{1}\sim
A_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if and only if there merely
exists an element $q:A_{1}\approx_{p}A_{2}$.

###### Proof.

The reverse implication is evident. The forward implication follows from
section 8.2. ∎

######  Lemma 8.0.

Take elements $p:\Gamma_{1}\approx\Gamma_{2}$ and $q:A_{1}\approx_{p}A_{2}$
and terms $(\Gamma_{1}\vdash a_{1}:A_{1}),(\Gamma_{2}\vdash
a_{2}:A_{2})\in\mathcal{T}_{{\widehat{E}}}$. Then $(a_{1}\sim
a_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if and only if there merely
exists an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
r(\gamma_{e}):\beta_{q}(K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

###### Proof.

The reverse implication is evident. For the forward implication, we can find
$p_{a}:\Gamma_{1}\approx\Gamma_{2}$ and $q_{a}:A_{1}\approx_{p_{a}}A_{2}$ and
an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{a}}(\gamma_{1},\gamma_{2})\vdash
r_{a}(\gamma_{e}):\beta_{q_{a}}(K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

By section 8.2, we have homotopies between $\alpha_{p}$ and $\alpha_{p_{a}}$
and between $\beta_{q}$ and $\beta_{q_{a}}$. By transporting over these
homotopies, we obtain

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
r_{a}(\gamma_{e}):\beta_{q}(K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}},$

as needed. ∎

######  Lemma 8.0.

Take elements $p:\Gamma_{1}\approx\Gamma_{2}$ and
$q:\Delta_{1}\approx_{p}\Delta_{2}$ and morphisms
$f_{1}:\Gamma_{1}\to\Delta_{1}$ and $f_{2}:\Gamma_{2}\to\Delta_{2}$. Then
$(f_{1}\sim f_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$ if and only if
there merely exists an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
r(\gamma_{e}):\alpha_{q}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

###### Proof.

Similar to section 8.2. ∎

It remains to prove that these relations are preserved by all
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF operations.

######  Lemma 8.0.

The relations of $\widetilde{\mathcal{T}_{{\widehat{E}}}}$ form a fibrant
congruence over the $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
$\mathcal{T}_{{\widehat{E}}}$.

###### Proof.

We prove that all operations are preserved. The proof is quite lengthy due to
the large number of operations in the theory of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs. However, all cases are rather
straightforward. The main idea is to use section 8.2, section 8.2 and section
8.2 to ensure that we do not obtain different elements of
$\Gamma_{1}\approx\Gamma_{2}$ or $A_{1}\approx_{p}A_{2}$. Section 8.2 is also
needed in the rules that involve substitution.

Identity morphism:

Take $p:\Gamma_{1}\approx\Gamma_{2}$. Then over the context
$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2}))$,
the identification

$(\gamma_{e}:\alpha_{p}(K(\mathsf{id})(\gamma_{1}),K(\mathsf{id})(\gamma_{2})))$

witnesses the fact that
$\mathsf{id}_{\Gamma_{1}}\sim\mathsf{id}_{\Gamma_{2}}$.

Composition of morphisms:

Take morphisms $f_{1}:\Gamma_{1}\to\Delta_{1}$,
$g_{1}:\Delta_{1}\to\Theta_{1}$, $f_{2}:\Gamma_{2}\to\Delta_{2}$ and
$g_{2}:\Delta_{2}\to\Theta_{2}$ such that $f_{1}\sim f_{2}$ and $g_{1}\sim
g_{2}$. Relying on section 8.2, we can find elements
$p_{f}:\Gamma_{1}\approx\Gamma_{2}$, $q_{f}:\Delta_{1}\approx\Delta_{2}$ and
$q_{g}:\Theta_{1}\approx\Theta_{2}$ and identifications

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash
r_{f}(\gamma_{e}):\alpha_{q_{f}}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}$

and

$(\delta_{1}:K(\Delta_{1}),\delta_{2}:K(\Delta_{2}),\delta_{e}:\alpha_{q_{f}}(\delta_{1},\delta_{2})\vdash
r_{g}(\delta_{e}):\alpha_{q_{g}}(K(g_{1})(\delta_{1}),K(g_{2})(\delta_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

We then have, over the context
$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2}))$,
an identification

$(r_{g}(r_{f}(\gamma_{e})):\alpha_{q_{g}}(K(g_{1}\circ
f_{1})(\gamma_{1})),K(g_{2}\circ
f_{2})(\gamma_{2}))\in\mathcal{T}^{\infty}_{{\widehat{E}}},$

witnessing that $(g_{1}\circ f_{1})\sim(g_{2}\circ g_{2})$.

Functorial action on terms:

Similar to composition of morphisms, using section 8.2 instead.

Functorial action on types:

Take morphisms $f_{1}:\Gamma_{1}\to\Delta_{1}$ and
$f_{2}:\Gamma_{2}\to\Delta_{2}$ and types $(\Delta_{1}\vdash A_{1}\
\mathsf{type})$ and $(\Delta_{2}\vdash A_{2}\ \mathsf{type})$ such that
$f_{1}\sim f_{2}$ and $A_{1}\sim A_{2}$.

Using section 8.2, we can find elements $p_{f}:\Gamma_{1}\approx\Gamma_{2}$,
$q_{f}:\Delta_{1}\approx\Delta_{2}$ and $q_{A}:A_{1}\approx_{q_{f}}A_{2}$ and
an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash
r_{f}(\gamma_{e}):\alpha_{q_{f}}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

We then conclude using section 8.2.

Functorial action on representable types:

Similar to the functorial action on types.

Context extension:

Let $(\Gamma_{1}\vdash A_{1}\ \mathsf{type}),(\Gamma_{2}\vdash A_{2}\
\mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$ be two types such that
$A_{1}\sim A_{2}$.

We can find $p:\Gamma_{1}\approx\Gamma_{2}$ and $q:A_{1}\approx_{p}A_{2}$.
Then $(p,q):(\Gamma_{1}.A_{1})\approx(\Gamma_{2}.A_{2})$.

Substitution extension:

Let $(\Delta_{1}\vdash A_{1}\ \mathsf{type}),(\Delta_{2}\vdash A_{2}\
\mathsf{type})\in\mathcal{T}_{{\widehat{E}}}$ be two types such that
$A_{1}\sim A_{2}$, let $f_{1}:\Gamma_{1}\to\Delta_{1}$ and
$f_{2}:\Gamma_{2}\to\Delta_{2}$ be two morphisms such that $f_{1}\sim f_{2}$,
and let $(\Gamma_{1}\vdash a_{1}:A_{1}[f_{1}])$ and $(\Gamma_{2}\vdash
a_{2}:A_{2}[f_{2}])$ be two terms such that $a_{1}\sim a_{2}$.

We can find elements $p_{A}:\Delta_{1}\approx\Delta_{2}$,
$q_{A}:A_{1}\approx_{p_{A}}A_{2}$, $p_{f}:\Gamma_{1}\approx\Gamma_{2}$,
$q_{f}:\Delta_{1}\approx\Delta_{2}$ along with identifications

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash
r_{f}(\gamma_{e}):\alpha_{q_{f}}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

By section 8.2, we have $q_{A}[r_{f}]:A_{1}[f_{1}]\approx_{p_{f}}A_{2}[f_{2}]$
and a homotopy between $\beta_{q_{A}[r_{f}]}$ and $\beta_{q_{A}}[r_{f}]$.

Using section 8.2, we can then find

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash
r_{a}(\gamma_{e}):\beta_{q_{A}[r_{f}]}(K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}$

The homotopy between $\beta_{q_{A}[r_{f}]}$ and $\beta_{q_{A}}[r_{f}]$ has an
underlying transport function

$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2}),a_{1},a_{2},a_{e}:\beta_{q_{A}[r_{f}]}(\gamma_{e},a_{1},a_{2})\vdash
h(\gamma_{e},a_{e}):q_{A}(r_{f}(\gamma_{e}),a_{1},a_{2})).$

Then the identification

$((r_{f}(\gamma_{e}),h(\gamma_{e},r_{a}(\gamma_{e}))):\alpha_{p_{A},q_{A}}(K({\left\langle
f_{1},a_{1}\right\rangle})(\gamma_{1}),K({\left\langle
f_{2},a_{2}\right\rangle})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}$

over the context
$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2}))$
witnesses that ${\left\langle f_{1},a_{1}\right\rangle}\sim{\left\langle
f_{2},a_{2}\right\rangle}$.

Substitution projections:

Let $f_{1}:\Gamma_{1}\to\Delta_{1}.A_{1}$ and
$f_{2}:\Gamma_{2}\to\Delta_{2}.A_{2}$ be two morphisms such that $f_{1}\sim
f_{2}$ and $A_{1}\sim A_{2}$.

Using section 8.2, we can find elements $p_{f}:\Delta_{1}\approx\Delta_{2}$,
$p_{A}:\Gamma_{1}\approx\Gamma_{2}$, $q_{A}:A_{1}\approx_{p_{A}}A_{2}$ and an
identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash
r_{f}(\gamma_{e}):\alpha_{(p_{A},q_{A})}(K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

By definition of $\alpha_{(p_{A},q_{A})}$, we can decompose $r_{f}$ into
identifications

$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash\pi_{1}(r_{f})(\gamma_{e}):\alpha_{p_{A}}(K(\pi_{1}(f_{1}))(\gamma_{1})),K(\pi_{1}(f_{2}))(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}$

and

$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{f}}(\gamma_{1},\gamma_{2})\vdash\pi_{2}(r_{f})(\gamma_{e}):\beta_{q_{A}}(\pi_{1}(r_{f})(\gamma_{e}),K(\pi_{2}(f_{1}))(\gamma_{1})),K(\pi_{2}(f_{2}))(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

Then $\pi_{1}(r_{f})$ witnesses the fact that
$\pi_{1}(f_{1})\sim\pi_{1}(f_{2})$.

By section 8.2, we have an element
$q_{A}[r_{f}]:A_{1}[\pi_{1}(r_{f})]\approx_{p_{f}}A_{2}[\pi_{2}(r_{f})]$ and a
homotopy between $\beta_{q_{A}[r_{f}]}$ and $\beta_{q_{A}}[r_{f}]$. Up to
transport over this homotopy, $\pi_{2}(r_{f})$ witnesses the fact that
$\pi_{2}(f_{1})\sim\pi_{2}(f_{2})$.

$\mathbf{1}$-type structure:

Straightforward. Note that we also need to consider the $\mathbf{1}$-type
structure on representable types.

$\Sigma$-type structure:

Similar to context extensions, substitution extension and substitution
projections. We also need to consider the $\Sigma$-type structure on
representable types.

$\Pi_{\mathsf{rep}}$-type structure:

Type former:

Let $(\Gamma_{1}.A_{1}\vdash B_{1}\ \mathsf{type}),(\Gamma_{2}.A_{2}\vdash
B_{2}\ \mathsf{type})$ be two dependent types such that $A_{1}\sim A_{2}$ and
$B_{1}\sim B_{2}$. Using section 8.2, we can find
$p_{A}:\Gamma_{1}\approx\Gamma_{2}$,
$q_{A}:A_{1}\approx^{\mathsf{rep}}_{p_{A}}A_{2}$ and
$q_{B}:B_{1}\approx_{(p_{A},q_{A})}B_{2}$. Then
$(q_{A},q_{B}):\Pi_{\mathsf{rep}}(A_{1},B_{1})\approx_{p_{A}}\Pi_{\mathsf{rep}}(A_{2},B_{2})$,
as needed.

Application:

Let $(\Gamma_{1}\vdash
f_{1}:\Pi_{\mathsf{rep}}(A_{1},B_{1})),(\Gamma_{2}\vdash
f_{2}:\Pi_{\mathsf{rep}}(A_{2},B_{2}))$ be two terms such that $f_{1}\sim
f_{2}$, and $(\Gamma_{1}\vdash a_{1}:A_{1}),(\Gamma_{2}\vdash a_{2}:A_{2})$ be
two terms such that $a_{1}\sim a_{2}$. We have $p_{A}$, $q_{A}$ and $q_{B}$ as
before.

Using section 8.2, we can find identifications

$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{A}}(\gamma_{1},\gamma_{2})\vdash
r_{f}(\gamma_{e}):\beta_{(q_{A},q_{B})}(\gamma_{e},K(f_{1})(\gamma_{1}),K(f_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}$

and

$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{A}}(\gamma_{1},\gamma_{2})\vdash
r_{a}(\gamma_{e}):\beta_{q_{A}}(\gamma_{e},K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

By definition of $\beta_{(q_{A},q_{B})}$, we can apply $r_{f}(\gamma_{e})$ to
$r_{a}(\gamma_{e})$ to obtain an identification in

$\beta_{q_{B}}(\gamma_{e},K(\mathsf{app}(f_{1},a_{1}))(\gamma_{1}),K(\mathsf{app}(f_{2},a_{2}))(\gamma_{2}))$

witnessing that $\mathsf{app}(f_{1},a_{1})\sim\mathsf{app}(f_{2},a_{2})$.

Lambda:

Let $(\Gamma_{1}.A_{1}\vdash b_{1}:B_{1}),(\Gamma_{2}.A_{1}\vdash
b_{2}:B_{2})$ be two terms such that $b_{1}\sim b_{2}$. We have $p_{A}$,
$q_{A}$ and $q_{B}$ as before. By section 8.2, we can find an identification

$(r_{b}(\gamma_{e},a_{e}):\beta_{q_{B}}((\gamma_{e},a_{e}),K(b_{1})(\gamma_{1},a_{1}),K(b_{2})(\gamma_{2},a_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}$

over the context
$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{A}}(\gamma_{1},\gamma_{2}),a_{1},a_{2},a_{e}:\beta_{q_{A}}(a_{1},a_{2}))$.

By definition of $\beta_{(q_{A},q_{B})}$, we can construct an element

$\displaystyle\mathsf{lam}(\lambda(a_{1}:A_{1})\
((a_{2},a_{e}):=\overrightarrow{\beta_{q_{A}}}(a_{1}))\mapsto
r_{b}(\gamma_{e},a_{e}))$
$\displaystyle\quad:\beta_{(q_{A},q_{B})}(\gamma_{e},K(\mathsf{lam}(b_{1}))(\gamma_{1}),K(\mathsf{lam}(b_{2})(\gamma_{2})))$

over the context
$(\gamma_{1},\gamma_{2},\gamma_{e}:\alpha_{p_{A}}(\gamma_{1},\gamma_{2}))$.
Thus $\mathsf{lam}(b_{1})\sim\mathsf{lam}(b_{2})$, as needed. ∎

######  Lemma 8.0.

Given $p:\Gamma_{1}\approx\Gamma_{2}$ we have $F(\Gamma_{1})=F(\Gamma_{2})$
and $G(\alpha_{p})$ is (homotopic to) the identity equivalence in
$\mathcal{T}_{E}^{1}$.

Given $q:A_{1}\approx_{p}A_{2}$ we have $F(A_{1})=F(A_{2})$ and $G(\beta_{p})$
is (homotopic to) the identity equivalence in $\mathcal{T}_{E}^{1}$.

###### Proof.

By mutual induction on the structure of contexts and terms.

The recursive cases follow from the fact that $F$ is a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism, that $G$ is a
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-morphism and that the
constructions of $\alpha_{p}$ and $\beta_{q}$ preserve identity equivalences.

In the base case, we have
$q:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{1})\approx_{p}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma_{2})$,
i.e.

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
q(\gamma_{e}):K(\sigma_{1})(\gamma_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}K(\sigma_{2})(\gamma_{2}))\in\mathcal{T}_{{\widehat{E}}}^{\infty}.$

By applying $G$, we obtain

$(\gamma_{1},\gamma_{2},\gamma_{e}:G(\alpha_{p})(\gamma_{1},\gamma_{2})\vdash
G(q)(\gamma_{e}):G(K(\sigma_{1}))(\gamma_{1})\simeq_{\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}}G(K(\sigma_{2}))(\gamma_{2}))\in\mathcal{T}_{E}^{1}.$

By the induction hypothesis, $F(\Gamma_{1})=F(\Gamma_{2})$ and $\alpha_{p}$ is
the identity equivalence. We also recall that $\mathcal{T}_{E}^{1}$ satisfies
equality reflection. This implies that $G(K(\sigma_{1}))=G(K(\sigma_{2}))$, or
equivalently $L(F(\sigma_{1}))=L(F(\sigma_{2}))$. Since the actions of $L$ on
terms are bijective, we have $F(\sigma_{1})=F(\sigma_{2})$. Furthermore, since
$G(\alpha_{q})$ is an equivalence defined by transport over an equality, it is
the identity equivalence, as needed. ∎

######  Lemma 8.0.

We have $\widetilde{\mathcal{T}_{{\widehat{E}}}}\subseteq\ker_{F}$.

###### Proof.

We prove the inclusions of the relations for each sort.

  * •

Take $(\Gamma_{1}\sim\Gamma_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$.
We have some $p:\Gamma_{1}\approx\Gamma_{2}$. By section 8.2,
$F(\Gamma_{1})=F(\Gamma_{2})$, as needed.

  * •

Take $(A_{1}\sim A_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$. We have
some $q:A_{1}\approx_{p}A_{2}$. By section 8.2, $F(A_{1})=F(A_{2})$, as
needed.

  * •

Take $(a_{1}\sim a_{2})\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$. We have
some $q:A_{1}\approx_{p}A_{2}$ and an identification

$(\gamma_{1}:K(\Gamma_{1}),\gamma_{2}:K(\Gamma_{2}),\gamma_{e}:\alpha_{p}(\gamma_{1},\gamma_{2})\vdash
r(\gamma_{e}):\beta_{q}(K(a_{1})(\gamma_{1}),K(a_{2})(\gamma_{2})))\in\mathcal{T}^{\infty}_{{\widehat{E}}}.$

By section 8.2, we know that $F(A_{1})=F(A_{2})$ and that $G(\beta_{q})$ is
the identity equivalence in $\mathcal{T}_{E}^{1}$. Therefore, $G(r)$ proves
that $G(K(a_{1}))=G(K(a_{2}))$ in $\mathcal{T}_{E}^{1}$, or equivalently
$L(F(a_{1}))=L(F(a_{2}))$. Since the actions of $L$ on terms are bijective, we
have $F(a_{1})=F(a_{2})$, as needed.

  * •

The case of morphisms is similar to the case of terms. ∎

######  Lemma 8.0.

For every marked homotopy

$(\gamma:\Gamma\vdash
h(\gamma):x(\gamma)\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}y(\gamma))\in
E,$

we have $(x\sim y)\in\widetilde{\mathcal{T}_{{\widehat{E}}}}$

###### Proof.

Take a marked homotopy $h$ as in the statement.

Let $p:\Gamma\approx\Gamma$ and
$q:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)\approx_{p}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)$
be $r_{\Gamma}$ and
$r_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}$
from section 8.2.

It then suffices to construct an element of type

$\alpha_{q}(K(x)(\gamma_{1}),K(y)(\gamma_{2}))$

over the context
$(\gamma_{1}:K(\Gamma),\gamma_{2}:K(\Gamma),\alpha_{p}(\gamma_{1},\gamma_{2}))$.

Since $\alpha_{p}$ and $\alpha_{q}$ are homotopic to identity equivalences, it
suffices to construct an element of type

$K(x)(\gamma)\simeq K(y)(\gamma)$

over the context $(\gamma:K(\Gamma))$.

We can then pick the element $\widehat{h}(\gamma):K(x)(\gamma)\simeq
K(y)(\gamma)$. ∎

###  8.3. Proof of the main theorem

We can now prove section 8.

###### Proof of section 8.

We have constructed a fibrant congruence
$\widetilde{\mathcal{T}_{{\widehat{E}}}}$ over the
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF $\mathcal{T}_{{\widehat{E}}}$ and we can
consider the quotient $\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})$ in
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF.

By section 7.3, the quotient inclusion
$\mathbf{q}:\mathcal{T}_{{\widehat{E}}}\to\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})$
is a non-split trivial fibration.

By section 8.2 and the universal property of the quotient, the map
$F:\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ factors through the quotient
inclusion. We obtain a map
$R:\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})\to\mathcal{T}_{E}$.

By section 8.2 and the universal property of $\mathcal{T}_{E}$, we obtain a
section
$S:\mathcal{T}_{E}\to\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})$.

${\mathbf{Q}(\widetilde{\mathcal{T}_{{\widehat{E}}}})}$${\mathcal{T}_{{\widehat{E}}}}$${\mathcal{T}_{E}}$$\scriptstyle{R}$$\scriptstyle{F}$$\scriptstyle{\mathbf{q}}$$\scriptstyle{S}$

The map $F$ is then a section of the quotient inclusion $\mathbf{q}$. Since
non-split trivial fibrations are closed under retracts, the map $F$ is a non-
split trivial fibration. ∎

Our main theorem directly follows.

###### Proof of section 6.3.

By section 6.3 the map $\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}$ is a weak
equivalence in $\mathbf{Mod}_{\mathcal{T}}$. By section 8 the map
$\mathcal{T}\to\mathcal{T}_{E}$ is a non-split trivial fibration in
$\mathbf{CwF}_{\Sigma},\Pi_{\mathsf{rep}}$, hence a non-split weak equivalence
in $\mathbf{Mod}_{\mathcal{T}}$. Their composite
$\mathcal{T}\to\mathcal{T}_{E}$ is then also a non-split weak equivalence in
$\mathbf{Mod}_{\mathcal{T}}$. ∎

##  9\. Future directions

###  9.1. Alternative proofs of theorem 8.1

The proof of section 8 is very close to Hofmann’s original proof of the
conservativity of extensional type theory over intensional type theory. We
discuss potential ways to obtain simpler proofs of section 8.

#### Local universes

In presence of enough universes in $\mathcal{T}_{\widehat{E}}^{\infty}$, there
would be a simpler way to define the relations of the congruence
$\widetilde{\mathcal{T}_{\widehat{E}}}$. Indeed, we could say that
$(\Gamma\sim\Delta)\in\widetilde{\mathcal{T}_{\widehat{E}}}$ when there merely
exists
$p:\mathsf{code}(K(\Gamma))\simeq_{\mathcal{U}}\mathsf{code}(K(\Delta))$,
where $\mathsf{code}(-)$ gives the code of a context or type in the universe.

In the absence of universe, we can try to use local universes. A local
universe in $\mathcal{T}_{\widehat{E}}^{\infty}$ is a type $(V\vdash E\
\mathsf{type})\in\mathcal{T}_{\widehat{E}}^{\infty}$. By induction on the
shape of contexts and types of $\mathcal{T}_{\widehat{E}}$, we would define
for every $\Gamma\in\mathcal{T}_{\widehat{E}}$ a local universe
$(V_{\Gamma},E_{\Gamma})$ and an element
$(\chi_{\Gamma}:V_{\Gamma})\in\mathcal{T}_{\widehat{E}}^{\infty}$ such that
$K(\Gamma)=E_{\Gamma}[\chi_{\Gamma}]$. We could then say that
$(\Gamma\sim\Delta)\in\widetilde{\mathcal{T}_{\widehat{E}}}$ when
$(V_{\Gamma},E_{\Gamma})=(V_{\Delta},E_{\Delta})$ and there merely exists
$p:\chi_{\Gamma}\simeq_{V_{\Gamma}}\chi_{\Delta}$.

Unfortunately, it is not possible to define these local universes: we would
need arbitrary $\Pi$-types in $\mathcal{T}_{\widehat{E}}^{\infty}$, but we
only have $\Pi_{\mathsf{rep}}$-types. If we could conservatively embed
$\mathcal{T}_{\widehat{E}}^{\infty}$ into a $(\Sigma,\Pi,{\mathsf{Id}})$-CwF,
this method would be applicable.

#### Higher-order congruences

Another possible simplification would be obtained by working internally to
$\mathbf{Psh}(\mathcal{T}_{{\widehat{E}}})$ instead of externally.

Consider the following external diagram:

${\mathcal{T}}$${\mathcal{T}_{E}}$${\mathcal{T}_{{\widehat{E}}}}$${\mathcal{T}_{E}}$${\mathcal{T}_{{\widehat{E}}}^{\infty}}$${\mathcal{T}_{E}^{1}\hbox
to0.0pt{\
.\hss}}$$\scriptstyle{F}$$\scriptstyle{K}$$\scriptstyle{L}$$\scriptstyle{G}$

Following ideas from [BKS23], it is possible to internalize this diagram
internally to $\mathbf{Psh}(\mathcal{T}_{{\widehat{E}}})$ as follows:

${\mathcal{T}}$${\mathcal{T}_{E}}$${\mathbf{Tele}_{\mathbb{T}_{{\widehat{E}}}}}$${\mathcal{I}_{E}}$${\mathcal{I}_{{\widehat{E}}}^{\infty}}$${\mathcal{I}_{E}^{1}\hbox
to0.0pt{\ .\hss}}$

Here $\mathbf{Tele}_{\mathbb{T}_{{\widehat{E}}}}$ is an internal
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF called the _telescopic contextualization_ of
the family $\mathbb{T}_{{\widehat{E}}}$; its contexts are the telescopes of
the family $\mathbb{T}_{{\widehat{E}}}$. Similarly,
$\mathcal{I}_{{\widehat{E}}}^{\infty}$, $\mathcal{I}_{E}$ and
$\mathcal{I}_{E}^{1}$ are internalization of $\mathcal{T}_{{\widehat{E}}}$,
$\mathcal{T}_{E}$ and $\mathcal{T}_{E}^{1}$. Using the restriction operation
from [BKS23], they would be defined as
$\mathcal{I}_{{\widehat{E}}}^{\infty}\triangleq
K^{\ast}(\mathbf{Tele}_{\mathbb{T}_{\widehat{E}}^{\infty}})$,
$\mathcal{I}_{E}\triangleq F^{\ast}(\mathbf{Tele}_{\mathbb{T}_{E}})$ and
$\mathcal{I}_{{\widehat{E}}}^{\infty}\triangleq
K^{\ast}(G^{\ast}(\mathbf{Tele}_{\mathbb{T}_{E}^{1}}))$. The internal versions
of $\mathcal{T}$ and $\mathcal{T}_{E}$ should be constant over , i.e. defined
by restriction of their external counterparts over the unique functor
$\mathcal{T}_{{\widehat{E}}}\to 1_{\mathbf{Cat}}$.

It should then be possible to define a “higher-order congruence” over
$\mathbb{T}_{{\widehat{E}}}$. The advantage of this approach is that higher-
order congruences only consist of equivalence relations on types and terms,
not on contexts and substitutions; we would avoid the parts of the current
proof that have to deal with contexts and substitutions.

This higher-order congruence should induce a fibrant “first-order” congruence
over the $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
$\mathbf{Tele}_{\mathbb{T}_{\widehat{E}}}$. We can then consider the internal
quotient of this fibrant congruence; it fits in the following diagram.

${\mathcal{T}}$${\mathcal{T}_{E}}$${Q}$${\mathbf{Tele}_{\mathbb{T}_{{\widehat{E}}}}}$${\mathcal{I}_{E}\hbox
to0.0pt{\ .\hss}}$

By externalizing the above diagram, i.e. restricting it along the functor
$1_{\mathcal{T}_{{\widehat{E}}}}:1_{\mathbf{Cat}}\to\mathcal{T}_{{\widehat{E}}}$,
we obtain the following external diagram:

${\mathcal{T}}$${\mathcal{T}_{E}}$${1_{\mathcal{T}_{\widehat{E}}}^{\ast}(Q)}$${\mathcal{T}_{{\widehat{E}}}}$${\mathcal{T}_{E}\hbox
to0.0pt{\ .\hss}}$

We would then conclude as before, by observing that
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ becomes a retract of the
quotient inclusion $\mathcal{T}_{{\widehat{E}}}\to
1_{\mathcal{T}_{\widehat{E}}}^{\ast}(Q)$.

This proof strategy requires some additional tools for axiomatizing models,
morphisms of models and their properties in the internal language of presheaf
toposes.

###  9.2. Conjectures

This paper includes several conjectures (section 4.4, section 4.6, section
5.2, section 5.3, section 6.2).

The first three conjectures (section 4.4, section 4.6 and section 5.2) should
be mostly unproblematic, at least in a classical setting; The author has
already drafts of their proofs. It may however be rather difficult to obtain
constructive proofs.

Results analogous to section 4.4 are well-known for algebraic theories and
essentially algebraic theories, and it is possible to extend these results to
first-order GATs. For SOGATs, it seems that the simplest approach is a
reduction to first-order GATs. Indeed, the underlying $\Sigma$-CwF of a SOGAT
$\mathcal{T}$ is a first-order GAT that classifies the contextual models of
$\mathcal{T}$ (see [Uem19, Theorem 7.30]).

Proving section 4.6 is mainly a matter of translating between the weakly
stable identity types of $\mathcal{T}$ and properties of the weak
factorization systems of $\mathbf{Mod}_{\mathcal{T}}^{\mathsf{cxl}}$ with
regard to the fully faithful functor
$\mathbf{0}_{\mathcal{T}}[-]:\mathcal{T}^{\mathsf{op}}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{cxl}}$.
The theory $\mathcal{T}$ being finitary explains why considering the finitely
generated models of $\mathcal{T}$ suffices.

The proof of section 5.2 has already been sketched in section 5.2.

Section 5.3 should follow from strictification theorems for weakly stable
identity types. An approach for solving these coherence problems is discussed
in section 9.3.

Section 6.2 should follow from gluing arguments that are very similar to the
gluing arguments used in the proofs of section 6.2. The main issue is that one
likely has to use the internal language of some $\infty$-topos, which is not
easily available in our setting. A possible solution is also discussed in
section 9.3.

###  9.3. Coherence problems and the Yoneda embedding

Coherence problems arise from the use of $(\Sigma,{\mathsf{Id}})$\- or
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$\- CwFs to morally represent
structured $\infty$-categories. In particular, the notion of external
univalence is expressed using weakly stable identity types. Thus, in order to
rely on external univalence, the two choices are either to only use weakly
stable identity types, or to prove coherence theorem that allow for the
strictification of the weakly stable identity types.

The Yoneda embedding is one of the most important constructions of category
theory. For applications, it seems very important to access the
$\infty$-categorical Yoneda embedding at the level of
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs. If $\mathcal{C}$ is a
cofibrant $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF, it should be
possible to find a model $\mathcal{D}$ of HoTT (corresponding to
$\infty$-presheaves over $\mathcal{C}$) and a
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF morphism
$\mathcal{C}\to\mathcal{D}$ that is essentially surjective on terms
(corresponding to the fully faithful Yoneda embedding).

We hope that both of these issues will be solved in the future using cubical
methods, thanks to the fact that the cubical model of HoTT is constructive
(using a suitable cube category). If $\mathcal{C}$ is any $1$-category with a
terminal object, then the category $[\mathcal{C}^{\mathsf{op}},\mathbf{cSet}]$
of cubical presheaves is equipped with a model of HoTT. Indeed, we can
construct the cubical set model internally to $\mathbf{Psh}(\mathcal{C})$.
This internal construction corresponds externally to a functor
$\mathcal{C}\to\mathbf{Mod}_{\mathsf{HoTT}}^{\mathsf{op}}$. By composing this
functor with
$1_{\mathcal{C}}:1_{\mathbf{Cat}}^{\mathsf{op}}\to\mathcal{C}^{\mathsf{op}}$,
we obtain an external model of HoTT; it can be shown that its underlying
category is the category $[\mathcal{C}^{\mathsf{op}},\mathbf{cSet}]$ of
cubical presheaves over $\mathcal{C}$. When $\mathcal{C}$ is a
$(\Sigma,{\mathsf{Id}})$-CwF or a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF, we then
want to compare $\mathcal{C}$ with this model
$[\mathcal{C}^{\mathsf{op}},\mathbf{cSet}]$. It should then suffice to
compare, internally to $\mathbf{Psh}(\mathcal{C})$, the CwF
$\mathrm{Set}_{\mathsf{rf}}$ of sets and Reedy-fibrant types with the cubical
set model $\mathsf{cSet}$. This problem seems tractable (using, for example,
ideas from two-level type theory (2LTT) and the development of Reedy-fibrant
diagrams in 2LTT [ACKS17]).

###  9.4. Proving $0$-truncatedness from normalization

In order to apply our methods, we would need to be able to prove the
(relative) $0$-truncatedness of $\mathcal{T}_{\widehat{E}}^{\infty}$ in
concrete examples. We believe that such results can be obtained by lifting
normalization proofs from $\mathcal{T}_{E}$ to
$\mathcal{T}_{{\widehat{E}}}^{\infty}$. These normalization results should
even provide direct proofs of the fact that
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ is a _split_ trivial
fibration, without going through any quotient.

Strict normalization for $\mathcal{T}_{E}$ states that every term of
$\mathcal{T}_{E}$ admits a unique normal form. Normalization is usually proven
for the syntax of type theory, that is for the initial model
$\mathbf{0}_{\mathcal{T}_{E}}$. Proving normalization for $\mathcal{T}_{E}$
instead is akin to proving normalization for all freely generated models of
$\mathcal{T}_{E}$ at once. For most theories, proving normalization for
$\mathcal{T}_{E}$ is not more complicated than proving normalization for
$\mathbf{0}_{\mathcal{T}_{E}}$.

Homotopy normalization for $\mathcal{T}_{{\widehat{E}}}^{\infty}$ should then
state that every term of $\mathcal{T}_{{\widehat{E}}}^{\infty}$ admits a
contractible space of normal forms (over contexts in the image of
$\mathcal{T}\to\mathcal{T}_{\widehat{E}}^{\infty}$). Stated appropriately,
this is sufficient to obtain the $0$-truncatedness of
$\mathcal{T}_{\widehat{E}}^{\infty}$. Proving homotopy normalization for
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ is however much more complicated than
proving strict normalization. Indeed, where strict normalization proofs for
type theory make use of set-valued logical relations, homotopy normalization
proofs should use space-valued logical relations.

For this we essentially need to use $\infty$-presheaves over some
$\infty$-categories, and the interpretation of HoTT into $\infty$-toposes. But
because we have used $(\Sigma,{\mathsf{Id}})$-CwFs or
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs instead of other models of
$\infty$-categories, we cannot directly use the known interpretation of HoTT
into $\infty$-toposes. Hopefully, the cubical methods mentioned in section 9.3
can be used instead.

We note that Uemura has recently written a proof of normalization and
$0$-truncatedness for the initial models of $\infty$-type theories [Uem22].
Only a small $\infty$-type theory with only $\Pi$-types has been considered so
far, but the methods should also work for other $\infty$-type theories. It
does not seem realistic to directly use these results for our purposes
(although it would be possible in principle, given a precise comparison
between $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs and $\infty$-type
theories (representable map $\infty$-categories)). But the fact that
$0$-truncatedness results can be obtained for $\infty$-type theories indicates
that similar methods should also yield the $0$-truncatedness results we need.

## Acknowledgements

The author would like to thank Thorsten Altenkirch, Martin Bidlingmaier, Paolo
Capriotti, Thierry Coquand, Simon Huber, Ambrus Kaposi, András Kovács, Nicolai
Kraus, Chaitanya Leena Subramaniam, Christian Sattler and Bas Spitters for
expressing interest in this work and helpful discussions.

## References

  * [ACC+17] Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, Simon Huber, and Nicolai Kraus.  Type Theory with Weak J.  23rd International Conference on Types for Proofs and Programs, 2017.
  * [ACKS17] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler.  Two-level type theory and applications.  CoRR, abs/1705.03307, 2017.
  * [Acz95] Peter Aczel.  Galois: a theory development project.  Report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks, 1995.
  * [AMB13] Guillaume Allais, Conor McBride, and Pierre Boutillier.  New equations for neutral terms: a sound and complete decision procedure, formalized.  In Stephanie Weirich, editor, Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013, pages 13–24. ACM, 2013.
  * [AW09] Steve Awodey and Michael A. Warren.  Homotopy theoretic models of identity types.  Math. Proc. Cambridge Philos. Soc., 146(1):45–55, 2009.
  * [Awo18] Steve Awodey.  Natural models of homotopy type theory.  Math. Struct. Comput. Sci., 28(2):241–286, 2018.
  * [BKS23] Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler.  For the metatheory of type theory, internal sconing is enough.  CoRR, abs/2302.05190, 2023.
  * [Boc22] Rafaël Bocquet.  External univalence for second-order generalized algebraic theories.  CoRR, abs/2211.07487, 2022.
  * [Bru16] Guillaume Brunerie.  On the homotopy groups of spheres in homotopy type theory.  CoRR, abs/1606.05916, 2016.
  * [Bru18] Guillaume Brunerie.  Computer-generated proofs for the monoidal structure of the smash product.  HoTTEST electronic seminar, Nov 2018.
  * [CCD19] Simon Castellan, Pierre Clairambault, and Peter Dybjer.  Categories with families: Unityped, simply typed, and dependently typed.  CoRR, abs/1904.00827, 2019.
  * [CCHM17] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg.  Cubical type theory: A constructive interpretation of the univalence axiom.  FLAP, 4(10):3127–3170, 2017.
  * [Gal14] Cesare Gallozzi.  Constructive set theory from a weak tarski universe, 2014.
  * [Gar09] Richard Garner.  Two-dimensional models of type theory.  Mathematical Structures in Computer Science, 19(4):687–736, 2009\.
  * [GCST19] Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.  Definitional proof-irrelevance without K.  Proc. ACM Program. Lang., 3(POPL):3:1–3:28, 2019.
  * [GG08] Nicola Gambino and Richard Garner.  The identity type weak factorisation system.  Theoretical Computer Science, 409, 05 2008.
  * [GS20] Daniel Gratzer and Jonathan Sterling.  Syntactic categories for dependent type theory: sketching and adequacy.  CoRR, abs/2012.10783, 2020.
  * [Hof95] Martin Hofmann.  Conservativity of equality reflection over intensional type theory.  In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 153–164. Springer, 1995.
  * [HS94] Martin Hofmann and Thomas Streicher.  The groupoid model refutes uniqueness of identity proofs.  In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS ’94), Paris, France, July 4-7, 1994, pages 208–212. IEEE Computer Society, 1994.
  * [Isa18a] Valery Isaev.  Model structures on categories of models of type theories.  Mathematical Structures in Computer Science, 28(10):1695–1722, 2018\.
  * [Isa18b] Valery Isaev.  Morita equivalences between algebraic dependent type theories.  CoRR, abs/1804.05045, 2018.
  * [Isa21] Valery Isaev.  Indexed type theories.  Mathematical Structures in Computer Science, 31(1):3–63, 2021\.
  * [JS91] André Joyal and Ross Street.  The geometry of tensor calculus, i.  Advances in Mathematics, 88(1):55–112, 1991.
  * [KL16] Chris Kapulkin and Peter Lumsdaine.  The homotopy theory of type theories.  Advances in Mathematics, 337, 09 2016.
  * [KL21a] Chris Kapulkin and Peter Lumsdaine.  The simplicial model of Univalent Foundations (after Voevodsky).  Journal of the European Mathematical Society, 23(6):2071–2126, 2021\.
  * [KL21b] Krzysztof Kapulkin and Peter LeFanu Lumsdaine.  Homotopical inverse diagrams in categories with attributes.  Journal of Pure and Applied Algebra, 225(4):106563, 2021.
  * [Kov22] András Kovács.  Staged compilation with two-level type theory.  Proc. ACM Program. Lang., 6(ICFP):540–569, 2022.
  * [KS17] Chris Kapulkin and Karol Szumiło.  Internal language of finitely complete $(\infty,1)$-categories.  Selecta Mathematica, 25, 09 2017.
  * [Lan63] Saunders Mac Lane.  Natural associativity and commutativity.  Rice University Studies, 1963.
  * [Nor19] Paige Randall North.  Identity types and weak factorization systems in cauchy complete categories.  Math. Struct. Comput. Sci., 29(9):1411–1427, 2019.
  * [NU22] Hoang Kim Nguyen and Taichi Uemura.  $\infty$-type theories, 2022.
  * [Our05] Nicolas Oury.  Extensionality in the calculus of constructions.  In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 278–293. Springer, 2005.
  * [Pal17] Erik Palmgren.  On equality of objects in categories in constructive type theory.  In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, volume 104 of LIPIcs, pages 7:1–7:7. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [Shu19] Michael Shulman.  All $(\infty,1)$-toposes have strict univalent universes.  arXiv: Algebraic Topology, 2019.
  * [Uem19] Taichi Uemura.  A general framework for the semantics of type theory.  CoRR, abs/1904.04097, 2019.
  * [Uem22] Taichi Uemura.  Normalization and coherence for $\infty$-type theories.  CoRR, abs/2212.11764, 2022.
  * [vdB18] Benno van den Berg.  Path categories and propositional identity types.  ACM Trans. Comput. Log., 19(2):15:1–15:32, 2018.
  * [WST19] Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau.  Eliminating reflection from type theory.  In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 91–103. ACM, 2019.