# Towards coherence theorems for equational extensions of type theories

Rafaël Bocquet  Department of Programming Languages and Compilers, Eötvös
Loránd University, Budapest, Hungary<EMAIL_ADDRESS>https://rafaelbocquet.gitlab.io/

###### Abstract.

We study the conservativity of extensions by additional strict equalities of
dependent type theories (and more general second-order generalized algebraic
theories). The conservativity of Extensional Type Theory over Intensional Type
Theory was proven by Hofmann. Our goal is to generalize such results to type
theories without the Uniqueness of Identity Proofs principles, such as
variants of Homotopy Type Theory.

For this purpose, we construct what is essentially the $\infty$-congruence on
the base theory that is freely generated by the considered equations. This
induces a factorization of any equational extension, whose two factors can be
studied independently. We conjecture that the first factor is always an
equivalence when the base theory is well-behaved. We prove that the second
factor is an equivalence when the $\infty$-congruence is $0$-truncated.

###### Key words and phrases:

conservativity, coherence, strictification, dependent type theory, homotopy
type theory, definitional equalities, strict equalities

The author was supported by the European Union, co-financed by the European
Social Fund (EFOP-3.6.3-VEKOP-16-2017-00002).

##  1\. Introduction

Equality and computation are central components of type theories. The
computational content of a type theory is presented by computation rules
(often called $\beta$-rules, or $\iota$-rules for inductive types), and
perhaps uniqueness rules (usually called $\eta$-rules) or more exotic rules
(such as the $\nu$-rules considered in [AMB13]). This computational content is
typically explained by the means of a normalization algorithm. In presence of
identity types, there is a distinction between two notions of equality or
identification between terms of a type theory. Internally, the identity types
provide the notion of _internal identification_ , also called _propositional
equality_ or _typal equality_. Externally, we can also compare terms up to
_strict equality_ , which is the proof-irrelevant equality of our metatheory.
Strict equality is also often called _definitional_ or _judgemental_ equality.

When working internally to a type theory, it is desirable to have as many
strict equalities as possible. Indeed, strict equality can be implicitly and
silently coerced over. On the other hand, internal identifications require
explicit transports and coercions, which quickly clutter the terms of the
theory. Conversely, the trade-off is that type theories with additional strict
equalities have fewer models, and their semantics are therefore more
complicated.

Hofmann proved in [Hof95] a conservativity theorem, showing that all internal
identifications in a type theory can conservatively be turned into strict
equalities, when the base type theory satisfies some principles. The most
important of these principles is the Uniqueness of Identity Proofs (UIP)
principle, which states that there is an identification between any two
elements of identity types. A more syntactic proof was later given by Oury
[Our05] for the calculus of constructions. Oury’s proof had some issues,
mainly due to a presentation of the syntax of type theory with too few
annotations. An improvement of Oury’s proof and a presentation of this result
as a constructive and effective syntactic translation has been given recently
by Winterhalteret al. [WST19].

Since Hofmann’s proof of conservativity, there has been a lot of interest
going into the study of type theories with non-trivial higher dimensional
content inconsistent with UIP [HS94], and their semantics in homotopy
theoretic [AW09, KL21a] and $\infty$-categorical structures [KS17]. For type
theories without UIP, strict equalities are even more important, because they
are automatically coherent. Thus having more strict equalities means that we
escape not only “transport hell”, but also “higher-dimensional transport and
coherence hell”. Conversely, it is in practice much harder to justify strict
equalities in many homotopy theoretic models. Some authors have even
considered weak variants of the basic computation rules of type theories. For
instance, weak identity types, whose computation rule only holds up to
internal paths, have been introduced by [vdB18], under the name of
propositional identity types. The path types of cubical type theories [CCHM17]
also only satisfy weakly the computation rule of identity types. Other type
structures can be weakened similarly, and we can even consider type theories
whose computation rules are all expressed by internal identifications instead
of strict equalities. At the level of types and universes, instead of assuming
that each type former is strictly classified by some code in the universe, we
can ask for them to be classified only up to type equivalence. These weak
Tarski universes have been introduced in [Gal14]. The fact that homotopy type
theory with strict univalent universes, rather than weak universes, can be
interpreted in every $(\infty,1)$-topos has only been established recently
[Shu19].

In this setting, we can wonder how type theories with varying amounts of
strict equalities can be compared. More precisely, we wish to know how to
establish coherence and strictification theorems, that would allow us, when
working internally to a model of a weak type theory, to pretend that it
satisfies more strict equalities than it actually does, by replacing it by an
equivalent stricter model. The question of the conservativity of strict
identity types over weak identity types has been asked at the TYPES 2017
conference [ACC+17], motivated by the fact that the path types in cubical type
theory only satisfy the elimination principle of weak identity types. This was
also the original motivation for the present paper.

We give some examples of weakenings and extensions of homotopy type theory
that ought to be equivalent to standard homotopy type theory.

######  Examples 1.0.

  * •

Weakening the $\beta$ and $\eta$ computation rules of identity types,
$\Sigma$-types, inductive types, etc, gives a weaker variant of HoTT.

  * •

We can add strict equalities that make the addition on natural numbers into a
strictly associative and commutative operation. That is, while the inductive
definition of $(-+-):\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ only satisfies the
strict equalities $0+y=y$ and $(\mathsf{suc}\ x)+y=\mathsf{suc}\ (x+y)$, we
would add the strict equalities $x+0=0$, $x+(\mathsf{suc}\ y)=\mathsf{suc}\
(x+y)$, $x+y=y+x$, $(x+y)+z=x+(y+z)$, etc.

  * •

Similarly, we could make the composition of paths into a strictly associative
operation, optionally with strict inverses.

  * •

We can extend the theory with a universe of strict proposition [GCST19] that
is equivalent to the universe of homotopy propositions.

  * •

Similarly, we can extend the theory with universes of definitional categories,
definitional rings, etc, that satisfy strictly the equations of the theories
of categories, rings, etc.

  * •

We can extend the theory with a universe of “definitionally” pointed types
$\mathsf{DPtType}$, equivalent to the universe of pointed types
$\mathsf{PtType}\triangleq(A:\mathcal{U})\times A$, with a smash product
operation $(-\wedge-):\mathsf{DPtType}\to\mathsf{DPtType}\to\mathsf{DPtType}$
with more strict equalities than the smash product of $\mathsf{PtType}$. This
would provide an alternative interpretation of Brunerie’s rewriting based
method to prove that the smash product is a symmetric monoidal product on
pointed types [Bru18].

Some progress has been made by Isaev in [Isa18b]. In that paper, Isaev defines
the notion of Morita equivalence between type theories, and gives some
characterizations of that notion. A first conservativity result in the absence
of UIP is also proven, showing that type theories with weak or strict unit
types are Morita equivalent.

The constructions by Isaev [Isa18a] and Kapulkin and Lumsdaine [KL16, KL21b],
of Quillen model or semi-model structures over the categories of models of
type theories, are also extremely relevant for our work. In particular, as
remarked in [KL16], Hofmann’s conservativity theorem proves exactly that the
morphism $\mathbf{0}_{\mathsf{ITT}}\to\mathbf{0}_{\mathsf{ETT}}$ between the
initial models of intensional type theory and extensional type theory is a
trivial fibration of their semi-model structure. The weak equivalences of the
same semi-model structure correspond to a weaker notion of conservativity than
trivial fibrations. Isaev’s definition of Morita equivalence relies on that
notion of weak equivalence.

This paper builds on top of the aforementioned work. While Isaev considers the
notion of Morita equivalence for arbitrary morphisms between type theories, we
restrict our attention to the equational extensions
$\mathcal{T}\to\mathcal{T}_{E}$ of a weak type theory to a strict type theory
$\mathcal{T}_{E}$, by a family of equations $E$, which should hold weakly in
$\mathcal{T}$ and strictly in $\mathcal{T}_{E}$. We then establish sufficient
conditions for the theories $\mathcal{T}$ and $\mathcal{T}_{E}$ to be Morita
equivalent.

The situation can be compared to other well-known coherence theorems, such as
Mac Lane’s coherence theorem for monoidal categories [Lan63]. They can often
be stated in multiple different ways. For example, here are two related ways
to state the coherence theorem for monoidal categories.

  1. (1)

Every (weak) monoidal category is monoidally equivalent to a strict monoidal
category.

  2. (2)

In a freely generated monoidal category, every diagram made up of associators
and unitors commutes.

The statement (1) is generally the one that we want to use: it allows us to
work with any weak monoidal category as if it was strict. The statement (2) is
however perhaps easier to prove, because free monoidal categories can be seen
as syntactic objects, that are relatively easy to describe explicitly and
understand. See [JS91] for a proof of the statement (1) that relies on the
statement (2). In the case of monoidal category, it is actually possible to
prove the statement (1) more directly using representation theorems similar to
the Yoneda lemma. This kind of approach does not seem suitable for the
coherence theorems that we are interested in.

The main result of this paper is a coherence theorem for type theories that is
analogous to the fact the statement (1) can be deduced from the statement (2).
It states that to establish the conservativity of the equational extension
$\mathcal{T}\to\mathcal{T}_{E}$, it suffices to check that the
$\infty$-congruence over $\mathcal{T}$ freely generated by the equations of
$E$ exists and is $0$-truncated. This $0$-truncatedness condition encodes the
same idea as the fact that every diagram made up of associators and unitors
commutes in a freely generated monoidal category.

In general, we work at the level of _second-order generalized algebraic
theories_ (SOGATs) and their classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs.
SOGATs correspond to the class of theories classified by representable map
categories, which were introduced by Uemura [Uem19]. First-order generalized
algebraic theories are also SOGATs, so our results also apply to theories that
are not type theories, such as monoidal categories, etc. A SOGAT $\mathcal{T}$
is specified by its classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwF, also
denoted by $\mathcal{T}$, which can be seen as a syntactic model of some type
theory. A SOGAT has functorial semantics in
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs. Even if one is only interested in a
specific theory, working with SOGATs explicitly is advantageous. Indeed, many
semantic conditions can instead be stated more concisely and syntactically
directly at the level of the $(\Sigma,\Pi_{\mathsf{rep}})$-CwF $\mathcal{T}$.

The notion of $\infty$-congruence over a SOGAT $\mathcal{T}$ is specified at
the level of the classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwF. Informally, a
$1$-congruence over $\mathcal{T}$ is an extension of the set-valued
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF $\mathcal{T}$ to a setoid-valued
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF; this equips the sets of contexts,
substitutions, types and terms of $\mathcal{T}$ with equivalence relations
satisfying some conditions. Instead, an $\infty$-congruence should be an
extension of $\mathcal{T}$ to a space-valued
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF; this equips all components of $\mathcal{T}$
with $\infty$-groupoid structures.

Defining $\infty$-congruences require choosing a model of $\infty$-groupoids
among many. Instead of working with e.g. Kan simplicial sets, we rely on the
fact that $\infty$-groupoids are closely related to models of type theory with
identity types. Instead of working with space valued
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs, with work with
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs with identity types, i.e.
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs. In the original presentation
of this work, this was inspired by Brunerie’s type-theoretic definition of
$\infty$-groupoid [Bru16]. Another point of view is that models of type theory
with identity types correspond to structured $\infty$-categories. When working
with $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs, we morally work with
representable map $\infty$-categories. Representable map $\infty$-categories
have recently been used by Nguyen and Uemura [NU22] to give functorial
semantics to $\infty$-type theories, generalizing the functorial semantics of
$1$-type theories in representable map categories.

We don’t give any application of our coherence theorem in this paper, which is
instead focused on proving general results that hold for any SOGAT. Two
elements are still missing for applications, discussed in more details in
section 9. First, we need a proof of section 6.2, which essentially states
that our construction of the $\infty$-congruence generated by $E$ is
meaningful when $\mathcal{T}$ satisfies external univalence [Boc22]. Second,
we need ways to prove the $0$-truncatedness conditions for concrete theories.
We believe that in most cases, this $0$-truncatedness can be obtained as a
consequence of a homotopy normalization proof. A strict normalization states
that every term has a unique normal form; homotopy normalization states
instead that every term has a contractible space of normal forms. Uemura has
recently given a general proof scheme for normalization of $\infty$-type
theories [Uem22], which can be used to prove such homotopy normalization
results. Because we work with $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs
rather than $\infty$-type theories, the proof does not directly carry over to
our setting, but we believe that the results we need can be proven using
similar methods.

### Outline of the paper

In section 2, we introduce our notations and conventions, and review the
notion of Category with Families (CwFs) and associated definitions. We make
use of the internal language of presheaf categories to describe our
constructions. In particular, instead of working with CwFs externally, we
often prefer to work with families internally to presheaf categories.

In section 3, we define the structures of weak identity types, and show that
these structures can be lifted from a family to its family of telescopes. This
means that these structures are well-behaved even in the absence of
$\Sigma$-types.

In section 4, we recall the definition of second-order generalized algebraic
theories (SOGATs) and their functorial semantics in
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs. We follow the presentation of the author’s
paper on external univalence for SOGATs [Boc22]. Examples include the theories
of categories, monoidal categories, etc., as well as type theory with various
type structures. We also recall the notion of external univalence for SOGATs
equipped with homotopy relations. We also define classes of trivial
fibrations, fibrations and weak equivalences between models of SOGATs equipped
with homotopy relations.

In section 5, we introduce the notion of equational extension
$\mathcal{T}\to\mathcal{T}_{E}$ of a SOGAT, where $E$ is a collection of
homotopies in $\mathcal{T}$ that become strict equalities in
$\mathcal{T}_{E}$. We discuss some categorical and type-theoretic examples. We
also specify the notion of conservativity an equational extension, by adapting
Isaev’s definition of Morita equivalence [Isa18b].

In section 6, we introduce the notion of partial saturation: a
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF $\mathcal{C}$ with a morphism
$\mathcal{T}\to\mathcal{C}$ is partially saturated with respect to a
collection of homotopies $E$ when the homotopies in $E$ can be lifted to the
identity types of $\mathcal{C}$. This generalizes the notion of (full)
saturation used in the specification of external univalence. We then define
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ as the initial object among
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs under $\mathcal{T}$ that are
partially saturated with respect to $E$. It can be viewed as the
$\infty$-congruence on $\mathcal{T}$ that is freely generated by the
homotopies of $E$; the elements of its identity types are compositions and
higher-dimensional compositions of the lifts of the homotopies in $E$. Our
next step is to consider the following diagram.

${\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{\sim}$

The model $\mathcal{T}_{{\widehat{E}}}$ is the subCwF of
$\mathcal{T}_{{\widehat{E}}}^{\infty}$ spanned by the contexts and types that
do not contain identity types. The CwF $\mathcal{T}_{E}^{1}$ is obtained by
adding equality reflection to $\mathcal{T}_{\widehat{E}}^{\infty}$, or
equivalently by adding extensional equality types to $\mathcal{T}_{E}$.

To prove that the equational extension $\mathcal{T}\to\mathcal{T}_{E}$ is a
Morita equivalence, it then suffices to show that
$\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}$ and
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ are both equivalences.

We view proving that $\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}$ is an
equivalence (or equivalently
$\mathcal{T}\to\mathcal{T}_{{\widehat{E}}}^{\infty}$, by $2$-out-of-$3$) as a
proof that $\mathcal{T}_{{\widehat{E}}}^{\infty}$ is really an
$\infty$-congruence.

######  Conjecture (Simplified statement of section 6.2).

If $\mathcal{T}$ satisfies external univalence and is cofibrant, then
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$ is an equivalence.
$\lrcorner$

This conjecture will be discussed in section 9. For most examples, external
univalence can be proven using the tools of [Boc22].

The main theorem of the paper involves the second morphism
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$.

######  Theorem (Simplified statement of section 8).

If $\mathcal{T}^{\infty}_{{\widehat{E}}}$ is merely $0$-truncated relatively
to $\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$, then
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ is an equivalence.

The $(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF
$\mathcal{T}^{\infty}_{{\widehat{E}}}$ being $0$-truncated means that all of
its types are h-sets. Being merely $0$-truncated means that we only know the
mere existence of the terms witnessing $0$-truncatedness. Being $0$-truncated
relatively to $\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$ means that
this is only valid over contexts in the image of
$\mathcal{T}\to\mathcal{T}^{\infty}_{{\widehat{E}}}$.

In section 7 we discuss congruences and quotients for models of first-order
generalized algebraic theories. The proof of our main theorem requires the
construction of quotients of $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs by a
congruence; a congruence is an extension of a set-valued model to a setoid-
valued model. The categories of models of GATs are cocomplete, so quotients
always exists, but they are ill-behaved in general: the quotient inclusions
are not always trivial fibrations (surjective on every sort). We show that
this can be fixed by restricting our attention to _fibrant_ congruences; a
fibrant congruence is an extension of a set-valued model of a setoid-valued
model satisfying some fibration condition. The quotient inclusion of a fibrant
congruence is always a trivial fibration, and conversely every trivial
fibration is the quotient inclusion of a fibrant congruence.

In section 8 we prove section 8 by showing that under its assumptions, the map
$\mathcal{T}_{{\widehat{E}}}\to\mathcal{T}_{E}$ is a retract of some quotient
inclusion. We rely on the theory of fibrant congruences developed in the
previous section.

In section 9 we discuss some conjectures and the future work that would be
required for applications.

##  2\. Background

We recall in this section the semantics of type theories in categories with
families (CwFs), and introduce the tools and notations that we will use in
this paper. We will make use in particular of the internal type-theoretic
language of the presheaf category $\mathbf{Psh}(\mathcal{C})$ as a tool to
define and work with type-theoretic structures over a CwF $\mathcal{C}$.

###  2.1. Metatheory and basic notations

We work in a constructive metatheory, say extensional type theory with enough
universes and all QIITs. In some cases we will need distinguish split and non-
split surjective functions. We adopt terminology from the HoTT book; we use
the adverb _merely_ to indicate that we have an element of the propositional
truncation of some set. For example, a function $f:A\to B$ is a split
surjection when for every $b:B$ there is some element $a:A$ such that
$f(a)=b$. A function $f:A\to B$ is a non-split surjection when f or every
$b:B$ there merely exists some $a:A$ such that $f(a)=b$.

The sets of dependent function are written $(a:A)\to B(a)$, and dependent
functions are introduced by $(a:A)\mapsto b(a)$. We sometimes omit function
arguments when they can be inferred from the context. For instance, given a
function $f:(a:A)\to B(a)\to C(a)$, and elements $a:A$ and $b:B(a)$, we may
just write $f(b)$ or $f_{a}(b)$ instead of $f(a,b)$.

The sets of dependent pairs are written $(a:A)\times B(a)$, and dependent
pairs are introduced by $(a,b)$.

We make use of the interpretation of extensional type theory into presheaf
toposes. Because our metatheory is constructive, any of our external
constructions can also be interpreted in presheaf toposes.

###  2.2. Families

######  Definition 2.0.

A family $\mathbb{C}$ consists of a set $\mathbb{C}.\mathsf{Ty}:\mathrm{Set}$
of _types_ and a dependent set
$\mathbb{C}.\mathsf{Tm}:\mathbb{C}.\mathsf{Ty}\to\mathrm{Set}$ of _terms_ or
_elements_. We often let $\mathbb{C}$ stand for $\mathbb{C}.\mathsf{Ty}$, and
use $\mathbb{C}.\mathsf{Tm}$ as an implicit coercion from types to sets.
$\lrcorner$

There is a category $\mathbf{Fam}$ of families and family morphisms. It is
equivalent to the arrow category $\mathbf{Set}^{\to}$.

######  Definition 2.0.

A restriction of a family $\mathbb{C}$ is a map
$\iota:\mathsf{Ty}^{\prime}\to\mathbb{C}.\mathsf{Ty}$. It induces a restricted
family $\mathbb{C}^{\prime}$, with
$\mathbb{C}^{\prime}.\mathsf{Tm}(A)=\mathbb{C}.\mathsf{Tm}(\iota(A))$. There
is an induced family morphism $\mathbb{C}^{\prime}\to\mathbb{C}$. We say that
a family morphism is cartesian if it induced by a family restriction, or
equivalently if its action on terms is bijective.  $\lrcorner$

###  2.3. Type-structures

######  Definition 2.0.

A $\mathbf{1}$-type structure on a family $\mathbb{C}$ consists of a type
$\mathbf{1}:\mathbb{C}$ and an isomorphism
$\mathbb{C}.\mathsf{Tm}(\mathbf{1})\cong\\{\star\\}$.  $\lrcorner$

######  Definition 2.0.

A $\Sigma$-type structure on a family $\mathbb{C}$ consists, for every
$A:\mathbb{C}$ and $B:A\to\mathbb{C}$, of a type $\Sigma(A,B):\mathbb{C}$ and
an isomorphism $\mathbb{C}.\mathsf{Tm}(\Sigma(A,B))\cong(a:A)\times B(a)$.
$\lrcorner$

######  Definition 2.0.

A $\Pi$-type structure on a family $\mathbb{C}$ consists, for every
$A:\mathbb{C}$ and $B:A\to\mathbb{C}$, of a type $\Pi(A,B):\mathbb{C}$ and an
isomorphism $\mathbb{C}.\mathsf{Tm}(\Pi(A,B))\cong((a:A)\to B(a))$.
$\lrcorner$

It is often the case that a family is not closed under arbitrary $\Pi$-types,
but only under $\Pi$-types whose domains lie in another family.

######  Definition 2.0.

Let $\mathbb{C}$ and $\mathbb{D}$ be two families. A $\Pi$-type structure on
$\mathbb{D}$ with arities in $\mathbb{C}$ consist, for every $A:\mathbb{C}$
and $B:A\to\mathbb{D}$, of a type $\Pi(A,B):\mathbb{D}$ and an isomorphism
$\mathbb{D}.\mathsf{Tm}(\Pi(A,B))\cong((a:A)\to B(a))$.  $\lrcorner$

######  Definition 2.0.

Let $\mathbb{C}$ be a family, along with a restriction
$\mathbb{C}_{\mathsf{rep}}\to\mathbb{C}$. A $\Pi_{\mathsf{rep}}$-type
structure on $\mathbb{C}$ consists of a $\Pi$-type structure on $\mathbb{C}$
with arities in $\mathbb{C}_{\mathsf{rep}}$.  $\lrcorner$

The types of $\mathbb{C}_{\mathsf{rep}}$ are called representable types. The
restriction $\mathbb{C}_{\mathsf{rep}}\to\mathbb{C}$ is not necessarily
injective, but we can often pretend that it is injective and omit it.

######  Definition 2.0.

A $(\Sigma,\Pi_{\mathsf{rep}})$-family is a family $\mathbb{C}$, along with a
restriction $\mathbb{C}_{\mathsf{rep}}\to\mathbb{C}$, such that both
$\mathbb{C}$ and $\mathbb{C}_{\mathsf{rep}}$ have $\mathbf{1}$\- and
$\Sigma$\- type structures, and such that $\mathbb{C}$ has a
$\Pi_{\mathsf{rep}}$-type structure.  $\lrcorner$

Similarly, we may talk of $\Sigma$-families or $(\Sigma,\Pi)$-families.

When working with $(\Sigma,\Pi_{\mathsf{rep}})$-families, we may sometimes
omit to mention $\mathbb{C}_{\mathsf{rep}}$ in some constructions. It should
then be understood that the same construction is applied to
$\mathbb{C}_{\mathsf{rep}}$. For example, the $\mathbf{1}$\- and $\Sigma$\-
types of $\mathbb{C}$ and $\mathbb{C}_{\mathsf{rep}}$ are distinct, but in
some constructions we may only refer to the $\mathbf{1}$\- and $\Sigma$\-
types of $\mathbb{C}$.

###  2.4. Categories with families

We review the notion of category with families (CwF), which is used to model
type theory.

We first recall the definition of locally representable presheaf, which is
used to encode the context extensions in models of type theory. This
definition is a reformulation of the notion of representable natural
transformation, which has been used by Awodey [Awo18] to define natural
models, which are equivalent to categories with families.

######  Definition 2.0.

Let $Y$ be a dependent presheaf over a presheaf $X$. We say that $Y$ is
locally representable if for every element $x:X(\Gamma)$, the presheaf
$Y_{\mid x}:(\mathcal{C}/\Gamma)^{\mathsf{op}}\to\mathbf{Set}$ is
representable, where

$\displaystyle Y_{\mid x}(\rho:\Delta\to\Gamma)\triangleq Y(x[\rho]).$

In that case, its representing object consists of an extended context
$\Gamma.Y[x]$ and a projection map $\bm{p}_{x}:\Gamma.Y[x]\to\Gamma$. There is
a generic element $\bm{q}_{x}:Y(x[\bm{p}_{x}])$. These satisfy the following
universal property: for every other object $\Delta$, map
$\gamma:\Delta\to\Gamma$ and element $a:Y(x[\gamma])$, there is a unique map
${\left\langle\gamma,a\right\rangle}:\Delta\to\Gamma.Y[x]$ such that
$\bm{p}_{x}\circ{\left\langle\gamma,a\right\rangle}=\gamma$ and
$\bm{q}_{x}[{\left\langle\gamma,a\right\rangle}]=a$.  $\lrcorner$

######  Definition 2.0.

A category with families (CwF) consists of a category $\mathcal{C}$, with a
terminal object, along with a global family $\mathbb{C}$ in
$\mathbf{Psh}(\mathcal{C})$ such that $\mathbb{C}.\mathsf{Tm}$ is locally
representable.  $\lrcorner$

A $(\Sigma,\Pi_{\mathsf{rep}})$-CwF is a CwF $\mathcal{C}$ such that the
family $\mathbb{C}$ is a $(\Sigma,\Pi_{\mathsf{rep}})$-family in
$\mathbf{Psh}(\mathcal{C})$. Similarly, we have $\Sigma$-CwFs,
$(\Sigma,\Pi)$-CwFs, $(\Sigma,\mathsf{Eq})$-CwFs,
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs, etc. (Identity types and
equality types will be specified in section 3). The $1$-category of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs is denoted by
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$, and other $1$-categories of
structured CwFs are written similarly.

Given a CwF $\mathcal{C}$, we will write $(\Gamma\vdash A\
\mathsf{type})\in\mathcal{C}$ to indicate that $A$ is a type is context
$\Gamma$, and $(\Gamma\vdash a:A)\in\mathcal{C}$ to indicate that $a$ is a
term of type $A$ in context $\Gamma$. Occasionally we may also write
$(\gamma:\Gamma\vdash A(\gamma)\ \mathsf{type})\in\mathcal{C}$ and
$(\gamma:\Gamma\vdash a(\gamma):A(\gamma))\in\mathcal{C}$. We write
$(\Gamma\vdash A\ {\mathsf{type}_{\mathsf{rep}}})\in\mathcal{C}$ if $A$ is a
representable type over $\Gamma$, when $\mathcal{C}$ is a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF. We may write $(A\
\mathsf{type})\in\mathcal{C}$ or $(a:A)\in\mathcal{C}$ when working over the
empty context $1_{\mathcal{C}}$.

We have freely generated $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs Free_Σ,Π_rep(Γ ⊢),

Free_Σ,Π_rep(Γ ⊢A type),

Free_Σ,Π_rep(Γ ⊢A type_rep),
Free_Σ,Π_rep(Γ ⊢a : A), where we use bold letters to indicate the generators.

We have maps

$\displaystyle
I^{\mathsf{ty}}:\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash)\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}\
\mathsf{type}),$ $\displaystyle
I^{{\mathsf{ty}_{\mathsf{rep}}}}:\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash)\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}\
{\mathsf{type}_{\mathsf{rep}}}),$ $\displaystyle
I^{\mathsf{tm}}:\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}\
\mathsf{type})\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{a}:\bm{A}),$

which are generic extensions of a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF by a new
type, representable type or term.

We also have maps

$\displaystyle
E^{\mathsf{ty}}:\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A},\bm{B}\
\mathsf{type})\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}=\bm{B}),$
$\displaystyle
E^{{\mathsf{ty}_{\mathsf{rep}}}}:\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A},\bm{B}\
{\mathsf{type}_{\mathsf{rep}}})\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}=\bm{B}),$
$\displaystyle
E^{\mathsf{tm}}:\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{x},\bm{y}:\bm{A})\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{x}=\bm{y}),$

which are generic extensions of a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF by a new
equation between two types, representable types or terms. These maps are the
codiagonals of
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}}\\}$.

We will consider various weak factorization systems and orthogonal
factorization systems generated by subsets of
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{ty}},E^{{\mathsf{ty}_{\mathsf{rep}}}},E^{\mathsf{tm}}\\}$.
We may also similarly consider factorization systems on other categories of
CwFs, e.g. $\mathbf{CwF}_{\Sigma}$ or just $\mathbf{CwF}$.

In section 4 we will also consider similar factorization systems on the
categories of models of arbitrary SOGATs.

We start with the (cofibrations, trivial fibrations) weak factorization
systems.

######  Definition 2.0.

A map $F:\mathcal{C}\to\mathcal{D}$ in $(\Sigma,\Pi_{\mathsf{rep}})$-CwF is a
(split) trivial fibration if its actions on types, representable types and
terms are split surjective.  $\lrcorner$

######  Definition 2.0.

A map $F:\mathcal{C}\to\mathcal{D}$ in $(\Sigma,\Pi_{\mathsf{rep}})$-CwF is a
(non-split) trivial fibration if its actions on types, representable types and
terms are merely surjective.  $\lrcorner$

The split trivial fibrations are the right class of the weak factorization
system generated by
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}}\\}$. Maps
in the left class are called _cofibrations_.

The conservativity of Extensional Type Theory over Intensional Type Theory can
be stated using the notion of trivial fibration: the unique morphism
$\mathbf{0}_{\mathsf{ITT}}\to\mathbf{0}_{\mathsf{ETT}}$ between the initial
models of the two type theories is a non-split trivial fibration in
$\mathbf{CwF}$, i.e. its actions on types and terms are surjective.

The global picture of Hofmann’s proof of conservativity [Hof95] is the
following. We construct a quotient $Q$ of the syntactic model
$\mathbf{0}_{\mathsf{ITT}}$. By the universal properties of the quotient $Q$
and of the model $\mathbf{0}_{\mathsf{ETT}}$, we obtain a section-retraction
pair $(\mathbf{0}_{\mathsf{ETT}}\to Q,Q\to\mathbf{0}_{\mathsf{ETT}})$. This
exhibits the map $\mathbf{0}_{\mathsf{ITT}}\to\mathbf{0}_{\mathsf{ETT}}$ as a
retract of the quotient inclusion $\mathbf{0}_{\mathsf{ITT}}\to Q$. Since the
quotient inclusion is a non-split trivial fibration and non-split trivial
fibration are closed under retracts, we obtain the desired conservativity
result. Most of the complexity of the proof lies in the construction of the
quotient $Q$.

It is not possible to prove constructively that
$\mathbf{0}_{\mathsf{ITT}}\to\mathbf{0}_{\mathsf{ETT}}$ is a split trivial
fibration. Indeed, if it were possible, it would be possible to decide
equality of terms of $\mathbf{0}_{\mathsf{ETT}}$ by deciding the equality of
their lifts in $\mathsf{ITT}$.

###  2.5. Contextual CwFs

An important class of CwFs are the _contextual_ CwFs, whose objects and
morphisms are really given by lists of types and terms. Indeed, from some
point of view, in the language of type theory, we never explicitly talk about
the objects and morphisms of a model, but only about types and terms that live
in the same contextual slice of a given model. From this perspective, only the
contextual models matter. However, a direct definition of contextual models is
complicated (their generalized algebraic presentation is infinite, as it
quantifies over all possible context lengths), and many intermediate
constructions go through non-contextual models. It is thus more convenient to
define contextuality as a property of general models. Fortunately, they can be
described by the means of an orthogonal factorization system on
$\mathbf{CwF}$111The author learnt of this definition of contextuality from
Christian Sattler..

######  Definition 2.0.

A CwF morphism $F:\mathcal{C}\to\mathcal{D}$ is said to be a contextual
isomorphism if its actions on types and terms are bijective.  $\lrcorner$

Contextual isomorphisms are the right class of maps of the orthogonal
factorization system generated by $\\{I^{\mathsf{ty}},I^{\mathsf{tm}}\\}$, or
equivalently of the weak factorization system generated by
$\\{I^{\mathsf{ty}},E^{\mathsf{ty}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$. The
maps in the left class are called left contextual maps.

Any CwF morphism $F:\mathcal{C}\to\mathcal{D}$ admits an unique (up to
isomorphism) factorization $\mathcal{C}\to\mathsf{cxlim}(F)\to\mathcal{D}$
where $\mathcal{C}\to\mathsf{cxlim}(F)$ is left contextual and
$\mathsf{cxlim}(F)\to\mathcal{D}$ is a contextual isomorphism. The CwF
$\mathsf{cxlim}(F)$ is called the contextual image of $F$.

In particular, given any $\mathcal{C}:\mathbf{CwF}$, the unique morphism
$\mathbf{0}\to\mathcal{C}$ admits such a factorization. Its contextual image
is called the contextual core of $\mathcal{C}$, and is denoted by
$\mathsf{cxl}(\mathcal{C})$. The map $\mathsf{cxl}(\mathcal{C})\to\mathcal{C}$
is a contextual isomorphism by definition. When the map
$\mathsf{cxl}(\mathcal{C})\to\mathcal{C}$ is also an isomorphism of CwFs, we
say that $\mathcal{C}$ is contextual.

This definition of contextuality is equivalent to the usual definition, as
found for instance in [CCD19].

######  Proposition 2.0.

A CwF $\mathcal{C}$ is contextual if and only there exists a length function
$l:\mathsf{Ob}_{\mathcal{C}}\to\mathbb{N}$ such than for any
$\Gamma\in\mathcal{C}$, if $l(\Gamma)=0$ then $\Gamma=1_{\mathcal{C}}$ and if
$l(\Gamma)=n+1$, then there are unique $\Gamma^{\prime}\in\mathcal{C}$ and
$(\Gamma^{\prime}\vdash A\ \mathsf{type})\in\mathcal{C}$ such that
$\Gamma=\Gamma^{\prime}.A$. ∎

We write $\mathbf{CwF}^{\mathsf{cxl}}$ for the full subcategory of
$\mathbf{CwF}$ spanned by the contextual CwFs. The contextual core functor
$\mathsf{cxl}:\mathbf{CwF}\to\mathbf{CwF}^{\mathsf{cxl}}$ is a right adjoint
of $\mathbf{CwF}^{\mathsf{cxl}}$. This exhibits $\mathbf{CwF}^{\mathsf{cxl}}$
as a coreflective subcategory of $\mathbf{CwF}$.

This definition of contextuality extends to
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$ by considering the orthogonal
factorization system generated by
$\\{I^{\mathsf{ty}},E^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},E^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$
instead, i.e. contextual isomorphisms in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$ also need to have bijective actions
on representable types.

###  2.6. Join of families and telescopes

We do not always assume the presence of $\Sigma$-types. To circumvent their
absence in some constructions, we need to work with families of telescopes,
whose types and terms are finite sequences of types and terms of the base
family. It is convenient to present them as the coproduct of length $n$
telescopes for all $n:\mathbb{N}$, and to generalize the notion of length $n$
telescope to a more heterogeneous notion, using the notion of join of
families222The author learnt of this presentation from Christian Sattler..

######  Definition 2.0.

Let $\mathbb{C}$ and $\mathbb{D}$ be two families. Their join
$\mathbb{C}\ast\mathbb{D}$ is the family defined by:

$\displaystyle(\mathbb{C}\ast\mathbb{D}).\mathsf{Ty}\triangleq(A:\mathbb{C})\times(B:A\to\mathbb{D})$
$\displaystyle(\mathbb{C}\ast\mathbb{D}).\mathsf{Tm}(A,B)\triangleq(a:A)\times(b:B(a))$
$\lrcorner$

In other words, the join of $\mathbb{C}$ and $\mathbb{D}$ is the family of
length $2$ telescopes, whose first and second components come respectively
from $\mathbb{C}$ and $\mathbb{D}$.

The join operation is a monoidal product on $\mathbf{Fam}$.

######  Definition 2.0.

If $\mathbb{C}$ is a family and $n:\mathbb{N}$, the family $\mathbb{C}^{\ast
n}$ of length $n$ telescopes is the $n$-fold iterated join of $\mathbb{C}$.
$\lrcorner$

######  Definition 2.0.

If $\mathbb{C}$ is a family, the family of telescopes of $\mathbb{C}$ is the
coproduct $\mathbb{C}^{\star}\triangleq\coprod_{n:\mathbb{N}}\mathbb{C}^{\ast
n}$.  $\lrcorner$

If $\mathcal{C}$ is a contextual CwF, we may identify its objects with the
closed telescopes of types (i.e. the global elements of the presheaf
$\mathbb{C}^{\star}.\mathsf{Ty}$) and its morphisms from $\Gamma$ to $\Delta$
with the natural transformations from $\mathbb{C}^{\star}.\mathsf{Tm}(\Gamma)$
to $\mathbb{C}^{\star}.\mathsf{Tm}(\Delta)$. When $\mathcal{C}$ is an
arbitrary CwF, this is an explicit description of the objects and morphisms of
the contextual core of $\mathcal{C}$.

##  3\. Weak identity types

In this section we define the weak and strict variants of identity types.
Generally, the computation rules of a weak type structure are expressed by
internal identifications, whereas the computation rules of strict type
structures are expressed by strict equalities. These notions should not be
confused with weakly stable and strictly stable type-structures. Since type
theories with weak computation rules are the main focus of this paper, we
reserve the short naming for this notion. In ambiguous cases, we could talk of
weakly computational and strictly computational type-structures. In the
literature, strict identity types sometimes refer to $(-1)$-truncated identity
types, which satisfy the Uniqueness of Identity Proofs principle.

###  3.1. Definition

In presence of (strict) $\Sigma$-type and $\Pi$-types, there are several
equivalent ways to define the eliminator for identity types. The Martin-Löf
eliminator is given by the following rule. [Martin-Löf eliminator]A type
x : A, y : A, p : Id_A(x,y) ⊢D(x,y,p) type
x : A ⊢d(x) : D(x,x,refl)
x : A
y : A
p : Id_A(x,y)J(D,d,y,p) : D(x,y,p) In absence of $\Pi$-types, the Martin-Löf
eliminator does not seem to be strong enough to even define transport.

In [GG08], a variant of the Martin-Löf eliminator, now called the Frobenius
variant of the Martin-Löf eliminator, is introduced. The idea is to circumvent
the absence of $\Pi$-types by allowing the target type family $D$ of the
elimination to depend on any telescope $\Delta$ of parameters. [Frobenius
Martin-Löf eliminator]A type
x : A, y : A, p : Id_A(x,y) ⊢Δ(x,y,p) type^⋆

x : A, y : A, p : Id_A(x,y), δ: Δ(x,y,p) ⊢D(x,y,p,δ) type
x : A, δ: Δ(x,x,refl) ⊢d(x,δ) : D(x,x,refl,δ)

x : A
y : A
p : Id_A(x,y)
δ: Δ(x,y,p)J(D,d,x,y,p,δ) : D(x,y,p,δ) Another alternative is the Paulin-
Mohring eliminator, also known as based path induction, or one-sided
eliminator. [Paulin-Mohring eliminator]A type
x : A
y : A, p : Id_A(x,y) ⊢D(y,p) type

d(x) : D(x,refl)
y : A
p : Id_A(x,y)J(D,d,y,p) : D(y,p) North [Nor19] and Isaev [Isa21] have
independently given proofs of the fact that the Paulin-Mohring eliminator is
equivalent to the Frobenius variant of the Martin-Löf eliminator in the
presence of $\Sigma$-types.

We use the weak variant of the Paulin-Mohring eliminator, with the computation
rule weakened to a weak equality. We will show that the other eliminators can
also be derived, even in the absence of $\Sigma$-types. In fact, we will prove
that weak identity types can be lifted from a family $\mathbb{C}$ to its
telescope family $\mathbb{C}^{\star}$, i.e. the family whose types are list of
types of $\mathbb{C}$; the derivation of the Frobenius eliminator can be seen
as a consequence of this fact. The main step of this derivation is originally
due to András Kovács. The proof has been simplified using the notion of join
of families by Christian Sattler.

######  Definition 3.0.

Let $\mathbb{C}$ be a family. An identity type introduction structure over
$\mathbb{C}$ consists of the following operations:

$\displaystyle\mathsf{Id}:(A:\mathbb{C})(x:A)(y:A)\to\mathbb{C},$
$\displaystyle\mathsf{refl}:(A:\mathbb{C})(x:A)\to\mathsf{Id}_{A}(x,x).$
$\lrcorner$

Given an identity type introduction structure and $A:\mathbb{C}$, we write
$\mathsf{IdFrom}(x)$ for the set of identifications with $x:A$ as the fixed
left endpoint.

$\displaystyle\mathsf{IdFrom}(x)\triangleq(y:A)\times\mathsf{Id}_{A}(x,y).$

######  Definition 3.0.

Let $\mathbb{C}$ and $\mathbb{D}$ be two families with identity type
introduction structures. A weak identity type elimination structure from
$\mathbb{C}$ to $\mathbb{D}$ consists of the following operations:

$\displaystyle\mathsf{J}$ $\displaystyle:{}$
$\displaystyle(A:\mathbb{C})(x:A)(D:\mathsf{IdFrom}(x)\to\mathbb{D})$
$\displaystyle(d:D(x,\mathsf{refl}))(p:\mathsf{IdFrom}(x))$ $\displaystyle\to
D(p)$ $\displaystyle\mathsf{J}_{\beta}$ $\displaystyle:{}$
$\displaystyle(A:\mathbb{C})(x:A)(D:\mathsf{IdFrom}(x)\to\mathbb{D})$
$\displaystyle(d:D(x,\mathsf{refl}))$
$\displaystyle\to\mathsf{Id}(\mathsf{J}(D,d,(x,\mathsf{refl})),d)$ $\lrcorner$

A weak identity type structure over a family $\mathbb{C}$ consists of an
identity type introduction structure over $\mathbb{C}$ along with a weak
identity type elimination structure from $\mathbb{C}$ to $\mathbb{C}$.

######  Definition 3.0.

A weak identity type structure is said to be strict if the following equations
hold, for all relevant arguments:

$\displaystyle\mathsf{J}(D,d,(x,\mathsf{refl}))=d,$
$\displaystyle\mathsf{J}_{\beta}(D,d)=\mathsf{refl}.$ $\lrcorner$

Given an internal family $\mathbb{C}$ equipped with weak identity types, we
can derive the transport operation:

$\mathsf{transport}:(D:A\to\mathbb{C})(p:\mathsf{Id}(x,y))\to D(x)\to D(y).$

We may write $p^{\star}(d)$ instead of $\mathsf{transport}(D,p,d)$, leaving
the family $D$ implicit.

The standard notions of homotopy type theory, such as contractible types,
propositional types, equivalences, etc, can be defined. However, since we may
not have $\Sigma$-types or $\Pi$-types, they are not always encoded by types
of the theory.

######  Definition 3.0.

An equality type structure over a family $\mathbb{C}$ is a weak identity type
structure satisfying the following two equations

$\displaystyle\mathsf{Id}(A,x,y)\to(x=y),$
$\displaystyle(p:\mathsf{Id}(A,x,y))\to(p=\mathsf{refl}).$ $\lrcorner$

We will use $\mathsf{Eq}$ instead of $\mathsf{Id}$ for equality type
structures.

###  3.2. Lifting type structures to telescopes

In this subsection, we show that $\mathsf{Id}$-type structures on a family
$\mathbb{C}$ can be lifted to the telescope family $\mathbb{C}^{\star}$.
Similar results have been proven and used before in the literature [Gar09,
KL21b]. We generalize them to weak type structures and families without
locally representable elements. The constructions have been formalized in
Agda.333The Agda files are available at
https://rafaelbocquet.gitlab.io/Agda/20230420_WeakIdTypes/. We refer the
reader to the formalization for the detailed constructions.

######  Construction 3.0.

Let $\mathbb{C}$ and $\mathbb{D}$ be families with identity type introduction
structures, along with a weak identity type elimination structure from
$\mathbb{C}$ to $\mathbb{D}$.

Then the family $\mathbb{C}\ast\mathbb{D}$ is equipped with the following
identity type introduction structure:

$\displaystyle\mathsf{Id}_{(A,B)}((x_{c},x_{d}),(y_{c},y_{d}))\triangleq(\mathsf{Id}_{A}(x_{c},y_{c}),\lambda
p_{c}\mapsto\mathsf{Id}_{B(y_{c})}(p_{c}^{\star}(y_{c}),y_{d})$
$\displaystyle\mathsf{refl}_{(A,B)}(x_{c},x_{d})\triangleq(\mathsf{refl},\mathsf{tr}_{\beta}),$

where $\mathsf{tr}_{\beta}$ is some term of type
$\mathsf{Id}(\mathsf{refl}^{\star}(x_{c}),x_{c})$, definable using
$\mathsf{J}_{\beta}$.  $\lrcorner$

######  Construction 3.0.

Let $\mathbb{C}$, $\mathbb{D}$ and $\mathbb{E}$ be families with identity type
introduction structures, along with identity type elimination structures from
$\mathbb{C}$ to $\mathbb{D}$ and $\mathbb{E}$, from $\mathbb{D}$ to
$\mathbb{D}$ and $\mathbb{E}$ and from $\mathbb{E}$ to $\mathbb{E}$.

Then there exist weak identity type elimination structures from
$(\mathbb{C}\ast\mathbb{D})$ to $\mathbb{E}$ and from $\mathbb{C}$ to
$(\mathbb{D}\ast\mathbb{E})$.  $\lrcorner$

######  Construction 3.0.

Let $\mathbb{C}$ be a family with a weak identity type structure.

Then for every $n:\mathbb{N}$, the family $\mathbb{C}^{\ast n}$ of length $n$
telescopes has a canonical identity type introduction structure, and for every
$n,m:\mathbb{N}$ there is a weak identity type elimination structure from
$\mathbb{C}^{\ast n}$ to $\mathbb{C}^{\ast m}$.

###### Proof.

By iterating section 3.2 and section 3.2. ∎

In all of these constructions, if all of the given identity type are strict,
then the constructed type structures are also strict.

###  3.3. Parametrized elimination structures

######  Definition 3.0.

Let $\mathbb{C}$, $\mathbb{D}$ and $\mathbb{E}$ be families, together with
identity type introduction structures over $\mathbb{C}$ and $\mathbb{E}$.
A parametrized identity type elimination structure from $\mathbb{C}$ to
$\mathbb{E}$ with parameters in $\mathbb{D}$ consists of operations

$\displaystyle\mathsf{J}$ $\displaystyle:{}$
$\displaystyle(A:\mathbb{C})(x:A)(Q:\mathsf{IdFrom}(x)\to\mathbb{D})$
$\displaystyle(D:(p:\mathsf{IdFrom}(x))(q:Q(p))\to\mathbb{E})$
$\displaystyle(d:(q:Q(x,\mathsf{refl}))\to D((x,\mathsf{refl}),q))$
$\displaystyle(p:\mathsf{IdFrom}(x))(q:Q(y))$ $\displaystyle\to D(p,q)$
$\displaystyle\mathsf{J}_{\beta}$ $\displaystyle:{}$
$\displaystyle(A:\mathbb{C})(x:A)(Q:\mathsf{IdFrom}(x)\to\mathbb{D})$
$\displaystyle(D:(p:\mathsf{IdFrom}(x))(q:Q(y))\to\mathbb{E})$
$\displaystyle(d:(q:Q(x,\mathsf{refl}))\to D((x,\mathsf{refl}),q))$
$\displaystyle\to\mathsf{Id}(\mathsf{J}(Q,D,d,(x,\mathsf{refl})),d(q))$
$\lrcorner$

######  Construction 3.0.

Assume that $\mathbb{C}$, $\mathbb{D}$ and $\mathbb{E}$ are families equipped
with identity type introduction structures and identity type elimination
structures from $\mathbb{C}$ to $\mathbb{C}$, $\mathbb{D}$ and $\mathbb{E}$,
from $\mathbb{D}$ to $\mathbb{D}$ and $\mathbb{E}$ and from $\mathbb{E}$ to
$\mathbb{E}$.

Then we can construct a parametrized identity type elimination structure from
$\mathbb{C}$ to $\mathbb{E}$ with parameters in $\mathbb{D}$.  $\lrcorner$

The Frobenius variant of the Paulin-Mohring identity type eliminator is
exactly a parametrized identity type elimination structure with parameters in
the family of telescopes.

###  3.4. CwFs with identity types

A CwF $\mathcal{C}$ is equipped with identity types if its family $\mathbb{C}$
is equipped with a global weak identity type structure in
$\mathbf{Psh}(\mathcal{C})$.

We will write $\mathbf{CwF}_{\mathsf{Id}}$ for the category of CwFs equipped
with weak identity types.

In presence of both $\Pi$-types and $\mathsf{Id}$-types, we always assume that
function extensionality is satisfied. We write
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}}}$ for the category of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs equipped with weak identity types
satisfying function extensionality. We write
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}},\mathsf{Eq}}$ for the category of
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF equipped with extensional equality types.

##  4\. Second-order generalized algebraic theories

In this section we recall the theory of second-order generalized algebraic
theories. Generalized algebraic theories (GATs) are theories specified by a
collection of dependent sorts, operations and equations between them. Second-
order generalized algebraic theories (SOGATs) generalize GATs by allowing
second-order operations, meaning that the arguments of an operation can bind
some variables. Most type theories can be encoded as SOGATs. Any (first-order)
GAT can also be seen as a SOGAT. Among other examples, we will consider the
SOGAT $\mathcal{T}_{\mathsf{Id}}$ of weak identity types, the GAT
$\mathcal{T}_{\mathbf{MonCat}}$ of monoidal categories, and their extensions
to strict identity types and strict monoidal categories.

It is possible to develop the functorial semantics SOGATs in
$\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$. Given a SOGAT $\mathcal{T}$, there
is a notion of model of $\mathcal{T}$ in any $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
$\mathcal{C}$, corresponding to an interpretation of the sorts and operations
of $\mathcal{T}$ as types and terms of $\mathcal{C}$. The SOGAT $\mathcal{T}$
can be identified with its classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwF, also
written $\mathcal{T}$. A model of $\mathcal{T}$ in $\mathcal{C}$ is then
identified with a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism
$\mathcal{T}\to\mathcal{C}$.

By working with SOGATs we know that our results apply to a large class of type
theories. More importantly, many semantic conditions can be expressed more
naturally at the level of the classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
$\mathcal{T}$. Instead of considering arbitrary models of $\mathcal{T}$, it is
often sufficient to consider $\mathcal{T}$ instead. The reason combines two
ideas. First, any object of $\mathcal{T}$ can be seen as a signature
presenting a finitely generated model; this should induce a fully faithful
functor
$\mathbf{0}_{\mathcal{T}}[-]:\mathcal{T}^{\mathsf{op}}\to\mathbf{Mod}_{\mathcal{T}}$
whose essential image consists of the finitely generated models of
$\mathcal{T}$, see section 4.4. Second, any model can be approximated by
finitely generated models; more precisely any model admits a cofibrant
replacement that is freely generated, and any freely generated model is a
filtered colimit of finitely generated models.

For this reason, we focus on the classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
of a SOGAT. Our main results are stated at this level and do not depend on the
semantics of SOGATs. We still develop some of the semantics in order to
provide some additional intuition for our definitions. However, semantic
considerations that would require rather technical proofs are omitted or left
to future work.

We also review the notion of external univalence for a SOGATs equipped with
homotopy relations. This notion was introduced by the author in [Boc22]. Given
a choice of a homotopy relation for every sort of a SOGAT, external univalence
expresses the well-behavedness of the homotopy relations; in particular the
fact that they are preserved by all operations. External univalence is also
stated at the level of the classifying $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
$\mathcal{T}$, as the existence of some identity type structure (unfortunately
both weakly computational and weakly stable) on $\mathcal{T}$. These identity
types have to satisfy a univalence condition, also called saturation
condition. An analogous partial saturation condition will be introduced in
section 6.

More semantically, external univalence is closely related to left semi-model
structures on the category of models, as considered by Kapulkin and Lumsdaine
[KL16] and Isaev [Isa18a]. External univalence is also a way to morally view a
SOGAT as an $\infty$-type theory (in the sense of Nguyen and Uemura [NU22]),
without using quasicategories.

###  4.1. Definitions and examples

######  Definition 4.0.

A second-order generalized algebraic theory is an
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$-cellular
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF $\mathcal{T}$, where we recall that the maps
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{tm}}\\}$
are the generic extensions of $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs by a type,
representable type, term or term equality:

$\displaystyle I^{\mathsf{ty}}$ $\displaystyle:{}$
$\displaystyle\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash)\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}\
\mathsf{type}),$ $\displaystyle I^{{\mathsf{ty}_{\mathsf{rep}}}}$
$\displaystyle:{}$
$\displaystyle\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash)\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}\
{\mathsf{type}_{\mathsf{rep}}}),$ $\displaystyle I^{\mathsf{tm}}$
$\displaystyle:{}$
$\displaystyle\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{A}\
\mathsf{type})\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{a}:\bm{A}),$
$\displaystyle E^{\mathsf{tm}}$ $\displaystyle:{}$
$\displaystyle\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{x},\bm{y}:\bm{A})\to\mathsf{Free}_{\Sigma,\Pi_{\mathsf{rep}}}(\bm{\Gamma}\vdash\bm{x}=\bm{y}).$
$\lrcorner$

A morphism between SOGATs is a morphism of $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs.

The cellular presentation of a SOGAT consists of sorts, representable sorts,
operations and equations between operations, corresponding to the four maps
$I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}},E^{\mathsf{tm}}$.

A SOGAT without equations is a SOGAT that is actually
$\\{I^{\mathsf{ty}},I^{{\mathsf{ty}_{\mathsf{rep}}}},I^{\mathsf{tm}}\\}$-cellular
in $\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$. SOGATs without equations are
cofibrant objects in $\mathbf{CwF}_{\Sigma,\Pi_{\mathsf{rep}}}$, and are
therefore better behaved than general SOGATs in some situations. When
considering equational extensions of SOGATs, the source SOGAT will usually be
a SOGAT without equations.

We will write $\mathbb{T}$, $\mathbb{T}_{1}$, $\mathbb{T}_{2}^{3}$, etc., for
the internal $(\Sigma,\Pi_{\mathsf{rep}})$-families corresponding to SOGATs
$\mathcal{T}$, $\mathcal{T}_{1}$, $\mathcal{T}_{2}^{3}$, etc. in the presheaf
categories $\mathbf{Psh}(\mathcal{T})$, $\mathbf{Psh}(\mathcal{T}_{1})$, etc.

We use a bold red font for the sorts and operations of a SOGAT, mainly to
distinguish them from the type-theoretic structure of the
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF.

######  Example 4.0.

The GAT of categories $\mathcal{T}_{\mathbf{Cat}}$ is given by the following
signature:

$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}:\mathbb{T}_{\mathbf{Cat}}$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}:{\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{Ob}}}\to\mathbb{T}_{\mathbf{Cat}}$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}:\forall
x\
y\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\to\mathbb{T}_{\mathbf{Cat}}$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}}:{}\forall
x\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,x)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{comp}}}:{}\forall
x\ y\
z\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(y,z)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,z)$
$\displaystyle
f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}g\triangleq{}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{comp}}}(g,f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}:{}\forall
x\ y\
\to(f:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}}\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}f=f$
$\displaystyle
f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}}=f$
$\displaystyle(f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}g)\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}h=f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}(g\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}h)$
$\displaystyle\forall x\ y\ f\
g\to(p,q:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g))\to
p=q$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)\to
f=g$ $\lrcorner$

Some of the equations of $\mathcal{T}_{\mathbf{Cat}}$ can be replaced by
operations targeting the sort
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)$.
However, some equations cannot be avoided, namely the propositionality of
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}$
and the reflection rule
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)\to
f=g$.

An alternative to the theory of categories is the theory of $E$-categories
[Acz95, Pal17], which does not include equations. An $E$-category is
essentially a category enriched over setoids, i.e. with a setoid of morphisms
between any two objects, except that the categorical laws are expressed using
the relations of the setoids.

######  Example 4.0.

The GAT $\mathcal{T}_{{E\text{-}\mathbf{Cat}}}$ of $E$-categories is presented
by the following signature:

$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}:\mathbb{T}_{{E\text{-}\mathbf{Cat}}}$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}:{\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{Ob}}}\to\mathbb{T}_{{E\text{-}\mathbf{Cat}}}$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}:\forall
x\
y\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\to\mathbb{T}_{{E\text{-}\mathbf{Cat}}}$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,x)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{comp}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(y,z)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,z)$
$\displaystyle
f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}g\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{comp}}}(g,f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}:(f:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{sym}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(g,f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{trans}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(g,h)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,h)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{assoc}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}(g\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}h),(f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}g)\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}h)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{idl}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}}\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}f,f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{idr}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}},f)$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{cong\text{-}\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,h)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(g,i)\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}g,h\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}i)$

The GAT $\mathcal{T}_{\mathbf{Cat}}$ is isomorphic to the extension of
$\mathcal{T}_{{E\text{-}\mathbf{Cat}}}$ by the equations

$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)\to
f=g,$
$\displaystyle(p:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g))\to
p={\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}.$
$\lrcorner$

######  Example 4.0.

The GAT $\mathcal{T}_{\mathbf{MonCat}}$ of (weak) monoidal categories is the
extension of $\mathcal{T}_{\mathbf{Cat}}$ by the following operations:

$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{I}}}:{}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}},$
$\displaystyle\\_\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}\\_:{}{\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{Ob}}}\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}},$
$\displaystyle\\_\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}\\_:{}{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,x^{\prime})\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(y,y^{\prime})\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}y,x^{\prime}\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}y^{\prime}),$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{\alpha}}}:{}x\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}(y\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}z)\mathrel{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\cong}}}}(x\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}y)\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}z,$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{\lambda}}}:{}x\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}I\mathrel{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\cong}}}}x,$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{\rho}}}:{}I\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}x\mathrel{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\cong}}}}x,$

and equations (or operations returning in
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}$)
expressing the functoriality of
$\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}$,
the naturality of $\alpha$, $\lambda$ and $\rho$, and the pentagon and
triangle coherence laws.  $\lrcorner$

######  Example 4.0.

The GAT $\mathcal{T}_{\mathbf{StrMonCat}}$ of strict monoidal categories is
the extension of $\mathcal{T}_{\mathbf{MonCat}}$ by the following equations: x
⊗(y ⊗z) = (x ⊗y) ⊗z,

α_x,y,z = id,
x ⊗I = x,

λ_x = id,

I ⊗x = x,

ρ_x = id.

######  Example 4.0.

The SOGAT $\mathcal{T}_{\mathsf{Id}}$ of weak identity types is specified by
the following signature:

$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}:\mathbb{T}_{\mathsf{Id}},$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}\to{(\mathbb{T}_{\mathsf{Id}})}_{\mathsf{rep}},$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}:(A:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})(x:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))(y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}},$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}:(A:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})(x:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}(A,x,x)),$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{J}}}:(A:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})(x:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))(P:(y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))(p:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}(A,x,y)))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})$
$\displaystyle\quad(d:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(P(x,{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}})))(y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))(p:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}(A,x,y)))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(P(y,p)),$
$\displaystyle{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{J_{\mathnormal{\beta}}}}}:(A:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})(x:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))(P:(y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A))(p:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}(A,x,y)))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})$
$\displaystyle\quad(d:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(P(x,{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}})))\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}(P(x,\mathsf{refl}),{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{J}}}(A,x,P,d,x,{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}),d)).$

Note that $\mathcal{T}_{\mathsf{Id}}$ is a SOGAT without equations.
$\lrcorner$

######  Example 4.0.

The SOGAT $\mathcal{T}_{\mathsf{Id}_{s}}$ of strict identity types is the
extension of $\mathcal{T}_{\mathsf{Id}}$ by equations J(A,x,P,d,x,refl) =
refl,

J_β= refl.  $\lrcorner$

###  4.2. Structure of the types of a SOGAT

Because SOGATs are $(\Sigma,\Pi_{\mathsf{rep}})$-CwFs that are presented
without equations between types or representable types, their types admit
simple normal forms: they are the free closure of the generating types by the
operations of a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF.

There is a set $\mathsf{GenTy}_{\mathcal{T}}$ of generating types, which can
be read from the cellular presentation of $\mathcal{T}$. For example, the
generating types of $\mathcal{T}_{\mathbf{Cat}}$ are
$(\vdash{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}\
\mathsf{type})$,
$(x,y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}\vdash{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\
\mathsf{type})$ and
$(x,y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}},f,g:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)\vdash{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)\
\mathsf{type})$.

Similarly, there is a set $\mathsf{GenRepTy}_{\mathcal{T}}$ of generating
representable types, with an inclusion
$\mathsf{GenRepTy}_{\mathcal{T}}\hookrightarrow\mathsf{GenTy}_{\mathcal{T}}$.

A basic type of $\mathcal{T}$ is a type of the form
$(\Gamma\vdash{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)\
\mathsf{type})$, where
$\sigma:\Gamma\to\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
for a generating type
$(\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}\vdash{\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}}$.
The basic representable types are defined similarly. A basic non-representable
type is a basic type whose generating type is in
$(\mathsf{GenTy}_{\mathcal{T}}\backslash\mathsf{GenRepTy}_{\mathcal{T}})$.

######  Proposition 4.0.

Any type or representable type in $\mathcal{T}$ can be uniquely obtained from
the basic non-representable types and basic representable types, and from the
operations $\mathbf{1}$-, $\Sigma$-, $\Pi_{\mathsf{rep}}$ and the inclusion
from representable types into types. ∎

###  4.3. Functorial semantics

######  Definition 4.0.

An internal model of $\mathcal{T}$ in a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF
$\mathcal{C}$ is a $(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism

$\mathbb{C}:\mathcal{T}\to\mathcal{C}.$

We often write $X_{\mathcal{C}}$, $A_{\mathcal{C}}$, $a_{\mathcal{C}}$, etc.,
or even just $X$, $A$, $a$, etc. instead of $\mathbb{C}(X)$, $\mathbb{C}(A)$,
$\mathbb{C}(a)$, etc. for the application of the
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism $\mathbb{C}$ on objects, morphisms,
types and terms.

By the universal property of $\mathcal{T}$, an internal model in $\mathcal{C}$
is uniquely determined by the image of the generators of $\mathcal{T}$, that
is by an interpretation of the signature $\mathcal{T}$ in $\mathcal{C}$.

######  Definition 4.0.

A model of $\mathcal{T}$ consists of a category $\mathcal{C}$ with a terminal
object, along with an internal model of $\mathcal{T}$ in the
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF $\widehat{\mathcal{C}}$, that is a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF morphism
$\mathbb{C}:\mathcal{T}\to\widehat{\mathcal{C}}$.  $\lrcorner$

######  Example 4.0.

A model of the SOGAT $\mathcal{T}_{\mathsf{Id}}$ of weak identity types is
exactly a CwF equipped with weak identity types.

However, the models of the SOGAT $\mathcal{T}_{\mathbf{Cat}}$ are not
categories, but pairs $(\mathcal{C},\mathcal{D})$ where $\mathcal{C}$ is a
base category and $\mathcal{D}$ is an internal category in
$\mathbf{Psh}(\mathcal{C})$. In section 4.4 we will define contextual models.
In the case of $\mathcal{T}_{\mathbf{Cat}}$ we recover categories: the
contextual models of $\mathcal{T}_{\mathbf{Cat}}$ are the models
$(\mathcal{C},\mathcal{D})$ such that $\mathcal{C}$ is the terminal category
$1_{\mathbf{Cat}}$. $\mathcal{D}$ is then an internal category in
$\mathbf{Psh}(1_{\mathbf{Cat}})$, i.e. an external category.  $\lrcorner$

Given a model $\mathcal{C}$ of $\mathcal{T}$ and a closed sort
$X\in\mathcal{T}$, we will write $(\Gamma\vdash x:X)\in\mathcal{C}$ to
indicate that $x:X_{\mathcal{C}}(\Gamma)$. Given a dependent sort $(X\vdash Y\
\mathsf{type})\in\mathcal{T}$, we will write $(\Gamma\vdash
y:Y(x))\in\mathcal{C}$ to indicate that $y:Y_{\mathcal{C}}(\Gamma,x)$. We may
also write $(\gamma:\Gamma\vdash x(\gamma):X)\in\mathcal{C}$ and
$(\gamma:\Gamma\vdash y(\gamma):Y(x(\gamma)))\in\mathcal{C}$.

######  Definition 4.0.

A weak morphism $F$ of models of $\mathcal{T}$ consists of a functor
$F:\mathcal{C}\to\mathcal{D}$ such that:

  * •

The functor $F$ weakly preserves terminal objects.

  * •

For every object $X\in\mathcal{T}$, we have a transformation

$F_{X}:(\Gamma\in\mathcal{C})\to X_{\mathcal{C}}(\Gamma)\to
X_{\mathcal{D}}(F(\Gamma))$

contravariantly natural in $\Gamma$.

  * •

For every morphism $\alpha:X\to Y$, the following square commutes

${X_{\mathcal{C}}(\Gamma)}$${X_{\mathcal{D}}(F(\Gamma))}$${Y_{\mathcal{C}}(\Gamma)}$${Y_{\mathcal{D}}(F(\Gamma))}$$\scriptstyle{\alpha_{\mathcal{C}}(\Gamma)}$$\scriptstyle{F_{X}}$$\scriptstyle{\alpha_{\mathcal{D}}(F(\Gamma))}$$\scriptstyle{F_{Y}}$

  * •

Remark that we obtain, for every object $X\in\mathcal{T}$ and type $(X\vdash
A\ \mathsf{type})\in\mathcal{T}$, a transformation

$\displaystyle F_{A}:(\Gamma\in\mathcal{C})\to(x:X_{\mathcal{C}}(\Gamma))\to
A_{\mathcal{C}}(x)\to A_{\mathcal{D}}(F_{X}(x))$

contravariantly natural in $\Gamma$, uniquely specified by the equation
$F_{X.A}(x,a)=(F_{X}(x),F_{A}(x,a))$.

  * •

Context extensions are weakly preserved: for every object $X\in\mathcal{T}$,
representable type $(X\vdash A\ \mathsf{type}_{\mathsf{rep}})\in\mathcal{T}$,
object $\Gamma\in\mathcal{C}$ and element $x:X_{\mathcal{C}}(\Gamma)$, the
comparison map

${\left\langle
F(\bm{p}),F_{A}(\bm{q})\right\rangle}:F(\Gamma.A_{\mathcal{C}}[x])\to
F(\Gamma).A_{\mathcal{D}}[F_{X}(x)]$

is an isomorphism.

A morphism is strict if the terminal object and context extensions are
strictly preserved.  $\lrcorner$

We have a $(2,1)$-category of models, weak morphisms and $2$-cells, and a
$1$-category $\mathbf{Mod}_{\mathcal{T}}$ of models and strict morphisms. We
will only work with the $1$-category $\mathbf{Mod}_{\mathcal{T}}$. The
category $\mathbf{Mod}_{\mathcal{T}}$ is locally finitely presentable; in
particular we have an initial model $\mathbf{0}_{\mathcal{T}}$ and more
general freely generated models.

###  4.4. Contextuality and trivial fibrations

Similarly to our definitions of trivial fibrations and contextuality for CwFs,
we can define these notions for models of arbitrary SOGATs using factorization
systems on the category of models.

We define a set
$I=\\{I^{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}\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}}\\}$
of maps in $\mathbf{Mod}_{\mathcal{T}}$, where

$I^{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}:\mathsf{Free}_{\mathcal{T}}(\bm{\Gamma}\vdash\bm{\sigma}:\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})\to\mathsf{Free}_{\mathcal{T}}(\bm{\Gamma}\vdash\bm{x}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\bm{\sigma}))$

is the generic extension of a model by an element of the sort
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$.

We write
$E=\\{E^{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}\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}}\\}$
for the set of codiagonals of maps in $I$.

$E^{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}:\mathsf{Free}_{\mathcal{T}}(\bm{\Gamma}\vdash\bm{x},\bm{y}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\bm{\sigma}))\to\mathsf{Free}_{\mathcal{T}}(\bm{\Gamma}\vdash\bm{x}=\bm{y})$

is the generic extension of a model by a new equation between elements of the
sort
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$.

######  Definition 4.0.

A morphism $F:\mathcal{C}\to\mathcal{D}$ in $\mathbf{Mod}_{\mathcal{T}}$ is a
split trivial fibration if 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}}$
the actions of $F$ on the elements of
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
are split surjections: for every object $\Gamma\in\mathcal{C}$, boundary
$(\gamma:\Gamma\vdash\sigma(\gamma):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})\in\mathcal{C}$
and element $(\gamma:F(\Gamma)\vdash
x(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma)))\in\mathcal{D}$,
there is a lifted element $(\gamma:\Gamma\vdash
x_{0}(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma(\gamma)))\in\mathcal{C}$
such that $F(x_{0})=x$.  $\lrcorner$

The trivial fibrations are the right class of maps in the weak factorization
system generated by $I$. The maps in the left class are called cofibrations.

There is also a notion of non-split trivial fibration.

######  Definition 4.0.

A morphism $F:\mathcal{C}\to\mathcal{D}$ in $\mathbf{Mod}_{\mathcal{T}}$ is a
non-split trivial fibration if 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}}$
the actions of $F$ on the elements of
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
are non-split surjections.  $\lrcorner$

Finally, contextuality is specified using the notion of contextual
isomorphism.

######  Definition 4.0.

A morphism $F:\mathcal{C}\to\mathcal{D}$ in $\mathbf{Mod}_{\mathcal{T}}$ is a
contextual isomorphism if 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}}$,
the actions of $F$ on the elements of
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
are bijections.  $\lrcorner$

The contextual isomorphisms are the right class of maps of the orthogonal
factorization system generated by $I$, or equivalently in the weak
factorization system generated by $I\cup E$.

Any morphism $F:\mathcal{C}\to\mathcal{D}$ admits a unique (up to isomorphism)
factorization $\mathcal{C}\to\mathsf{cxlim}(F)\to\mathcal{D}$ where
$\mathcal{C}\to\mathsf{cxlim}(F)$ is a $(I\cup E)$-cofibration and
$\mathsf{cxlim}(F)\to\mathcal{D}$ is a contextual isomorphism. The model
$\mathsf{cxlim}(F)$ is called the contextual image of $F$.

The contextual core $\mathsf{cxl}(\mathcal{C})$ of a model $\mathcal{C}$ is
the contextual image of the unique morphism
$\mathbf{0}_{\mathcal{T}}\to\mathcal{C}$. The map
$\mathsf{cxl}(\mathcal{C})\to\mathcal{C}$ is a contextual isomorphism by
definition. When the map $\mathsf{cxl}(\mathcal{C})\to\mathcal{C}$ is also an
isomorphism in $\mathbf{Mod}_{\mathcal{T}}$, we say that $\mathcal{C}$ is
contextual.

######  Conjecture 4.0.

There is a functor

$\mathbf{0}_{\mathcal{T}}[-]:\mathcal{T}^{\mathsf{op}}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{cxl}}.$

It is fully faithful, and its essential image consists of the finite
$I$-cellular models of $\mathcal{T}$.  $\lrcorner$

###  4.5. Homotopy relations

The data of homotopy relations on a SOGAT equips every sort of the SOGAT with
a notion of identification or sameness that is weaker than definitional
equality. It does not presuppose that these relations are well-behaved, for
example they could fail to even be symmetric and transitive. The well-
behavedness of homotopy relations is encoded in the notion of external
univalence.

######  Definition 4.0.

The data of homotopy relations on a SOGAT $\mathcal{T}$ consists, for every
generating sort
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$,
of a reflexive type-valued relation on its elements:

$\displaystyle\\_\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\\_)}\\_:(\sigma:\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})(x,y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma))\to\mathbb{T},$
$\displaystyle\mathsf{hrefl}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\\_)}:(\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))\to
x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}x.$
$\lrcorner$

We use $\mathsf{hrefl}$ for the constant homotopy, to distinguish it from
reflexivity witnesses of other relations, such as
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}$
in $\mathcal{T}_{\mathcal{T}}$, or $\mathsf{refl}$ in a
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwF.

######  Example 4.0.

The theory $\mathcal{T}_{{E\text{-}\mathbf{Cat}}}$ of $E$-categories is
equipped with the following homotopy relations:

$\displaystyle(x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}}y)\triangleq(x\mathrel{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\cong}}}}y),$
$\displaystyle\mathsf{hrefl}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}}(x)\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}},$
$\displaystyle(f\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)}g)\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g),$
$\displaystyle\mathsf{hrefl}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y)}(f)\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}(f),$
$\displaystyle(p\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)}q)\triangleq\mathbf{1}$
$\displaystyle\mathsf{hrefl}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)}(p)\triangleq\star,$

where
$(x\mathrel{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\cong}}}}y)$
is the sort of isomorphisms between $x$ and $y$.

$\displaystyle(x\mathrel{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\cong}}}}y)$
$\displaystyle{}\triangleq(f:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y))\times(g:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(y,x))$
$\displaystyle\quad\times{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}g,{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}})\times{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(g\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\circ}}}}f,{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{id}}}).$

The theories $\mathcal{T}_{\mathbf{Cat}}$, $\mathcal{T}_{\mathbf{MonCat}}$ and
$\mathcal{T}_{\mathbf{StrMonCat}}$, which can be seen as extensions of
$\mathcal{T}_{{E\text{-}\mathbf{Cat}}}$, are equipped with the same homotopy
relations.  $\lrcorner$

######  Example 4.0.

The theory $\mathcal{T}_{\mathsf{Id}}$ of weak identity types is equipped with
the following homotopy relations:

$\displaystyle(A\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}}B)\triangleq(A\simeq
B),$
$\displaystyle\mathsf{hrefl}_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}(A)\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}_{A},$
$\displaystyle(x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A)}y)\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}_{A}(x,y)),$
$\displaystyle\mathsf{hrefl}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Tm}}}(A)}(x)\triangleq{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{refl}}}(x).$

where $(x\simeq y)$ is the sort of equivalences between $A$ and $B$.
Equivalences are defined to be type-valued relations that are functional in
both directions:

$\displaystyle(A\simeq B)$ $\displaystyle{}\triangleq(R:A\to
B\to{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}})$
$\displaystyle\quad\times((a:A)\to\mathrm{isContr}((b:B)\times R(a,b))$
$\displaystyle\quad\times((b:B)\to\mathrm{isContr}((a:A)\times R(a,b)).$

Note that $(b:B)\times R(a,b)$ and $(a:A)\times R(a,b)$ are not types
(elements of
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ty}}}$)
in the absence of $\Sigma$-types, but rather telescopes of length $2$.
Contractibility can be defined for telescopes using the results of section 3.

In that setting the relation specified by the identity type
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Id}}}_{A}$
is the identity equivalence.  $\lrcorner$

The data of homotopy relations is sufficient to equip
$\mathbf{Mod}_{\mathcal{T}}$ with a notion of weak equivalences, trivial
cofibrations and fibrations. Together with the previously defined
(cofibrations, trivial fibrations) weak factorization system, the category
$\mathbf{Mod}_{\mathcal{T}}$ is equipped with all the data of a model
category, but may still fail to satisfy its axioms.

######  Definition 4.0.

A morphism $F:\mathcal{C}\to\mathcal{D}$ of models of $\mathcal{T}$ is a weak
equivalence if it satisfies the following weak lifting property 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}}$:

Weak lifting:

For every object $\Gamma\in\mathcal{C}$, boundary
$(\gamma:\Gamma\vdash\sigma(\gamma):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})\in\mathcal{C}$
and term $(\gamma:F(\Gamma)\vdash
x(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma)))\in\mathcal{D}$,
there is a lifted term

$(\gamma:\Gamma\vdash
x_{0}(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma(\gamma)))\in\mathcal{C}$

and a homotopy

$(\gamma:F(\Gamma)\vdash
p(\gamma):F(x_{0})(\gamma)\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma))}x(\gamma))\in\mathcal{D}.$

As with trivial fibrations, we actually have two notions of weak equivalences:
split weak equivalences, which come with the data of weak lifts for every
lifting problem, and non-split weak equivalences, for which only the mere
existence of lift is assumed.

######  Example 4.0.

In categories seen as contextual models of $\mathcal{T}_{\mathbf{Cat}}$, the
weak equivalences are the functors that are essentially surjective on objects,
morphisms and equalities between morphisms, i.e. functors that are essentially
surjective on objects and fully faithful. The weak equivalences in
$\mathcal{T}_{\mathbf{MonCat}}$ and $\mathcal{T}_{\mathbf{StrMonCat}}$ are the
same.

Weak equivalences in $\mathcal{T}_{\mathsf{Id}}$ are CwF morphisms
$F:\mathcal{C}\to\mathcal{D}$ that are essentially surjective on types and
terms, i.e. that satisfy the following two weak lifting conditions:

weak type lifting:

For every $\Gamma\in\mathcal{C}$ and $(F(\Gamma)\vdash A\
\mathsf{type})\in\mathcal{D}$, there is some $(\Gamma\vdash A_{0}\
\mathsf{type})\in\mathcal{C}$ and an equivalence $\alpha:F(A_{0})\simeq A$ in
$\mathcal{D}$.

weak term lifting:

For every $(\Gamma\vdash A\ \mathsf{type})\in\mathcal{C}$ and
$(F(\Gamma)\vdash a:F(A))\in\mathcal{D}$, there is some $(\Gamma\vdash
a_{0}:A)\in\mathcal{C}$ and an identification $p:F(a_{0})\simeq_{F(A)}a$ in
$\mathcal{D}$.

$\lrcorner$

######  Definition 4.0.

A morphism $F:\mathcal{C}\to\mathcal{D}$ of models of $\mathcal{T}$ is a
fibration if it satisfies the following path lifting property 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}}$:

Path lifting:

For every object $\Gamma\in\mathcal{C}$, boundary
$(\gamma:\Gamma\vdash\sigma(\gamma):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})\in\mathcal{C}$,
terms $(\gamma:F(\Gamma)\vdash
x(\gamma),y(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma)))\in\mathcal{D}$
and homotopy $(\gamma:F(\Gamma)\vdash
p(\gamma):F(x)(\gamma)\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma))}y(\gamma))\in\mathcal{D}$,
there is a lifted homotopy

$(\gamma:\Gamma\vdash
p_{0}(\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(\gamma))}y_{0}(\gamma))\in\mathcal{C}$

such that $F(y_{0})=y$ and $F(p_{0})=p$.

These fibrations could be called right fibrations, since their lifting
property only involves homotopies with a fixed left endpoint. We could also
consider a notion of left fibration.

The fibrations are the right class of maps of a weak factorization system
generated by
$J=\\{J^{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}\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}}\\}$,
where

$J^{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}:\mathsf{Free}_{\mathcal{T}}(\bm{\Gamma}\vdash\bm{x}:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\bm{\sigma}))\to\mathsf{Free}_{\mathcal{T}}(\bm{\Gamma}\vdash\bm{p}:\bm{x}\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\bm{\sigma})}\bm{y}).$

Maps in the left class are called trivial cofibrations.

######  Example 4.0.

Fibrations in categories seen as contextual models of
$\mathcal{T}_{\mathbf{Cat}}$ are isofibrations: functors
$F:\mathcal{C}\to\mathcal{D}$ such that for every isomorphism $g:F(x)\cong y$
in $\mathcal{D}$, there is an isomorphism $g_{0}:x\cong y_{0}$ in
$\mathcal{C}$ such that $F(y_{0})=y$ and $F(g_{0})=g$.

Fibrations in models of $\mathcal{T}_{\mathsf{Id}}$ are CwF morphisms that
satisfy lifting properties for equivalences and identifications.  $\lrcorner$

Without further assumptions, these classes of maps may fail to satisfy the
axioms of a model structure (see section 4.6). We won’t need all axioms in
this paper, but we need some directions of the $2$-out-of-$3$ property for
weak equivalences.

######  Definition 4.0.

We say that the homotopy relations on $\mathcal{T}$ are transitive if 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 can derive

$\forall\sigma\ x\ y\
z\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)\to(y\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}z)\to(x\sim_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma)}z)$

in $\mathcal{T}$.  $\lrcorner$

######  Lemma 4.0.

Let $\mathcal{C}\xrightarrow{F}\mathcal{D}\xrightarrow{G}\mathcal{E}$ be a
composable pair of morphisms. If both $G$ and $G\circ F$ are weak
equivalences, then $F$ is also a weak equivalence.

###### Proof.

Let
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
be a generating sort of $\mathcal{T}$ and take
$(\gamma:\Gamma\vdash\sigma(\gamma):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})\in\mathcal{C}$
and $(\gamma:F(\Gamma)\vdash
a(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma)))\in\mathcal{D}$.
Since $G\circ F$ is a weak equivalence, we can find a lift
$(\gamma:\Gamma\vdash
a_{0}(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma(\gamma)))\in\mathcal{C}$
and a homotopy $(\gamma:G(F(\Gamma))\vdash
p(\gamma):G(F(a_{0}))(\gamma)\sim_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}G(a)(\gamma))\in\mathcal{E}$.
Since $G$ is a weak equivalence, we can find a lift $(\gamma:F(\Gamma)\vdash
p_{0}(\gamma):F(a_{0})(\gamma)\sim_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}a(\gamma))$
of the homotopy $p$. Then $p_{0}$ witnesses the fact that $a_{0}$ is a weak
lift of $a$. ∎

######  Lemma 4.0.

Let $\mathcal{C}\xrightarrow{F}\mathcal{D}\xrightarrow{G}\mathcal{E}$ be a
composable pair of morphisms. Assume that the homotopy relations of
$\mathcal{T}$ are transitive. If both $G$ and $F$ are weak equivalences, then
$G\circ F$ is also a weak equivalence.

###### Proof.

Let
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$
be a generating sort of $\mathcal{T}$ and take
$(\gamma:\Gamma\vdash\sigma(\gamma):\partial{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}})\in\mathcal{C}$
and $(\gamma:G(F(\Gamma))\vdash
a(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(G(F(\sigma))(\gamma)))\in\mathcal{E}$.
Since $G$ is a weak equivalence, we can find a lift $(\gamma:F(\Gamma)\vdash
a_{0}(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(F(\sigma)(\gamma)))\in\mathcal{D}$
and a homotopy $(\gamma:G(F(\Gamma))\vdash
p_{0}(\gamma):G(a_{0})(\gamma)\sim_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}a(\gamma))\in\mathcal{E}$.
Since $F$ is a weak equivalence, we can find a lift $(\gamma:\Gamma\vdash
a_{1}(\gamma):{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma(\gamma)))\in\mathcal{C}$
and a homotopy $(\gamma:F(\Gamma)\vdash
p_{1}(\gamma):F(a_{0})(\gamma)\sim_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}a_{0}(\gamma))\in\mathcal{D}$.
By transitivity, we obtain a homotopy $(\gamma:G(F(\Gamma))\vdash
G(p_{0})(\gamma)\cdot
p_{1}(\gamma):G(F(a_{1}))(\gamma)\sim_{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}a(\gamma))\in\mathcal{E}$.
This proves that $a_{1}$ is a weak lift of $a$ along $G\circ F$. ∎

###  4.6. External univalence

The notion of external univalence then captures the well-behavedness of
homotopy relations on a SOGAT.

Here a $(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Id}_{\mathsf{ws}})$-CwF is a
$(\Sigma,\Pi_{\mathsf{rep}})$-CwF equipped with weakly stable identity types
satisfying function extensionality. We have not defined weakly stable identity
types, but they are only needed for this definition, which is only used to
define the notion of external univalence.

######  Definition 4.0.

Let $\mathcal{C}$ be a
$(\Sigma,\Pi_{\mathsf{rep}},\mathsf{Id}_{\mathsf{ws}})$-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 saturated
(or that the internal model is univalent) if for every generating sort
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}$,
the dependent type

$(y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma))\times(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)$

is contractible over the context
$(\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))$.
$\lrcorner$

Note that the above definition also makes sense for
$(\Sigma,\Pi_{\mathsf{rep}},{\mathsf{Id}})$-CwFs.

######  Definition 4.0.

We say that $\mathcal{T}$ satisfies external univalence if $\mathcal{T}$ can
be equipped with weakly stable identity types that satisfy function
extensionality and saturation.  $\lrcorner$

The following conjecture was made in [Boc22].

######  Conjecture 4.0.

A SOGAT $\mathcal{T}$ satisfies external univalence if and only if the
category $\mathbf{Mod}_{\mathcal{T}}^{\mathsf{cxl}}$, equipped with the
previously defined classes of cofibrations, weak equivalences and fibrations,
is a left-semi model category.  $\lrcorner$

######  Example 4.0.

The theories $\mathcal{T}_{\mathbf{Cat}}$, $\mathcal{T}_{\mathbf{MonCat}}$ and
$\mathcal{T}_{\mathbf{StrMonCat}}$ of categories, monoidal categories and
strict monoidal categories all satisfy external univalence with respect to the
homotopy relations defined in section 4.5.

Indeed, the fact that $\mathcal{T}_{\mathbf{Cat}}$ satisfies external
univalence is proven in [Boc22]. Using the methods presented in that paper, in
order to prove that $\mathcal{T}_{\mathbf{MonCat}}$ and
$\mathcal{T}_{\mathbf{StrMonCat}}$ satisfy external univalence, it suffices to
additionally show that the additional operations of
$\mathcal{T}_{\mathbf{MonCat}}$ and $\mathbf{StrMonCat}$ preserve isomorphisms
in a way that preserves identities. This only needs to be checked for
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{I}}}$
and
$\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}$;
it is immediate for
${\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{I}}}$
and follows from the bifunctoriality for
$\mathbin{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\bm{\otimes}}}}$.
$\lrcorner$

######  Example 4.0.

The theory $\mathcal{T}_{\mathsf{Id}}$ of weak identity types satisfies
external univalence for the homotopy relations of section 4.5.  $\lrcorner$

##  5\. Equational extensions and conservativity

###  5.1. Equational extensions

We now define the notion of equational extension of a SOGAT. Let $\mathcal{T}$
be a SOGAT equipped with homotopy relations.

An equational extension of $\mathcal{T}$ is an extension
$\mathcal{T}\to\mathcal{T}_{E}$ of SOGATs, where $E$ is a family of homotopies
in $\mathcal{T}$. In $\mathcal{T}_{E}$, all the homotopies in $E$ become
definitional equalities. Here, a homotopy in $\mathcal{T}$ is a tuple
$({\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}},\Gamma,\sigma,x,y,p)$,
where
${\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}}$
is a generating sort and $(\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(\gamma))}y(\gamma))\in\mathcal{T}$
is a homotopy between $x$ and $y$ over $\Gamma$.

######  Definition 5.0.

Let $E$ be a family of homotopies of $\mathcal{T}$; elements of $E$ are said
to be marked.

The equational extension of $\mathcal{T}$ by $E$ is the SOGAT
$\mathcal{T}_{E}$ defined by extending $\mathcal{T}$ by equations
$(\gamma:\Gamma\vdash x=y)$ and $(\gamma:\Gamma\vdash
p(\gamma)=\mathsf{hrefl}_{{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{S}}}(\sigma(\gamma))}(x(\gamma)))$
for every marked 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(\gamma))}y(\gamma))\in
E$.  $\lrcorner$

The following are examples of equational extensions of first-order GATs.

######  Examples 5.0.

  1. (1)

The extension
$\mathcal{T}_{{E\text{-}\mathbf{Cat}}}\to\mathcal{T}_{\mathbf{Cat}}$ is the
equational extension obtained by marking
$p:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g)$
over the context
$(x,y:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Ob}}},f,g:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{Hom}}}(x,y),p:{\color[rgb]{0.94921875,0.375,0.20703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.375,0.20703125}{\mathbf{EqHom}}}(f,g))$.

  2. (2)

The extension
$\mathcal{T}_{\mathbf{MonCat}}\to\mathcal{T}_{\mathbf{StrMonCat}}$ is the
equational extension obtained by marking the associator and unitors in
$\mathcal{T}_{\mathbf{MonCat}}$.

  3. (3)

We can also consider the extension
$\mathcal{T}_{{E\text{-}\mathbf{Cat}}}\to{(\mathcal{T}_{{E\text{-}\mathbf{Cat}}})}_{E}$
obtained by only marking the unitality and associativity laws. This extension
can be better behaved than $\mathcal{T}_{\mathbf{Cat}}$ for some applications.
Indeed, ${(\mathcal{T}_{{E\text{-}\mathbf{Cat}}})}_{E}$ has decidable
equality, while $\mathcal{T}_{\mathbf{Cat}}$ does not (e.g. by reduction to
the undecidability of the word problem for groups).  $\lrcorner$

We give some examples of equational extensions of type theories, obtained by
marking a family of type equivalences and identifications between terms.

######  Examples 5.0.

  1. (1)

For the extensions from weak computation rules to strict computation rules, we
mark the computation rules that should be made strict. For example, in the
case of identity types, we mark the family of identifications
$\mathsf{J}_{\beta}(P,d):\mathsf{Id}(\mathsf{J}_{A,x}(P,d,\mathsf{refl}),d)$
over the context $(A,x,P,d)$.

  2. (2)

When considering the extension from inductive natural numbers to natural
numbers with a strictly associative addition, we proceed in in two steps.
First we extend the base theory $\mathcal{T}_{0}$ by adding

$\mathsf{plus}:\mathbf{N}\to\mathbf{N}\to\mathbf{N}$

as a new primitive operation, along with some of the equalities that it
satisfies, such as

$\displaystyle\mathsf{plus}_{0}:\forall x\to\mathsf{plus}(0,x)\simeq x,$
$\displaystyle\mathsf{plus}_{1}:\forall x\to\mathsf{plus}(x,0)\simeq x,$
$\displaystyle\mathsf{plus}_{2}:\forall x\ y\
z\to\mathsf{plus}(\mathsf{plus}(x,y)),z)\simeq\mathsf{plus}(x,\mathsf{plus}(y,z)).$

The operation $\mathsf{plus}$ is homotopic to the usual inductively defined
addition, but not strictly equal to it. The weak type theory $\mathcal{T}$ is
then this extended theory. Because $\mathcal{T}$ can be seen as the extension
of $\mathcal{T}_{0}$ by new elements of contractible sorts, it should be a
conservative extension of $\mathcal{T}_{0}$ (see section 5.3).

As a second step, we consider the equational extension of $\mathcal{T}$
obtained by marking the identifications $\mathsf{plus}_{0}$,
$\mathsf{plus}_{1}$, $\mathsf{plus}_{2}$, etc. Thus the extended theory
$\mathcal{T}_{E}$ includes the strict equalities $\mathsf{plus}(0,x)=x$,
$\mathsf{plus}(x,0)=x$,
$\mathsf{plus}(\mathsf{plus}(x,y),z)=\mathsf{plus}(x,\mathsf{plus}(y,z))$,
etc. It also includes the strict equalities $\mathsf{plus}_{0}=\mathsf{refl}$,
$\mathsf{plus}_{1}=\mathsf{refl}$, $\mathsf{plus}_{2}=\mathsf{refl}$, etc.

  3. (3)

Similarly, we can consider the extension of type theory by a composition
operation on paths satisfying strictly the laws of a $1$-groupoid. We start by
extending the base theory $\mathcal{T}_{0}$ by new elements

$\displaystyle\mathsf{trans}:(x\simeq y)\to(y\simeq z)\to(x\simeq z),$
$\displaystyle\mathsf{inv}:(x\simeq y)\to(y\simeq x),$
$\displaystyle\mathsf{idl}:\mathsf{trans}(\mathsf{refl},p)\simeq p,$
$\displaystyle\mathsf{inv}\text{-}\mathsf{refl}:\mathsf{inv}(\mathsf{refl})\simeq\mathsf{refl},$
$\displaystyle\mathsf{idr}:\mathsf{trans}(p,\mathsf{refl})\simeq p,$
$\displaystyle\mathsf{assoc}:\mathsf{trans}(\mathsf{trans}(p,q),r)\simeq\mathsf{trans}(p,\mathsf{trans}(q,r)),$
$\displaystyle\mathsf{inv}\text{-}\mathsf{l}:\mathsf{trans}(\mathsf{inv}(p),p)\simeq\mathsf{refl},$
$\displaystyle\mathsf{inv}\text{-}\mathsf{r}:\mathsf{trans}(p,\mathsf{inv}(p))\simeq\mathsf{refl},$

along with some higher-dimensional identifications that are needed to ensure
that this is an extension by new elements of _contractible_ sorts. We can see
$\mathsf{idl}$ and $\mathsf{inv}\text{-}\mathsf{refl}$ as identifications
specifying $\mathsf{trans}$ and $\mathsf{inv}$ using the universal property of
$\mathsf{Id}$-types, so we need additional identifications specifying
$\mathsf{idr}$, $\mathsf{assoc}$, $\mathsf{inv}\text{-}\mathsf{l}$ and
$\mathsf{inv}\text{-}\mathsf{r}$:

$\displaystyle-:\mathsf{idr}(\mathsf{refl})\simeq\mathsf{idl}(\mathsf{refl}),$
$\displaystyle-:\mathsf{assoc}(p,q,\mathsf{refl})\simeq\dots,$
$\displaystyle-:\mathsf{inv}\text{-}\mathsf{l}(\mathsf{refl})\simeq\dots,$
$\displaystyle-:\mathsf{inv}\text{-}\mathsf{r}(\mathsf{refl})\simeq\dots,$

where the right-hand sides should be the usual proofs of these laws.

We obtain a theory $\mathcal{T}$ that should be a conservative extension of
$\mathcal{T}_{0}$.

Secondly, we consider the equational extension of $\mathcal{T}$ obtained by
marking the identifications $\mathsf{idl}$,
$\mathsf{inv}\text{-}\mathsf{refl}$, etc., as well as the additional higher-
dimensional identifications.

  4. (4)

To consider the extension of a type theory with a new universe of strict
propositions, we would also perform two steps. As a first step, we introduce a
new constant type $\mathsf{SProp}$, along with an equivalence
$\mathsf{SProp}\simeq\mathsf{HProp}$ with the type $\mathsf{HProp}$ of
propositions. We write $F:\mathsf{SProp}\to\mathsf{HProp}$ for the associated
transport function.

Secondly, we mark the family of identifications

$(A:\mathsf{SProp})(a,b:F(A))\to\mathsf{Id}(a,b).$

In the resulting strict type theory, the only way to obtain closed elements of
$\mathsf{SProp}$ is to use the inverse of the equivalence $F$ to replace
elements of $\mathsf{HProp}$ by elements in $\mathsf{SProp}$.

Note that the equational extension that marks instead the family of
identifications

$(A:\mathsf{HProp})(a,b:A)\to\mathsf{Id}(a,b)$

is not a conservative extension in the absence of UIP. Indeed, as remarked in
[GCST19], if all propositions are strict propositions, then UIP holds.

  5. (5)

So far we have only marked identification between terms. We can also mark
equivalences between types.

For example, let $\mathcal{T}$ be a type theory with a weak Tarski universe
closed under identity types. This means that $\mathcal{T}$ extends
$\mathcal{T}_{\mathsf{Id}}$ with:

$\displaystyle\mathcal{U}:\mathsf{Ty},$
$\displaystyle\mathsf{El}:\mathcal{U}\to\mathsf{Ty},$
$\displaystyle\widehat{\mathsf{Id}}:(A:\mathcal{U})\to\mathsf{El}(A)\to\mathsf{El}(A)\to\mathcal{U},$
$\displaystyle\alpha:\forall A\ x\
y\to\mathsf{El}(\widehat{\mathsf{Id}}(A,x,y))\simeq\mathsf{Id}(\mathsf{El}(A),x,y).$

We then mark the equivalence $\alpha$ over the context $(A,x,y)$. The
resulting theory $\mathcal{T}_{E}$ then has a strict Tarski universe.

Note that we have assumed that the same definition of equivalence (say
relational equivalences) is used in the specification of $\alpha$ and in the
specification of the homotopy relations of $\mathcal{T}$ in section 4.5.

If $\alpha$ were instead a family of say half-adjoint equivalences, we would
need to construct the extension in two steps similarly to the previous
examples. In the first step, we add a new family $\alpha^{\prime}$ of
relational equivalences, along with homotopies between $\alpha$ and
$\alpha^{\prime}$. In the second step, we consider the equational extension
obtained by marking the equivalences $\alpha^{\prime}$.

  6. (6)

As a last example, we can also mark the universal identification $p$ over the
generic context $(A:\mathsf{Ty},x:A,y:A,p:\mathsf{Id}(x,y))$. The
corresponding strict type theory then includes the equality reflection rule.
Equivalently, one might mark all identifications over arbitrary contexts.
$\lrcorner$

###  5.2. Morita equivalences

We now define the notion of Morita equivalence between SOGATs. In general, two
theories are Morita equivalent when they have equivalent categories of models.
Accordingly, two SOGATs equipped with homotopy relations should be Morita
equivalent when they have equivalent $\infty$-categories of models (provided
that these $\infty$-categories exist). Isaev [Isa18b] has defined a notion of
Morita equivalence between type theories and shown that two theories are
Morita equivalent if and only if their categories of models are Quillen
equivalent (provided that the model or semi-model structures on the categories
of models exist). We give a simpler definition at the level of the classifying
$(\Sigma,\Pi_{\mathsf{rep}})$-CwFs.

Let $\mathcal{T}_{1}\to\mathcal{T}_{2}$ be a morphism of SOGATs, where
$\mathcal{T}_{1}$ is equipped with homotopy relations.

######  Definition 5.0.

We say that the morphism $\mathcal{T}_{1}\to\mathcal{T}_{2}$ is a (split/non-
split) Morita equivalence if the map $\mathcal{T}_{1}\to\mathcal{T}_{2}$ is a
(split/non-split) weak equivalence in $\mathbf{Mod}_{\mathcal{T}_{1}}$.
$\lrcorner$

We have an adjunction between the categories $\mathbf{Mod}_{\mathcal{T}_{1}}$
and $\mathbf{Mod}_{\mathcal{T}_{2}}$ of models of $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$.

${\mathbf{Mod}_{\mathcal{T}_{1}}}$${\mathbf{Mod}_{\mathcal{T}_{2}}}$$\scriptstyle{L}$${\top}$$\scriptstyle{R}$

When $\mathcal{T}_{2}$ is an equational extension of $\mathcal{T}_{1}$, the
right adjoint $R$ is the forgetful functor that forgets that a model satisfies
the additional equations of $\mathcal{T}_{2}$.

We have the following characterizations of Morita equivalences. Condition (1)
is Isaev’s definition of Morita equivalence [Isa18b]. The full proof is left
to future work, but it ought to follow from the same ideas and methods as the
proof of section 4.6.

######  Conjecture 5.0.

Assume that $\mathcal{T}_{1}$ satisfies external univalence. Then the
following conditions are equivalent:

  1. (1)

For every cofibrant model $\mathcal{C}$ of $\mathcal{T}_{1}$, the unit
$\eta_{\mathcal{C}}:\mathcal{C}\to R(L(\mathcal{C}))$ is a weak equivalence in
$\mathbf{Mod}_{\mathcal{T}_{1}}$.

  2. (2)

For every freely generated model $\mathcal{C}$ of $\mathcal{T}_{1}$, the unit
$\eta_{\mathcal{C}}:\mathcal{C}\to R(L(\mathcal{C}))$ is a weak equivalence in
$\mathbf{Mod}_{\mathcal{T}_{1}}$.

  3. (3)

For every finitely generated model $\mathcal{C}$ of $\mathcal{T}_{1}$, the
unit $\eta_{\mathcal{C}}:\mathcal{C}\to R(L(\mathcal{C}))$ is a weak
equivalence in $\mathbf{Mod}_{\mathcal{T}_{1}}$.

  4. (4)

The SOGAT morphism $\mathcal{T}_{1}\to\mathcal{T}_{2}$ is a Morita
equivalence.

###### Proof sketch.

The fact that $\mathcal{T}_{1}$ satisfies external univalence is needed to
ensure that weak equivalences in $\mathbf{Mod}_{\mathcal{T}_{1}}$ satisfy some
closure conditions (some directions of the $2$-out-of-$3$ property and closure
under retracts).

The equivalence between (1) and (2) follows from the fact that every cofibrant
model is a retract of a freely generated model.

The equivalence between (2) and (3) follows from the fact that every
$I$-cellular model is a filtered colimit of finitely generated models (because
$\mathcal{T}$ is a finitary theory).

The equivalence between (3) and (4) follows from section 4.4. ∎

###  5.3. Extensions by contractible sorts

In our examples of equational extensions, we have often considered
compositions $\mathcal{T}_{0}\to\mathcal{T}\to\mathcal{T}_{E}$ of extensions,
where $\mathcal{T}\to\mathcal{T}_{E}$ is an equational extension and
$\mathcal{T}_{0}\to\mathcal{T}$ is the extension of $\mathcal{T}_{0}$ by new
elements of contractible sorts.