Thus, it suffices to show that $\mathcal{F}(\mathbf{y}(x))$ is democratic for
every $x\in\mathbb{T}$, but this follows from the description of
$\mathcal{F}(\mathbf{y}(x))$ in Section 4.3. ∎

######  Proposition 4.12.

The restriction of
$\mathrm{L}:\mathbf{Mod}(\mathbb{T})\to\mathbf{Th}(\mathbb{T})$ to
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\subset\mathbf{Mod}(\mathbb{T})$ is
conservative.

We first show the following lemma.

######  Lemma 4.13.

Let $F:\mathcal{M}\to\mathcal{N}$ be a morphism of models of $\mathbb{T}$ such
that $\mathrm{L}(F):\mathrm{L}(\mathcal{M})\to\mathrm{L}(\mathcal{N})$ is an
equivalence of $\mathbb{T}$-theories. Then, the map

$F(x)_{\Gamma}:\mathcal{M}(x)_{\Gamma}\to\mathcal{N}(x)_{F({\star})(\Gamma)}$

is an equivalence of spaces for any contextual object
$\Gamma\in\mathcal{M}({\star})$ and any object $x\in\mathbb{T}$.

###### Proof.

By induction on the contextual object $\Gamma\in\mathcal{M}({\star})$. When
$\Gamma=1$, the map $F(x)_{1}$ is an equivalence by assumption. Suppose that
$\Gamma=\\{a\\}_{u}$ for some contextual object
$\Gamma^{\prime}\in\mathcal{M}({\star})$, representable arrow $u:y\to z$ in
$\mathbb{T}$ and section
$a:\mathcal{M}({\star})/\Gamma^{\prime}\to\mathcal{M}(z)$. Since
$\mathcal{M}:\mathbb{T}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ commutes with
the polynomial functor $\mathbf{P}_{u}$, the sections
$\mathcal{M}({\star})/\\{a\\}_{u}\to\mathcal{M}(x)$ correspond to the sections
of $\mathcal{M}(\mathbf{P}_{u}x)\to\mathcal{M}(z)$ over
$a:\mathcal{M}({\star})/\Gamma^{\prime}\to\mathcal{M}(z)$. Thus,
$\mathcal{M}(x)_{\\{a\\}_{u}}$ is the pullback

${\mathcal{M}(x)_{\\{a\\}_{u}}}$${\mathcal{M}(\mathbf{P}_{u}x)_{\Gamma^{\prime}}}$${\Delta^{0}}$${\mathcal{M}(z)_{\Gamma^{\prime}}.}$$\scriptstyle{a}$

By the induction hypothesis, $F(\mathbf{P}_{u}x)_{\Gamma^{\prime}}$ and
$F(z)_{\Gamma^{\prime}}$ are equivalences, and thus $F(x)_{\\{a\\}_{u}}$ is an
equivalence. ∎

###### Proof of Proposition 4.12.

Let $F:\mathcal{M}\to\mathcal{N}$ be a morphism between democratic models of
$\mathbb{T}$ and suppose that
$\mathrm{L}(F):\mathrm{L}(\mathcal{M})\to\mathrm{L}(\mathcal{N})$ is an
equivalence of $\mathbb{T}$-theories. We show that $F$ is an equivalence of
models of $\mathbb{T}$. Since the forgetful functor
$\mathbf{Mod}(\mathbb{T})\to\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$
is conservative, it suffices to show that
$F(x):\mathcal{M}(x)\to\mathcal{N}(x)$ is an equivalence of
$\infty$-categories for every object $x\in\mathbb{T}^{\triangleright}$. Lemma
4.13 implies that the square

${\mathcal{M}(x)}$${\mathcal{N}(x)}$${\mathcal{M}({\star})}$${\mathcal{N}(*)}$$\scriptstyle{F(x)}$$\scriptstyle{F({\star})}$

is a pullback for every $x\in\mathbb{T}$. It remains to show that the functor
$F({\star}):\mathcal{M}({\star})\to\mathcal{N}(*)$ is fully faithful and
essentially surjective.

We show by induction on $\Delta$ that
$F({\star}):\mathcal{M}({\star})(\Gamma,\Delta)\to\mathcal{N}(*)(F({\star})(\Gamma),F({\star})(\Delta))$
is an equivalence of spaces for any objects
$\Gamma,\Delta\in\mathcal{M}({\star})$. The case when $\Delta=1$ is trivial.
Suppose that $\Delta=\\{a\\}_{u}$ for some object
$\Delta^{\prime}\in\mathcal{M}({\star})$, representable arrow $u:x\to y$ in
$\mathbb{T}$ and section
$a:\mathcal{M}({\star})/\Delta^{\prime}\to\mathcal{M}(y)$. By definition, we
have a pullback

${\mathcal{M}({\star})(\Gamma,\\{a\\}_{u})}$${\mathcal{M}(x)_{\Gamma}}$${\mathcal{M}({\star})(\Gamma,\Delta^{\prime})}$${\mathcal{M}(y)_{\Gamma}.}$$\scriptstyle{\mathcal{M}(u)_{\Gamma}}$$\scriptstyle{f\mapsto
f^{*}a}$

Then, by the induction hypothesis and Lemma 4.13, the map
$F({\star}):\mathcal{M}({\star})(\Gamma,\\{a\\}_{u})\to\mathcal{N}(*)(F({\star})(\Gamma),F({\star})(\\{a\\}_{u}))$
is an equivalence.

Finally, we show by induction on $\Delta$ that, for any object
$\Delta\in\mathcal{N}(*)$, there exists an object
$\Gamma\in\mathcal{M}({\star})$ such that $F({\star})(\Gamma)\simeq\Delta$.
The case when $\Delta=1$ is trivial. Suppose that $\Delta=\\{b\\}_{u}$ for
some object $\Delta^{\prime}\in\mathcal{N}(*)$, representable arrow $u:x\to y$
in $\mathbb{T}$ and section
$b:\mathcal{N}(*)/\Delta^{\prime}\to\mathcal{N}(y)$. By the induction
hypothesis, we have an object $\Gamma^{\prime}\in\mathcal{M}({\star})$ such
that $F({\star})(\Gamma^{\prime})\simeq\Delta^{\prime}$. By Lemma 4.13, we
have a section $a:\mathcal{M}({\star})/\Gamma^{\prime}\to\mathcal{M}(y)$ such
that $F(y)_{\Gamma^{\prime}}(a)\simeq b$. Then
$F({\star})(\\{a\\}_{u})\simeq\\{b\\}_{u}$. ∎

######  Theorem 4.14.

For an $\infty$-type theory, the restriction of
$\mathrm{L}:\mathbf{Mod}(\mathbb{T})\to\mathbf{Th}(\mathbb{T})$ to
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\subset\mathbf{Mod}(\mathbb{T})$ is an
equivalence

$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\simeq\mathbf{Th}(\mathbb{T}).$

###### Proof.

By Proposition 4.11, the functor
$\mathrm{L}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\to\mathbf{Th}(\mathbb{T})$
has the left adjoint $\mathcal{F}$. By Proposition 4.10, the unit of this
adjunction is invertible. By Proposition 4.12 and the triangle identities, the
counit is also invertible. ∎

##  5 Correspondence between type-theoretic structures and categorical
structures

We discuss a correspondence between type-theoretic structures and categorical
structures. Given an $\infty$-category $\mathcal{C}$ whose objects are small
$\infty$-categories equipped with a certain structure and morphisms are
structure-preserving functors, we try to find an $\infty$-type theory
$\mathbb{T}$ such that $\mathbf{Th}(\mathbb{T})\simeq\mathcal{C}$. Such an
$\infty$-type theory $\mathbb{T}$ can be understood in a couple of ways. Type-
theoretically, $\mathbb{T}$ provides _internal languages_ for
$\infty$-categories in $\mathcal{C}$. We will find type-theoretic structures
corresponding to categorical structures like finite limits and pushforwards.
Categorically, $\mathbb{T}$ gives a _presentation_ of the $\infty$-category
$\mathcal{C}$ as a localization of a presheaf $\infty$-category. Such a
presentation has the advantage that the $\infty$-type theory $\mathbb{T}$
often has a simple universal property from which one can derive a universal
property of $\mathcal{C}$ (see Corollary 5.21 for example).

The fundamental example of such an $\infty$-category $\mathcal{C}$ is
$\mathcal{C}=\mathbf{Lex}_{\infty}$, the $\infty$-category of small left exact
$\infty$-categories. In Section 5.3, we introduce an $\infty$-type theory
$\mathbb{E}_{\infty}$ which is an $\infty$-analogue of Martin-Löf type theory
with extensional identity types. The main result of this section is to
establish an equivalence
$\mathbf{Th}(\mathbb{E}_{\infty})\simeq\mathbf{Lex}_{\infty}$, and this is a
higher analogue of the result of [13]. To do this, we need two preliminaries:
one is the _representable map classifier_ of right fibrations over a left
exact $\infty$-category (Section 5.1) which is used for constructing a
democratic model of $\mathbb{E}_{\infty}$ out of a left exact
$\infty$-category; the other is the notion of _univalence_ in
$\infty$-categories with representable maps (Section 5.2) which for example
makes a type constructor unique up to contractible choice. We also give two
other examples $\mathcal{C}=\mathbf{LCCC}_{\infty}$, the $\infty$-category of
small locally cartesian closed $\infty$-categories (Section 5.4), and
$\mathcal{C}=\mathbf{TT}_{\infty}$, the $\infty$-category of $\infty$-type
theories (Section 5.5). The latter example shows that the notion of
$\infty$-type theories itself can be written in the $\infty$-type-theoretic
language.

###  5.1 The representable map classifier

In this preliminary subsection, we review a _representable map classifier_
over a left exact $\infty$-category $\mathcal{C}$, that is, a classifying
object for the class of representable maps of right fibrations over
$\mathcal{C}$.

######  Definition 5.1.

Let $S$ denote the category

${0}$${1}$${1.}$

The inclusion $\Delta^{1}=\\{0\to 1\\}\to S$ induces a functor
$S\pitchfork\mathcal{C}\to\Delta^{1}\pitchfork\mathcal{C}=\mathcal{C}^{\to}$
for an $\infty$-category $\mathcal{C}$. Note that $S\pitchfork\mathcal{C}$ is
the $\infty$-category of sections in $\mathcal{C}$.

######  Definition 5.2.

Let $\mathcal{C}$ be a left exact $\infty$-category. We define
$\mathcal{R}_{\mathcal{C}}$ to be the largest right fibration over
$\mathcal{C}$ contained in the cartesian fibration
$\mathrm{cod}:\mathcal{C}^{\to}\to\mathcal{C}$ and
$\rho_{\mathcal{C}}:\widetilde{\mathcal{R}}_{\mathcal{C}}\to\mathcal{R}_{\mathcal{C}}$
to be the pullback

${\widetilde{\mathcal{R}}_{\mathcal{C}}}$${S\pitchfork\mathcal{C}}$${\mathcal{R}_{\mathcal{C}}}$${\mathcal{C}^{\to}.}$$\scriptstyle{\rho_{\mathcal{C}}}$

That is, $\mathcal{R}_{\mathcal{C}}$ is the wide subcategory of
$\mathcal{C}^{\to}$ whose morphisms are the pullback squares. We refer to
$\mathcal{R}_{\mathcal{C}}$ as the _representable map classifier_ over
$\mathcal{C}$ and $\rho_{\mathcal{C}}$ as the _generic representable map_ of
right fibrations over $\mathcal{C}$ because of the following proposition.

######  Proposition 5.3.

Let $\mathcal{C}$ be a left exact $\infty$-category.

  1. 1.

$\rho_{\mathcal{C}}:\widetilde{\mathcal{R}}_{\mathcal{C}}\to\mathcal{R}_{\mathcal{C}}$
is a representable map of right fibrations over $\mathcal{C}$.

  2. 2.

For any right fibration $A$ over $\mathcal{C}$, the map

$\mathbf{RFib}_{\mathcal{C}}(A,\mathcal{R}_{\mathcal{C}})\to(\mathbf{RFib}_{\mathcal{C}}/A)_{r}$

defined by the pullback of $\rho_{\mathcal{C}}$ is an equivalence, where
$(\mathbf{RFib}_{\mathcal{C}}/A)_{r}$ denotes the subspace of
$(\mathbf{RFib}_{\mathcal{C}}/A)^{\simeq}$ spanned by the representable maps
over $A$.

###### Proof.

We first observe that
$\rho_{\mathcal{C}}:\widetilde{\mathcal{R}}_{\mathcal{C}}\to\mathcal{R}_{\mathcal{C}}$
is a right fibration, that is, the functor

$(\mathrm{ev}_{1},(\rho_{\mathcal{C}})_{*}):\Delta^{1}\pitchfork\widetilde{\mathcal{R}}_{\mathcal{C}}\to\widetilde{\mathcal{R}}_{\mathcal{C}}\times_{\mathcal{R}_{\mathcal{C}}}\Delta^{1}\pitchfork\mathcal{R}_{\mathcal{C}}$

is an equivalence. Since $\Delta^{1}\pitchfork\mathcal{R}_{\mathcal{C}}$ is a
subcategory of $(\Delta^{1}\times\Delta^{1})\pitchfork\mathcal{C}$ whose
objects are the pullback squares, this follows from the universal property of
pullbacks.

For the representability of $\rho_{\mathcal{C}}$, we use Proposition 2.16. Let
$\kappa_{y}:\mathcal{C}/x\to\mathcal{R}_{\mathcal{C}}$ be a section which
corresponds to an arrow $y\to x$ in $\mathcal{C}$. We show that
$\kappa_{y}^{*}\widetilde{\mathcal{R}}_{\mathcal{C}}$ is representable by $y$.
Since the diagonal map $y\to y\times_{x}y$ is a section of the first
projection, it determines a section
$\delta:\mathcal{C}/y\to\widetilde{\mathcal{R}}_{\mathcal{C}}$ such that the
diagram

${\mathcal{C}/y}$${\widetilde{\mathcal{R}}_{\mathcal{C}}}$${\mathcal{C}/x}$${\mathcal{R}_{\mathcal{C}}}$$\scriptstyle{\delta}$$\scriptstyle{\rho_{\mathcal{C}}}$$\scriptstyle{\kappa_{y}}$

commutes. This square is a pullback. Indeed, for an object $(u:z\to
x)\in\mathcal{C}/x$, the fiber of $\rho_{\mathcal{C}}$ over $\kappa_{y}(u)$ is
the space of sections of $z\times_{x}y\to z$ which is equivalent to the space
of sections of $y\to x$ over $u$.

For the second claim, observe that
$(\mathbf{RFib}_{\mathcal{C}}/\operatorname{colim}_{i\in\mathcal{I}}A_{i})_{r}\simeq\lim_{i\in\mathcal{I}}(\mathbf{RFib}_{\mathcal{C}}/A_{i})_{r}$
for any diagram $(A_{i})_{i\in\mathcal{I}}$ in $\mathbf{RFib}_{\mathcal{C}}$.
Indeed, since $\mathbf{RFib}_{\mathcal{C}}$ is an $\infty$-topos, we have
$(\mathbf{RFib}_{\mathcal{C}}/\operatorname{colim}_{i\in\mathcal{I}}A_{i})^{\simeq}\simeq\lim_{i\in\mathcal{I}}(\mathbf{RFib}_{\mathcal{C}}/A_{i})^{\simeq}$,
and this equivalence is restricted to representable maps by Proposition 2.16.
Then it is enough to show that the map in the statement is an equivalence in
the case when $A$ is representable by some $x\in\mathcal{C}$. By definition
$\mathbf{RFib}_{\mathcal{C}}(\mathcal{C}/x,\mathcal{R}_{\mathcal{C}})\simeq(\mathcal{C}/x)^{\simeq}$.
By Proposition 2.16, $(\mathbf{RFib}_{\mathcal{C}}/(\mathcal{C}/x))_{r}$ is
the space of arrows $y\to x$ of which the pullback along an arbitrary arrow
$z\to x$ exists, but since $\mathcal{C}$ has pullbacks this is
$(\mathcal{C}/x)^{\simeq}$. ∎

######  Remark 5.4.

The representable map classifier in $\mathbf{RFib}_{\mathcal{C}}$ exists even
when $\mathcal{C}$ is not left exact. In the above proof, we have seen that
$(\mathbf{RFib}_{\mathcal{C}}/\operatorname{colim}_{i\in\mathcal{I}}A_{i})_{r}\simeq\lim_{i\in\mathcal{I}}(\mathbf{RFib}_{\mathcal{C}}/A_{i})_{r}$
and that $(\mathbf{RFib}_{\mathcal{C}}/A)_{r}$ is essentially small. Then, by
[36, Proposition 5.5.2.2], the functor
$\mathbf{RFib}_{\mathcal{C}}^{\mathrm{op}}\ni
A\mapsto(\mathbf{RFib}_{\mathcal{C}}/A)_{r}\in\mathbf{S}$ is representable,
and the representing object is the representable map classifier. From the
concrete construction given in Definition 5.2, the construction of the
representable map classifier in the case when $\mathcal{C}$ is left exact is
moreover functorial: any left exact functor $F:\mathcal{C}\to\mathcal{D}$
induces a map of right fibrations
$\mathcal{R}_{\mathcal{C}}\to\mathcal{R}_{\mathcal{D}}$ over $F$.

###  5.2 Univalent representable arrows

In this preliminary subsection, we extend the notion of a univalent map in a
(presentable) locally cartesian closed $\infty$-category [19, 39, 40] to a
notion of a univalent representable arrow in an $\infty$-categories with
representable maps.

######  Definition 5.5.

For objects $x$ and $y$ of an $\infty$-category $\mathcal{C}$ with finite
products, let $\mathrm{Map}(x,y)\to\mathcal{C}$ denote the right fibration
whose fiber over $z$ is $\mathcal{C}/z(x\times z,y\times
z)\simeq\mathcal{C}(x\times z,y)$. It is defined by the pullback

${\mathrm{Map}(x,y)}$${\mathcal{C}/y}$${\mathcal{C}}$${\mathcal{C}.}$$\scriptstyle{({-}\times
x)}$

If $\mathrm{Map}(x,y)$ is representable, we denote by
$\underline{\mathrm{Map}}(x,y)$ the representing object. We define
$\mathrm{Eq}(x,y)$ to be the subfibration of $\mathrm{Map}(x,y)$ spanned by
the equivalences $x\times z\simeq y\times z$. If $\mathrm{Eq}(x,y)$ is
representable, we denote by $\underline{\mathrm{Eq}}(x,y)$ the representing
object.

######  Definition 5.6.

Let $u:x\to y$ be an arrow in a left exact $\infty$-category $\mathcal{C}$. We
regard $u\times y:x\times y\to y\times y$ and $y\times u:y\times x\to y\times
y$ as objects of $\mathcal{C}/y\times y$ and denote by $\mathrm{Eq}(u)$ the
right fibration $\mathrm{Eq}(u\times y,y\times u)\to\mathcal{C}/y\times y$. If
$\mathrm{Eq}(u)$ representable, we denote by $\underline{\mathrm{Eq}}(u)$ the
representing object.

By definition, an arrow $z\to\underline{\mathrm{Eq}}(u)$ corresponds to a
triple $(v_{1},v_{2},w)$ consisting of arrows $v_{1},v_{2}:z\to y$ and an
equivalence $w:v_{1}^{*}x\simeq v_{2}^{*}x$ over $z$.

######  Definition 5.7.

Let $u:x\to y$ be an arrow in a left exact $\infty$-category $\mathcal{C}$
such that $\mathrm{Eq}(u)$ is representable. We have a section
$|\mathrm{id}|:y\to\underline{\mathrm{Eq}}(u)$ over the diagonal $\delta:y\to
y\times y$ corresponding to the identity $\mathrm{id}:x\to x$. We say $u$ is
_univalent_ if the arrow $|\mathrm{id}|:y\to\underline{\mathrm{Eq}}(u)$ is an
equivalence.

######  Proposition 5.8.

Let $u:x\to y$ be an arrow in a left exact $\infty$-category $\mathcal{C}$
such that $\mathrm{Eq}(u)$ is representable. Let
$\kappa_{u}:\mathcal{C}/y\to\mathcal{R}_{\mathcal{C}}$ be the section
corresponding to $u$ by Yoneda. The following are equivalent:

  1. 1.

$u$ is univalent:

  2. 2.

the square

${\mathcal{C}/y}$${\mathcal{R}_{\mathcal{C}}}$${\mathcal{C}/y\times
y}$${\mathcal{R}_{\mathcal{C}}\times_{\mathcal{C}}\mathcal{R}_{\mathcal{C}}}$$\scriptstyle{\kappa_{u}}$$\scriptstyle{\delta}$$\scriptstyle{\delta}$$\scriptstyle{\kappa_{u}\times\kappa_{u}}$

is a pullback;

  3. 3.

$\kappa_{u}:\mathcal{C}/y\to\mathcal{R}_{\mathcal{C}}$ is a $(-1)$-truncated
map of right fibrations over $\mathcal{C}$. Equivalently, for any object
$z\in\mathcal{C}$, the map $\mathcal{C}(z,y)\to(\mathcal{C}/z)^{\simeq}$
defined by the pullback of $u$ is $(-1)$-truncated.

###### Proof.

The same proof as [19, Proposition 3.8 (1)–(3)] works only assuming the
representability of $\mathrm{Eq}(u)$. ∎

######  Example 5.9.

For any left exact $\infty$-category $\mathcal{C}$, the generic representable
map
$\rho_{\mathcal{C}}:\widetilde{\mathcal{R}}_{\mathcal{C}}\to\mathcal{R}_{\mathcal{C}}$
is a univalent representable map in $\mathbf{RFib}_{\mathcal{C}}$ by
Proposition 5.3.

######  Proposition 5.10.

Let $x$ and $y$ be objects in a left exact $\infty$-category $\mathcal{C}$ and
suppose that $x\times z$ and $y\times z$ are exponentiable in $\mathcal{C}/z$
for any object $z\in\mathcal{C}$.

  1. 1.

The right fibration $\mathrm{Eq}(x,y)\to\mathcal{C}$ is representable.

  2. 2.

Let $\mathcal{D}$ be a left exact $\infty$-category and
$F:\mathcal{C}\to\mathcal{D}$ a left exact functor. If $F$ sends $x\times z$
and $y\times z$ to exponentiable objects over $Fz$ and commutes with
exponentiation by $x\times z$ and $y\times z$ for any $z\in\mathcal{C}$, then
the canonical arrow
$F(\underline{\mathrm{Eq}}(x,y))\to\underline{\mathrm{Eq}}(F(x),F(y))$ is an
equivalence.

###### Proof.

The right fibration $\mathrm{Eq}(x,y)$ is equivalent to the right fibration
$\mathrm{BiInv}(x,y)$ of bi-invertible arrows whose fiber over
$z\in\mathcal{C}$ is the space of tuples $(u,v,\eta,w,\varepsilon)$ consisting
of arrows $u:x\times z\to y\times z$ and $v,w:y\times z\to x\times z$ over $z$
and homotopies $\eta:vu\simeq\mathrm{id}$ and
$\varepsilon:uw\simeq\mathrm{id}$ over $z$. The right fibration
$\mathrm{BiInv}(x,y)$ is representable by the exponentiability of $x\times z$
and $y\times z$. The second assertion is clear from the construction of the
representing object for $\mathrm{BiInv}(x,y)$. ∎

######  Corollary 5.11.

Let $u:x\to y$ be a representable arrow in an $\infty$-category with
representable maps $\mathcal{C}$.

  1. 1.

The right fibration $\mathrm{Eq}(u)\to\mathcal{C}/y\times y$ is representable.

  2. 2.

If $u$ is univalent, so is $Fu$ for any morphism of $\infty$-categories with
representable maps $F:\mathcal{C}\to\mathcal{D}$.

###  5.3 Left exact $\infty$-categories

We define an $\infty$-type theory $\mathbb{E}_{\infty}$ whose theories are
equivalent to small left exact $\infty$-categories.

######  Definition 5.12.

Let $\mathcal{C}$ be an $\infty$-category with representable maps and
$\partial:E\to U$ a representable arrow in $\mathcal{C}$.

  * •

A _$\mathsf{1}$ -type structure on $\partial$_ is a pullback square of the
form

${1}$${E}$${1}$${U.}$$\scriptstyle{*}$$\scriptstyle{\partial}$$\scriptstyle{\mathsf{1}}$
(6)

  * •

A _$\mathsf{\Sigma}$ -type structure on $\partial$_ is a pullback square of
the form

${\mathrm{dom}(\partial\otimes\partial)}$${E}$${\mathrm{cod}(\partial\otimes\partial)}$${U}$$\scriptstyle{\mathsf{p}}$$\scriptstyle{\partial\otimes\partial}$$\scriptstyle{\partial}$$\scriptstyle{\mathsf{\Sigma}}$
(7)

where $\otimes$ is the composition of polynomials (Section 2.4).

  * •

An _$\mathsf{Id}$ -type structure on $\partial$_ is a pullback square of the
form

${E}$${E}$${E\times_{U}E}$${U.}$$\scriptstyle{\mathsf{refl}}$$\scriptstyle{\delta}$$\scriptstyle{\partial}$$\scriptstyle{\mathsf{Id}}$
(8)

######  Proposition 5.13.

Let $\partial:E\to U$ be a univalent representable arrow in an
$\infty$-category with representable maps $\mathcal{C}$. Then
$\mathsf{1}$-type structures, $\mathsf{\Sigma}$-type structures and
$\mathsf{Id}$-type structures are unique up to contractible choice. Moreover,
we have the following:

  1. 1.

$\partial$ has a $\mathsf{1}$-type structure if and only if all the identity
arrows are pullbacks of $\partial$;

  2. 2.

$\partial$ has a $\mathsf{\Sigma}$-type structure if and only if pullbacks of
$\partial$ are closed under composition;

  3. 3.

$\partial$ has an $\mathsf{Id}$-type structure if and only if pullbacks of
$\partial$ are closed under equalizers: if $u:x\to y$ is a pullback of
$\partial$ and $v_{1},v_{2}:x^{\prime}\to x$ are arrows such that
$uv_{1}\simeq uv_{2}$, then the equalizer $x^{\prime\prime}\to x^{\prime}$ of
$v_{1}$ and $v_{2}$ in $\mathcal{C}/y$ is a pullback of $\partial$.

###### Proof.

The uniqueness follows from Item 3 of Proposition 5.8. The rests are
straightforward. ∎

######  Definition 5.14.

By a _left exact universe_ in an $\infty$-category with representable maps
$\mathcal{C}$ we mean a univalent representable arrow $\partial:E\to U$
equipped with a $\mathsf{1}$-type structure, a $\mathsf{\Sigma}$-type
structure and an $\mathsf{Id}$-type structure. We denote by
$\mathbb{E}_{\infty}$ the initial $\infty$-type theory containing a left exact
universe $\partial:E\to U$.

######  Theorem 5.15.

The functor
$\mathrm{ev}_{{\star}}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\to\mathbf{Cat}_{\infty}$
factors through $\mathbf{Lex}_{\infty}$ and induces an equivalence

$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\simeq\mathbf{Lex}_{\infty}.$

######  Lemma 5.16.

An arrow in $\mathbb{E}_{\infty}$ is representable if and only if it is a
pullback of $\partial:E\to U$.

###### Proof.

Let $\mathbb{E}_{\infty}^{\prime}$ denote the $\infty$-category with
representable maps whose underlying $\infty$-category is the same as
$\mathbb{E}_{\infty}$ and representable arrows are the pullbacks of
$\partial$. As $\partial$ is equipped with a $\mathsf{1}$-type structure and a
$\mathsf{\Sigma}$-type structure, the representable arrows in
$\mathbb{E}_{\infty}^{\prime}$ include all the identities and are closed under
composition by Proposition 5.13, so $\mathbb{E}_{\infty}^{\prime}$ is indeed
an $\infty$-category with representable maps. By the initiality of
$\mathbb{E}_{\infty}$, the inclusion
$\mathbb{E}_{\infty}^{\prime}\to\mathbb{E}_{\infty}$ has a section, and thus
$\mathbb{E}_{\infty}^{\prime}\simeq\mathbb{E}_{\infty}$. ∎

######  Definition 5.17.

Let $\mathcal{M}$ be a model of an $\infty$-type theory $\mathbb{T}$. By a
_display map_ we mean an arrow $f:\Delta\to\Gamma$ in $\mathcal{M}({\star})$
that is equivalent over $\Gamma$ to $\mathrm{p}_{u}:\\{b\\}_{u}\to\Gamma$ for
some representable arrow $u:x\to y$ in $\mathbb{T}$ and section
$b:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(y)$. By definition, display maps
are stable under pullbacks.

######  Lemma 5.18.

Let $\mathcal{M}$ be a model of $\mathbb{E}_{\infty}$. An arrow
$f:\Gamma_{1}\to\Gamma_{2}$ in $\mathcal{M}({\star})$ is a display map if and
only if there exists a pullback of the form

${\mathcal{M}({\star})/\Gamma_{1}}$${\mathcal{M}(E)}$${\mathcal{M}({\star})/\Gamma_{2}}$${\mathcal{M}(U).}$$\scriptstyle{f}$$\scriptstyle{\mathcal{M}(\partial)}$

###### Proof.

By Lemma 5.16. ∎

######  Lemma 5.19.

Let $\mathscr{D}$ be a pullback-stable class of arrows in an $\infty$-category
$\mathcal{C}$. Suppose that $\mathscr{D}$ contains all the identity and is
closed under composition and equalizers. Then, for arrows $u:x\to y$ and
$v:y\to z$, if $v$ and $vu$ are in $\mathscr{D}$, so is $u$.

###### Proof.

The assumption implies that the full subcategory of $\mathcal{C}/z$ spanned by
the arrows $x\to z$ in $\mathscr{D}$ is an $\infty$-category of fibrant
objects in which the weak equivalences are the equivalences and the fibrations
are the arrows in $\mathscr{D}$. Therefore, any arrow between fibrations is
equivalent to a fibration. ∎

######  Lemma 5.20.

Let $\mathcal{M}$ be a democratic model of $\mathbb{E}_{\infty}$. Then every
arrow in $\mathcal{M}({\star})$ is a display map.

###### Proof.

By Propositions 5.13, 5.18 and 5.19. ∎

###### Proof of Theorem 5.15.

Since display maps are stable under pullbacks and morphisms of models commute
with pullbacks of display maps, Lemma 5.20 implies that the base
$\infty$-category of a democratic model of $\mathbb{E}_{\infty}$ has all
finite limits and that any morphism between democratic models of
$\mathbb{E}_{\infty}$ commutes with finite limits in the base
$\infty$-categories. In other words, the functor
$\mathrm{ev}_{{\star}}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\to\mathbf{Cat}_{\infty}$
factors through $\mathbf{Lex}_{\infty}$.

Let $\mathcal{C}$ be a left exact $\infty$-category. We define a model
$\mathcal{R}_{\mathcal{C}}$ of $\mathbb{E}_{\infty}$ by setting
$\mathcal{R}_{\mathcal{C}}({\star})$ to be $\mathcal{C}$ and
$\mathcal{R}_{\mathcal{C}}(\partial):\mathcal{R}_{\mathcal{C}}(E)\to\mathcal{R}_{\mathcal{C}}(U)$
to be the generic representable map of right fibrations over $\mathcal{C}$. We
have seen in Example 5.9 that the generic representable map is univalent.
Since $\mathcal{C}$ has finite limits, representable maps of right fibrations
over $\mathcal{C}$ are closed under equalizers. Thus, by Proposition 5.13,
$\mathcal{R}_{\mathcal{C}}$ is indeed a model of $\mathbb{E}_{\infty}$. Since
the construction of the generic representable map for a left exact
$\infty$-category is functorial, the assignment
$\mathcal{C}\mapsto\mathcal{R}_{\mathcal{C}}$ is part of a functor

$\mathcal{R}:\mathbf{Lex}_{\infty}\to\mathbf{Mod}(\mathbb{E}_{\infty}).$

The model $\mathcal{R}_{\mathcal{C}}$ is democratic as the map
$\mathcal{C}/x\to\mathcal{C}/1$ is representable for every object
$x\in\mathcal{C}$.

We show that the functor
$\mathcal{R}:\mathbf{Lex}_{\infty}\to\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})$
is an inverse of
$\mathrm{ev}_{{\star}}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\to\mathbf{Lex}_{\infty}$.
By definition, $\mathrm{ev}_{{\star}}\circ\mathcal{R}\simeq\mathrm{id}$. To
show the other equivalence
$\mathcal{R}\circ\mathrm{ev}_{{\star}}\simeq\mathrm{id}$, let $\mathcal{M}$ be
a democratic model of $\mathbb{E}_{\infty}$. Since
$\mathcal{R}_{\mathcal{M}({\star})}(\partial)$ is the generic representable
map, we have a unique pullback

${\mathcal{M}(E)}$${\mathcal{R}_{\mathcal{M}({\star})}(E)}$${\mathcal{M}(U)}$${\mathcal{R}_{\mathcal{M}({\star})}(U).}$$\scriptstyle{\mathcal{M}(\partial)}$$\scriptstyle{\mathcal{R}_{\mathcal{M}({\star})}(\partial)}$$\scriptstyle{f}$

It suffices to show that $f$ is an equivalence of right fibrations over
$\mathcal{M}({\star})$. Since $\mathcal{M}(\partial)$ is univalent, the map
$f$ is $(-1)$-truncated [19, Corollary 3.10]. Recall that the objects of
$\mathcal{R}_{\mathcal{M}({\star})}(U)$ are the arrows of
$\mathcal{M}({\star})$. Lemma 5.18 implies that the essential image of $f$ is
the class of display maps in $\mathcal{M}({\star})$. Then, by Lemma 5.20, the
map $f$ is essentially surjective and thus an equivalence. ∎

Consider the image of the arrow $\partial:E\to U$ by the inclusion
$\mathbb{E}_{\infty}\to\mathbf{Th}(\mathbb{E}_{\infty})^{\mathrm{op}}\simeq\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})^{\mathrm{op}}\simeq\mathbf{Lex}_{\infty}^{\mathrm{op}}$.
For a left exact $\infty$-category $\mathcal{C}$, we have

$\displaystyle\mathbf{Th}(\mathbb{E}_{\infty})(\mathbf{y}(U),\mathrm{L}(\mathcal{R}_{\mathcal{C}}))\simeq\mathcal{R}_{\mathcal{C}}(U)_{1}\simeq\mathcal{C}^{\simeq}$
$\displaystyle\mathbf{Th}(\mathbb{E}_{\infty})(\mathbf{y}(E),\mathrm{L}(\mathcal{R}_{\mathcal{C}}))\simeq\mathcal{R}_{\mathcal{C}}(E)_{1}\simeq(1/\mathcal{C})^{\simeq}.$

Hence, the object $U$ corresponds to the free left exact $\infty$-category
$\langle\Box\rangle$ generated by an object $\Box$, the object $E$ corresponds
to the free left exact $\infty$-category
$\langle\widetilde{\Box}:1\to\Box\rangle$ generated by an object $\Box$ and a
global section $\widetilde{\Box}:1\to\Box$, and the arrow $\partial:E\to U$
corresponds to the inclusion
$\iota:\langle\Box\rangle\to\langle\widetilde{\Box}:1\to\Box\rangle$. Since
$\mathbf{y}(x)/\mathbf{Th}(\mathbb{E}_{\infty})\simeq\mathbf{Th}(\mathbb{E}_{\infty}/x)$,
we see that the inclusion $\iota$ becomes an exponentiable arrow in
$\mathbf{Lex}_{\infty}^{\mathrm{op}}$. This makes
$\mathbf{Lex}_{\infty}^{\mathrm{op}}$ an $\infty$-category with representable
maps in which the representable arrows are the pullbacks of $\iota$, and
$\iota$ is a left exact universe in $\mathbf{Lex}_{\infty}^{\mathrm{op}}$.
Since $\mathbf{Th}(\mathbb{E}_{\infty})$ is the $\omega$-free cocompletion of
$\mathbb{E}_{\infty}^{\mathrm{op}}$, the universal property of
$\mathbb{E}_{\infty}$ gives the following universal property of
$\mathbf{Lex}_{\infty}$.

######  Corollary 5.21.

Let $\mathcal{C}$ be an $\infty$-category with representable maps that has all
small limits and $u:x\to y$ a left exact universe in $\mathcal{C}$. Then there
exists a unique morphism of $\infty$-categories with representable maps
$F:\mathbf{Lex}_{\infty}^{\mathrm{op}}\to\mathcal{C}$ that sends $\iota$ to
$u$ and preserves small limits.

###### Proof.

By the definition of $\mathbb{E}_{\infty}$, we have a unique morphism of
$\infty$-categories with representable maps
$\overline{F}:\mathbb{E}_{\infty}\to\mathcal{C}$ that sends $\partial$ to $u$,
which uniquely extends to a limit-preserving functor
$F:\mathbf{Lex}_{\infty}^{\mathrm{op}}\simeq\mathbf{Th}(\mathbb{E}_{\infty})^{\mathrm{op}}\to\mathcal{C}$.
The functor $F$ sends pushforwards along $\iota$ to pushforwards along $u$
because the pushforward functors preserve limits and every object of
$\mathbf{Th}(\mathbb{E}_{\infty})^{\mathrm{op}}$ is a limit of objects from
$\mathbb{E}_{\infty}$. ∎

###  5.4 Locally cartesian closed $\infty$-categories

We define an $\infty$-type theory $\mathbb{E}_{\infty}^{\mathsf{\Pi}}$ whose
theories are equivalent to small locally cartesian closed $\infty$-categories.

######  Definition 5.22.

Let $\mathcal{C}$ be an $\infty$-category with representable maps and
$\partial:E\to U$ a representable arrow in $\mathcal{C}$. A _$\mathsf{\Pi}$
-type structure on $\partial$_ is a pullback square of the form

${\mathbf{P}_{\partial}E}$${E}$${\mathbf{P}_{\partial}U}$${U.}$$\scriptstyle{\mathsf{\lambda}}$$\scriptstyle{\mathbf{P}_{\partial}\partial}$$\scriptstyle{\partial}$$\scriptstyle{\mathsf{\Pi}}$
(9)

The following is straightforward.

######  Proposition 5.23.

Let $\partial:E\to U$ be a univalent representable arrow in an
$\infty$-category with representable maps. Then $\mathsf{\Pi}$-type structures
on $\partial$ are unique up to contractible choice. Moreover, there exists a
$\mathsf{\Pi}$-type structure on $\partial$ if and only if pullbacks of
$\partial$ are closed under pushforwards along pullbacks of $\partial$.

######  Definition 5.24.

Let $\mathbb{E}_{\infty}^{\mathsf{\Pi}}$ denote the initial $\infty$-type
theory containing a left exact universe $\partial:E\to U$ with a
$\mathsf{\Pi}$-type structure.

######  Theorem 5.25.

The functor
$\mathrm{ev}_{{\star}}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})\to\mathbf{Cat}_{\infty}$
factors through the $\infty$-category $\mathbf{LCCC}_{\infty}$ of small
locally cartesian closed $\infty$-categories and induces an equivalence

$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})\simeq\mathbf{LCCC}_{\infty}.$

###### Proof.

Lemma 5.16 holds for $\mathbb{E}_{\infty}^{\mathsf{\Pi}}$: an arrow in
$\mathbb{E}_{\infty}^{\mathsf{\Pi}}$ is representable if and only if it is a
pullback of $\partial$. It follows from this that the restriction of a
democratic model of $\mathbb{E}_{\infty}^{\mathsf{\Pi}}$ along the inclusion
$\mathbb{E}_{\infty}\to\mathbb{E}_{\infty}^{\mathsf{\Pi}}$ is a democratic
model of $\mathbb{E}_{\infty}$. Thus, by Theorem 5.15, it suffices to show
that the composite
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})\to\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\overset{\mathrm{ev}_{{\star}}}{\longrightarrow}\mathbf{Lex}_{\infty}$
factors through $\mathbf{LCCC}_{\infty}$ and gives rise a pullback square

${\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})}$${\mathbf{LCCC}_{\infty}}$${\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})}$${\mathbf{Lex}_{\infty}.}$$\scriptstyle{\mathrm{ev}_{{\star}}}$$\scriptstyle{\simeq}$

It suffices to show the following:

  1. 1.

an object $\mathcal{M}$ in $\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})$
is in $\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$ if and
only if $\mathcal{M}({\star})$ is in $\mathbf{LCCC}_{\infty}$;

  2. 2.

for objects
$\mathcal{M},\mathcal{N}\in\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$,
a morphism $F:\mathcal{M}\to\mathcal{N}$ in
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})$ is in
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$ if and only
if $F({\star}):\mathcal{M}({\star})\to\mathcal{N}({\star})$ is in
$\mathbf{LCCC}_{\infty}$.

Item 1. By Proposition 5.23, an object
$\mathcal{M}\in\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})$ is in
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$ if and only
if representable maps of right fibrations over $\mathcal{M}({\star})$ are
closed under pushforwards along representable maps. This is equivalent to that
the $\infty$-category $\mathcal{M}({\star})$ is locally cartesian closed.

Item 2. A morphism $F:\mathcal{M}\to\mathcal{N}$ in
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})$ between objects from
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$ is in
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$ if and only
if it commutes with $\mathsf{\Pi}$-type structures. Observe that
$\mathcal{M}(\mathsf{\Pi}):\mathcal{M}(\mathbf{P}_{\partial}U)\to\mathcal{M}(U)$
sends a pair of composable arrows $u:x\to y$ and $v:y\to z$ in
$\mathcal{M}({\star})$ to the pushforward $v_{*}u:v_{*}x\to z$. Thus, $F$
commutes with $\mathsf{\Pi}$-type structures if and only if
$F({\star}):\mathcal{M}({\star})\to\mathcal{N}({\star})$ commutes with
pushforwards. ∎

###  5.5 $\infty$-type theories

We define an $\infty$-type theory $\mathbb{R}_{\infty}$ whose theories are
equivalent to $\infty$-type theories.

######  Definition 5.26.

Let $\partial_{1}:E_{1}\to U_{1}$, $\partial_{2}:E_{2}\to U_{2}$ and
$\partial_{3}:E_{3}\to U_{3}$ be representable arrows in an $\infty$-category
with representable maps. A _$(\partial_{1},\partial_{2},\partial_{3})$
-$\mathsf{\Pi}$-type structure_ is a pullback of the form

${\mathbf{P}_{\partial_{1}}E_{2}}$${E_{3}}$${\mathbf{P}_{\partial_{1}}U_{2}}$${U_{3}.}$$\scriptstyle{\mathsf{\lambda}}$$\scriptstyle{\mathbf{P}_{\partial_{1}}\partial_{2}}$$\scriptstyle{\partial_{3}}$$\scriptstyle{\mathsf{\Pi}}$
(10)

Note that if $\partial_{3}$ is univalent, then
$(\partial_{1},\partial_{2},\partial_{3})$-$\mathsf{\Pi}$-type structure are
unique up to contractible choice, and there exists a
$(\partial_{1},\partial_{2},\partial_{3})$-$\mathsf{\Pi}$-type structure if
and only if the pushforward of a pullback of $\partial_{2}$ along a pullback
of $\partial_{1}$ is a pullback of $\partial_{3}$.

######  Definition 5.27.

We denote by $\mathbb{R}_{\infty}$ the initial $\infty$-type theory containing
the following data:

  * •

a left exact universe $\partial:E\to U$;

  * •

a $(-1)$-truncated arrow $R\hookrightarrow U$. We denote by $\partial_{R}$ the
pullback of $\partial$ along the inclusion $R\hookrightarrow U$;

  * •

a $\mathsf{1}$-type structure and a $\mathsf{\Sigma}$-type structure on
$\partial_{R}$;

  * •

a $(\partial_{R},\partial,\partial)$-$\mathsf{\Pi}$-type structure.

Note that the inclusion $R\hookrightarrow U$ automatically commutes with
$\mathsf{1}$-type structures and $\mathsf{\Sigma}$-type structures because of
univalence.

######  Definition 5.28.

Let $\mathcal{M}$ be a model of $\mathbb{R}_{\infty}$. We say an arrow in
$\mathcal{M}({\star})$ is _representable_ if it is a context comprehension
with respect to $\partial_{R}$. Using the
$(\partial_{R},\partial,\partial)$-$\mathsf{\Pi}$-type structure, we see that
the pushforward of a display map along a representable map exists and is a
display map. In particular, if $\mathcal{M}$ is democratic, then
$\mathcal{M}({\star})$ is an $\infty$-type theory and, for any morphism
$F:\mathcal{M}\to\mathcal{N}$ between democratic models,
$F({\star}):\mathcal{M}({\star})\to\mathcal{N}({\star})$ is a morphism of
$\infty$-type theories. Hence, we have a functor

$\mathrm{ev}_{{\star}}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{R}_{\infty})\to\mathbf{TT}_{\infty}$

######  Theorem 5.29.

The functor
$\mathrm{ev}_{{\star}}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{R}_{\infty})\to\mathbf{TT}_{\infty}$
is an equivalence.

###### Proof.

Similar to Theorem 5.15. For an $\infty$-type theory $\mathcal{C}$, the
representable map classifier $\mathcal{R}_{\mathcal{C}}(U)$ has the full
subfibration $\mathcal{R}_{\mathcal{C}}(R)\subset\mathcal{R}_{\mathcal{C}}(U)$
spanned by the representable arrows in $\mathcal{C}$, which defines a
democratic model of $\mathbb{R}_{\infty}$. ∎

##  6 Internal languages for left exact $\infty$-categories

In this section, we show [27]’s conjecture that the $\infty$-category of small
left exact $\infty$-categories is a localization of the category of theories
over Martin-Löf type theory with intensional identity types [27].

We first introduce a structure of _intensional identity types_ in the context
of $\infty$-type theory.

######  Definition 6.1.

Let $\mathcal{C}$ be an $\infty$-category with representable maps and
$\partial:E\to U$ a representable arrow in $\mathcal{C}$. An
_$\mathsf{Id}^{+}$ -type structure on $\partial$_ is a commutative square of
the form

${E}$${E}$${E\times_{U}E}$${U}$$\scriptstyle{\mathsf{refl}}$$\scriptstyle{\delta}$$\scriptstyle{\partial}$$\scriptstyle{\mathsf{Id}}$
(11)

equipped with a section $\mathsf{elim}_{\mathsf{Id}^{+}}$ of the induced arrow

$(\mathsf{refl}^{*},\partial_{*}):(\mathsf{Id}^{*}E\Rightarrow_{U}U^{*}E)\to(E\Rightarrow_{U}U^{*}E)\times_{(E\Rightarrow_{U}U^{*}U)}(\mathsf{Id}^{*}E\Rightarrow_{U}U^{*}U),$

where $\Rightarrow_{U}$ is the exponential in the slice $\mathcal{C}/U$.

The codomain of the arrow $(\mathsf{refl}^{*},\partial_{*})$ classifies
_lifting problems_ for $\mathsf{refl}$ against $\partial$, and the section
$\mathsf{elim}_{\mathsf{Id}^{+}}$ is considered as a _uniform solution_ to the
lifting problems. See [6, 5, 28] for how this definition is related to
syntactically presented intensional identity types. We note that for an
$\mathsf{Id}$-type structure $(\mathsf{Id},\mathsf{refl})$, the arrow
$(\mathsf{refl}^{*},\partial_{*})$ is invertible, and thus any
$\mathsf{Id}$-type structure is uniquely extended to an $\mathsf{Id}^{+}$-type
structure.

Let $\mathbb{I}$ denote the $1$-type theory freely generated by a
representable arrow $\partial:E\to U$ equipped with a $\mathsf{1}$-type
structure, a $\mathsf{\Sigma}$-type structure, and an $\mathsf{Id}^{+}$-type
structure. [27] conjectured that the $\infty$-category $\mathbf{Lex}_{\infty}$
is a localization of the $1$-category $\mathbf{Th}(\mathbb{I})$. Strictly,
they work with contextual categories with a unit type,
$\mathsf{\Sigma}$-types, and intensional identity types instead of theories
over $\mathbb{I}$ in our sense, but it is straightforward to see that those
contextual categories are equivalent to democratic models of $\mathbb{I}$.
They also gave a specific functor
$\mathbf{Th}(\mathbb{I})\to\mathbf{Lex}_{\infty}$ and conjectured that it is a
localization functor. We prove their conjecture using the theory of
$\infty$-type theories and the equivalence
$\mathbf{Th}(\mathbb{E}_{\infty})\simeq\mathbf{Lex}_{\infty}$.

We construct the functor
$\mathbf{Th}(\mathbb{I})\to\mathbf{Lex}_{\infty}\simeq\mathbf{Th}(\mathbb{E}_{\infty})$
differently from [27]. A first attempt is to construct a morphism between
$\mathbb{I}$ and $\mathbb{E}_{\infty}$, but this fails: since the generating
representable arrow $\partial$ is not univalent in $\mathbb{I}$, we do not
have a morphism $\mathbb{E}_{\infty}\to\mathbb{I}$; since $\partial$ is not
$0$-truncated in $\mathbb{E}_{\infty}$, we do not have a morphism
$\mathbb{I}\to\mathbb{E}_{\infty}$. We thus introduce an intermediate
$\infty$-type theory $\mathbb{I}_{\infty}$ defined as the free $\infty$-type
theory generated by the same data as $\mathbb{I}$ but without truncatedness.
Then $\mathbb{I}$ is the universal $1$-type theory under
$\mathbb{I}_{\infty}$, and $\mathbb{E}_{\infty}$ is the universal
$\infty$-type theory under $\mathbb{I}_{\infty}$ inverting the morphisms
$\mathsf{refl}:E\to\mathsf{Id}^{*}E$ and
$|\mathrm{id}|:U\to\underline{\mathrm{Eq}}(\partial)$. We thus have a span of
$\infty$-type theories

${\mathbb{I}}$${\mathbb{I}_{\infty}}$${\mathbb{E}_{\infty}.}$$\scriptstyle{\tau}$$\scriptstyle{\gamma}$
(12)

Since any morphism $F:\mathbb{T}\to\mathbb{T}^{\prime}$ between $\infty$-type
theories induces an adjunction $F_{!}\dashv
F^{*}:\mathbf{Th}(\mathbb{T})\to\mathbf{Th}(\mathbb{T}^{\prime})$ as
$\mathbf{Th}(\mathbb{T})=\mathbf{Lex}(\mathbb{T},\mathbf{S})$, we have a
functor

${\mathbf{Th}(\mathbb{I})}$${\mathbf{Th}(\mathbb{I}_{\infty})}$${\mathbf{Th}(\mathbb{E}_{\infty}).}$$\scriptstyle{\tau^{*}}$$\scriptstyle{\gamma_{!}}$
(13)

We define the _weak equivalences_ in $\mathbf{Th}(\mathbb{I})$ to be the
morphisms inverted by the functor $\gamma_{!}\tau^{*}$ and write
$L(\mathbf{Th}(\mathbb{I}))$ for the localization by the weak equivalences.

######  Theorem 6.2.

The functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{E}_{\infty})$
induces an equivalence of $\infty$-categories

$L(\mathbf{Th}(\mathbb{I}))\simeq\mathbf{Th}(\mathbb{E}_{\infty}).$

Moreover, the composite
${\mathbf{Th}(\mathbb{I})}$${\mathbf{Th}(\mathbb{E}_{\infty})}$${\mathbf{Lex}_{\infty}}$$\scriptstyle{\gamma_{!}\tau^{*}}$$\scriptstyle{\simeq}$
coincides with the functor considered by [27, Conjecture 3.7].

######  Remark 6.3.

The construction of the functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{E}_{\infty})$
is easily generalized to extensions with type-theoretic structures such as
$\mathsf{\Pi}$-types, (higher) inductive types, and universes. For example, if
we extend $\mathbb{I}$ with $\mathsf{\Pi}$-types, then we have a span

${\mathbb{I}^{\mathsf{\Pi}}}$${\mathbb{I}_{\infty}^{\mathsf{\Pi}}}$${\mathbb{E}_{\infty}^{\mathsf{\Pi}}}$$\scriptstyle{\tau}$$\scriptstyle{\gamma}$

by extending $\mathbb{I}_{\infty}$ with $\mathsf{\Pi}$-types. We expect that
similar results to Theorem 6.2 can be proved for a wide range of extensions of
$\mathbb{I}$, which is left as future work. See Section 6.2 for discussion.

###  6.1 Proof of the theorem

This subsection is devoted to the proof of Theorem 6.2. We use [12]’s results
on localizations of $\infty$-categories [12, Chapter 7]. We first give the
category $\mathbf{Th}(\mathbb{I})$ the structure of a _category with weak
equivalences and cofibrations_ (we recall the definition below) and show that
the functor $\gamma_{!}\tau^{*}$ is _right exact_. We then show that the
functor $\gamma_{!}\tau^{*}$ satisfies the _left approximation property_ (also
recalled below), which implies that the induced functor on localization is an
equivalence.

######  Definition 6.4.

A _category with weak equivalences and cofibrations_ is a category
$\mathcal{C}$ equipped with two classes of arrows called _weak equivalences_
and _cofibrations_ satisfying the conditions below. An object
$x\in\mathcal{C}$ is _cofibrant_ if the arrow $0\to x$ is a cofibration. An
arrow is a _trivial cofibration_ if it is both a weak equivalence and a
cofibration.

  1. 1.

$\mathcal{C}$ has an initial object.

  2. 2.

All the identities are trivial cofibrations, and weak equivalences and
cofibrations are closed under composition.

  3. 3.

The weak equivalences satisfy the _2-out-of-3_ property: if $u$ and $v$ are a
composable pair of arrows and if two of $u$, $v$, and $vu$ are weak
equivalences, then so is the rest.

  4. 4.

(Trivial) cofibrations are stable under pushouts along arbitrary arrows
between cofibrant objects: if $x,x^{\prime}\in\mathcal{C}$ are cofibrant
objects, $i:x\to y$ is a (trivial) cofibration, and $u:x\to x^{\prime}$ is an
arbitrary arrow, then the pushout $u_{!}y$ exists and the arrow $x^{\prime}\to
u_{!}y$ is a (trivial) cofibration.

  5. 5.

Any arrow $u:x\to y$ with cofibrant domain factors into a cofibration $x\to
y^{\prime}$ followed by a weak equivalence $y^{\prime}\to y$.

######  Definition 6.5.

Let $\mathcal{C}$ be a category with weak equivalences and cofibrations and
$\mathcal{D}$ an $\infty$-category with finite colimits. A functor
$F:\mathcal{C}\to\mathcal{D}$ is _right exact_ if it sends trivial
cofibrations between cofibrant objects to invertible arrows and preserves
initial objects and pushouts of cofibrations along arrows between cofibrant
objects. A right exact functor $F:\mathcal{C}\to\mathcal{D}$ has the _left
approximation property_ if the following conditions hold:

  1. 1.

an arrow in $\mathcal{C}$ is a weak equivalence if and only if it becomes
invertible in $\mathcal{D}$;

  2. 2.

for any cofibrant object $x\in\mathcal{C}$ and any arrow $u:F(x)\to y$ in
$\mathcal{D}$, there exists an arrow $u^{\prime}:x\to y^{\prime}$ in
$\mathcal{C}$ such that $F(y^{\prime})\simeq y$ under $F(x)$.

######  Proposition 6.6.

Any right exact functor $F:\mathcal{C}\to\mathcal{D}$ with the left
approximation property induces an equivalence
$L(\mathcal{C})\simeq\mathcal{D}$.

###### Proof.

By [12, Proposition 7.6.15]. ∎

Our first task will be to show that $\mathbf{Th}(\mathbb{I})$ admits the
structure of a category with weak equivalences and cofibrations. We have
already defined the weak equivalences in $\mathbf{Th}(\mathbb{I})$ as those
morphisms inverted by $\gamma_{!}\tau^{*}$. We define the cofibrations in
$\mathbf{Th}(\mathbb{I})$ as follows. Recall that
$\mathbf{y}:\mathbb{I}^{\mathrm{op}}\to\mathbf{Th}(\mathbb{I})$ is the Yoneda
embedding and $\mathbf{P}_{\partial}:\mathbb{I}\to\mathbb{I}$ is the
polynomial functor associated with $\partial:E\to U$.

######  Definition 6.7.

The _generating cofibrations in $\mathbf{Th}(\mathbb{I})$_ are the following
morphisms:

  * •

$\mathbf{y}(\mathbf{P}_{\partial}^{n}(1))\to\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))$
for $n\geq 0$;

  * •

$\mathbf{y}(\mathbf{P}_{\partial}^{n}(\partial)):\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))\to\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))$
for $n\geq 0$.

The class of _cofibrations in $\mathbf{Th}(\mathbb{I})$_ is the closure of the
generating cofibrations under retracts, pushouts along arbitrary morphisms,
and transfinite composition. Cofibrations in
$\mathbf{Th}(\mathbb{I}_{\infty})$ and $\mathbf{Th}(\mathbb{E}_{\infty})$ are
defined in the same way. Note that the functors $\tau_{!}$ and $\gamma_{!}$
preserve generating cofibrations.

######  Remark 6.8.

Our choice of generating cofibrations in $\mathbf{Th}(\mathbb{I})$ coincides
with the choice by [27]. That is, $\mathbf{y}(\mathbf{P}_{\partial}^{n}(1))$
is the theory freely generated by a context of length $n$,
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))$ is the theory freely generated by a
type over a context of length $n$, and
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))$ is the theory freely generated by a
term over a context of length $n$. This is verified as follows. Let $K$ be an
$\mathbb{I}$-theory and let $\mathcal{M}$ be the democratic model of
$\mathbb{I}$ corresponding to $K$ via the equivalence
$\mathbf{Th}(\mathbb{I})\simeq\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})$. By
construction, a morphism $\mathbf{y}x\to K$ correspond to a global section
$\mathcal{M}({\star})\to\mathcal{M}(x)$ for any object $x\in\mathbb{I}$. Then,
by the universal property of $\mathbf{P}_{\partial}$, a morphism
$\Gamma:\mathbf{y}(\mathbf{P}_{\partial}^{n}(1))\to K$ corresponds to a list
of sections

$\begin{split}\Gamma_{1}&:\mathcal{M}({\star})/\\{\Gamma_{0}\\}\to\mathcal{M}(U)\\\
\Gamma_{2}&:\mathcal{M}({\star})/\\{\Gamma_{1}\\}\to\mathcal{M}(U)\\\
\vdots\\\
\Gamma_{n}&:\mathcal{M}({\star})/\\{\Gamma_{n-1}\\}\to\mathcal{M}(U)\end{split}$
(14)

where $\\{\Gamma_{0}\\}=1$ and
$\mathcal{M}({\star})/\\{\Gamma_{i+1}\\}\simeq\Gamma_{i}^{*}\mathcal{M}(E)$.
Since we think of sections of $\mathcal{M}(U)$ as types, such a list of
sections can be regarded as a context of length $n$. Under this
identification, an extension $\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))\to K$
of $\Gamma$ corresponds to a section
$\mathcal{M}({\star})/\\{\Gamma_{n}\\}\to\mathcal{M}(U)$, that is, a type over
$\Gamma$. Similarly, an extension $\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))\to
K$ of $\Gamma$ corresponds to a term
$\mathcal{M}({\star})/\\{\Gamma_{n}\\}\to\mathcal{M}(E)$, that is, a term over
$\Gamma$. Hence, morphisms from $\mathbf{y}(\mathbf{P}_{\partial}^{n}(1))$,
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))$, and
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))$ correspond to contexts, types, and
terms, respectively. In this view, a cofibration in $\mathbf{Th}(\mathbb{I})$
is an extension by types and terms, but without any equation. In particular,
cofibrant $\mathbb{I}$-theories are those freely generated by types and terms.

######  Theorem 6.9.

The classes of cofibrations and weak equivalences endow
$\mathbf{Th}(\mathbb{I})$ with the structure of a category with weak
equivalences and cofibrations.

By definition, $\mathbf{Th}(\mathbb{I})$ satisfies Items 1, 2 and 3 of
Definition 6.4, and cofibrations are stable under arbitrary pushouts. To make
$\mathbf{Th}(\mathbb{I})$ a category with weak equivalences and cofibrations,
it remains to verify the stability of trivial cofibrations under pushouts and
the factorization axiom. The former is true if the functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{E}_{\infty})$
preserves initial objects and pushouts of cofibrations along morphisms between
cofibrant objects. Note that this also implies that the functor
$\gamma_{!}\tau^{*}$ must be right exact. Since $\gamma_{!}$ preserves all
colimits, it suffices to show that $\tau^{*}$ has this property. For the
latter, we introduce the notion of _trivial fibration_.

######  Definition 6.10.

A morphism $f:K\to L$ in $\mathbf{Th}(\mathbb{I})$ is a _trivial fibration_ if
it has the right lifting property against cofibrations: for any commutative
square

${A}$${K}$${B}$${L}$$\scriptstyle{g}$$\scriptstyle{i}$$\scriptstyle{f}$$\scriptstyle{h}$

in which $i$ is a cofibration, there exists a morphism $k:B\to K$ such that
$fk=h$ and $ki=g$. Trivial fibrations in $\mathbf{Th}(\mathbb{I}_{\infty})$
and $\mathbf{Th}(\mathbb{E}_{\infty})$ are defined in the same way. By a
standard argument in model category theory, $f$ is a trivial fibration if and
only if it has the right lifting property against generating cofibrations.

By the _small object argument_ , we know that any morphism in
$\mathbf{Th}(\mathbb{I})$ factors into a cofibration followed by a trivial
fibration. Thus, to show that $\mathbf{Th}(\mathbb{I})$ satisfies the
factorization axiom it is enough to show that trivial fibrations are inverted
by $\gamma_{!}\tau^{*}$. In conclusion, theorem 6.9 will follow from the
following two propositions.

######  Proposition 6.11.

The functor
$\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{I}_{\infty})$
preserves initial objects and pushouts of cofibrations along morphisms between
cofibrant objects.

######  Proposition 6.12.

Trivial fibrations in $\mathbf{Th}(\mathbb{I})$ are inverted by the functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{E}_{\infty})$.

We begin by proving Proposition 6.12. It can be broken into the following two
lemmas.

######  Lemma 6.13.

In $\mathbf{Th}(\mathbb{E}_{\infty})$, the trivial fibrations are precisely
the invertible morphisms. Equivalently, all the morphisms are cofibrations.

######  Lemma 6.14.

For any $\mathbb{I}$-theory $K$, the unit
$\tau^{*}K\to\gamma^{*}\gamma_{!}\tau^{*}K$ is a trivial fibration.

###### Proof of Proposition 6.12.

Let $f:K\to L$ be a trivial fibration in $\mathbf{Th}(\mathbb{I})$. Consider
the naturality square

${\tau^{*}K}$${\gamma^{*}\gamma_{!}\tau^{*}K}$${\tau^{*}L}$${\gamma^{*}\gamma_{!}\tau^{*}L}$$\scriptstyle{\eta_{\tau^{*}K}}$$\scriptstyle{\tau^{*}f}$$\scriptstyle{\gamma^{*}\gamma_{!}\tau^{*}f}$$\scriptstyle{\eta_{\tau^{*}L}}$

where $\eta$ is the unit of the adjunction $\gamma_{!}\dashv\gamma^{*}$. By an
adjoint argument, $\tau^{*}f$ is a trivial fibration. By Lemma 6.14,
$\eta_{\tau^{*}K}$ and $\eta_{\tau^{*}L}$ are trivial fibrations. Since the
domains of the generating cofibrations are cofibrant, it follows that
$\gamma^{*}\gamma_{!}\tau^{*}f$ is a trivial fibration. Then, again by an
adjoint argument, $\gamma_{!}\tau^{*}f$ is a trivial fibration and thus
invertible by Lemma 6.13. ∎

Lemma 6.13 is straightforward.

###### Proof of Lemma 6.13.

Since the representable arrow $\partial$ in $\mathbb{E}_{\infty}$ has an
$\mathsf{Id}$-type structure, the diagonal $E\to E\times_{U}E$ is a pullback
of $\partial$. This implies that the codiagonal
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(E\times_{U}E))\to\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))$
in $\mathbf{Th}(\mathbb{E}_{\infty})$ is a cofibration for $n\geq 0$.
Similarly, the univalence of $\partial$ implies that the codiagonal
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(U\times
U))\to\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))$ in
$\mathbf{Th}(\mathbb{E}_{\infty})$ is a cofibration for $n\geq 0$. Hence, for
any generating cofibration $i:A\to B$ in $\mathbf{Th}(\mathbb{E}_{\infty})$,
the codiagonal $B+_{A}B\to B$ is a cofibration, and thus cofibrations in
$\mathbf{Th}(\mathbb{E}_{\infty})$ are closed under codiagonal. It then
follows that cofibrations in $\mathbf{Th}(\mathbb{E}_{\infty})$ has the right
cancellation property: for a composable pair of morphisms $f$ and $g$, if $f$
and $gf$ are cofibrations, then so is $g$. Therefore, it suffices to show that
all the objects of $\mathbf{Th}(\mathbb{E}_{\infty})$ are cofibrant. One can
show that $\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))$’s and
$\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))$’s generate
$\mathbf{Th}(\mathbb{E}_{\infty})$ under colimits. Since they are cofibrant,
all the objects are cofibrant. ∎

For Propositions 6.11 and 6.14, we need analysis of the functors $\tau^{*}$
and $\gamma_{!}$. We work with democratic models instead of theories via the
equivalence
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\simeq\mathbf{Th}(\mathbb{T})$
(Theorem 4.14). We first note that the functors
$\tau^{*}:\mathbf{Mod}(\mathbb{I})\to\mathbf{Mod}(\mathbb{I}_{\infty})$ and
$\gamma^{*}:\mathbf{Mod}(\mathbb{E}_{\infty})\to\mathbf{Mod}(\mathbb{I}_{\infty})$
are fully faithful. More precisely, the models of $\mathbb{I}$ are the models
$\mathcal{M}$ of $\mathbb{I}_{\infty}$ such that $\mathcal{M}(U)$ and
$\mathcal{M}(E)$ are $0$-truncated objects in
$\mathbf{RFib}_{\mathcal{M}({\star})}$, and the models of
$\mathbb{E}_{\infty}$ are the models $\mathcal{M}$ of $\mathbb{I}_{\infty}$
such that the map
$\mathcal{M}(\mathsf{refl}):\mathcal{M}(E)\to\mathcal{M}(\mathsf{Id}^{*}E)$ is
invertible and the representable map $\mathcal{M}(\partial)$ is a univalent.
It is also clear from this description that the functors $\tau^{*}$ and
$\gamma^{*}$ preserve democratic models. Hence, we may identify the functors
$\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{I}_{\infty})$ and
$\gamma^{*}:\mathbf{Th}(\mathbb{E}_{\infty})\to\mathbf{Th}(\mathbb{I}_{\infty})$
with the inclusions
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})\subset\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})$
and
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\subset\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})$,
respectively.

To prove Lemma 6.14, we concretely describe
$\gamma_{!}\mathcal{M}\in\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})$ for
a democratic model $\mathcal{M}$ of $\mathbb{I}$. By a standard argument in
the categorical semantics of homotopy type theory [[, e.g.]Theorem
3.2.5]avigad2015homotopy, the base category $\mathcal{M}({\star})$ is a
category of fibrant objects whose fibrations are the display maps and whose
weak equivalences are homotopy equivalences defined by the identity types. By
the result of [44], the localization $L(\mathcal{M}({\star}))$ has finite
limits, and the localization functor $\mathcal{M}({\star})\to
L(\mathcal{M}({\star}))$ is left exact. The construction $\mathcal{M}\mapsto
L(\mathcal{M}({\star}))$ is the one considered by [27, Conjecture 3.7], and
thus the following lemma implies the second assertion of Theorem 6.2.

######  Lemma 6.15.

The functor

$\gamma_{!}:\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})\subset\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})\to\mathbf{Mod}^{\mathrm{dem}}(\mathbb{E}_{\infty})\simeq\mathbf{Lex}_{\infty}$

is naturally equivalent to the functor $\mathcal{M}\mapsto
L(\mathcal{M}({\star}))$.

###### Proof.

Let $\mathcal{C}$ be a left exact $\infty$-category and let
$\mathcal{R}_{\mathcal{C}}$ be the corresponding democratic model of
$\mathbb{E}_{\infty}$. We construct an equivalence of spaces

$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})(\mathcal{M},\mathcal{R}_{\mathcal{C}})\simeq\mathbf{Lex}_{\infty}(\mathcal{M}({\star}),\mathcal{C}).$
(15)

Then we see that $\gamma_{!}\mathcal{M}$ and $L(\mathcal{M}({\star}))$ has the
same universal property. Given a morphism
$F:\mathcal{M}\to\mathcal{R}_{\mathcal{C}}$ of models of
$\mathbb{I}_{\infty}$, since the weak equivalences in $\mathcal{M}({\star})$
is defined by the intensional identity types, and since the intensional
identity types become extensional one in $\mathcal{C}$, the underlying functor
$F_{{\star}}:\mathcal{M}({\star})\to\mathcal{C}$ is left exact. This defines
one direction of Eq. 15. For the other, let
$F_{{\star}}:\mathcal{M}({\star})\to\mathcal{C}$ be a left exact functor.
Recall that $\mathcal{R}_{\mathcal{C}}(U)$ is the right fibration of arrows in
$\mathcal{C}$ and that $\mathcal{R}_{\mathcal{C}}(E)$ is the right fibration
of sections in $\mathcal{C}$. Then we can construct maps
$F_{U}:\mathcal{M}(U)\to\mathcal{R}_{\mathcal{C}}(U)$ and
$F_{E}:\mathcal{M}(E)\to\mathcal{R}_{\mathcal{C}}(E)$ of right fibrations over
$F_{{\star}}$ by context comprehension followed by $F_{{\star}}$. It is
straightforward to see that these define a morphism
$\mathcal{M}\to\mathcal{R}_{\mathcal{C}}$ of democratic models of
$\mathbb{I}_{\infty}$. The two constructions are mutually inverses. ∎

We characterize trivial fibrations of democratic models of
$\mathbb{I}_{\infty}$ in the same way as [27].

######  Lemma 6.16.

A morphism $F:\mathcal{M}\to\mathcal{N}$ in
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})$ is a trivial fibration if
and only if the following conditions are satisfied:

Type lifting

for any object $\Gamma\in\mathcal{M}({\star})$ and any section
$A:\mathcal{N}({\star})/F(\Gamma)\to\mathcal{N}(U)$, there exists a section
$A^{\prime}:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(U)$ such that
$F(A^{\prime})\simeq A$;

Term lifting

for any object $\Gamma\in\mathcal{M}({\star})$, any section
$A:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(U)$, and any section
$a:\mathcal{N}({\star})/F(\Gamma)\to\mathcal{N}(E)$ over $F(A)$, there exists
a section $a^{\prime}:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(E)$ over $A$
such that $F(a^{\prime})\simeq a$ over $F(A)$.

###### Proof.

Let $K$ be the $\mathbb{I}_{\infty}$-theory corresponding to $\mathcal{M}$,
that is, $K(x)$ is the space of global sections of $\mathcal{M}(x)$ for
$x\in\mathbb{I}_{\infty}$. As we saw in Remark 6.8, a morphism
$\Gamma:\mathbf{y}(\mathbf{P}_{\partial}^{n}(1))\to K$ corresponds to a list
of sections 14, and extensions $\mathbf{y}(\mathbf{P}_{\partial}^{n}(U))\to K$
and $\mathbf{y}(\mathbf{P}_{\partial}^{n}(E))\to K$ of $\Gamma$ correspond to
sections $\mathcal{M}({\star})/\\{\Gamma_{n}\\}\to\mathcal{M}(U)$ and
$\mathcal{M}({\star})/\\{\Gamma_{n}\\}\to\mathcal{M}(E)$, respectively. Then,
type lifting and term lifting implies the right lifting property against the
generating cofibrations. The converse is also true because, since
$\mathcal{M}$ is democratic, any object of $\mathcal{M}({\star})$ is of the
form $\\{\Gamma_{n}\\}$ for some list of sections 14. ∎

###### Proof of Lemma 6.14.

We check type lifting and term lifting along the unit
$\eta:\mathcal{M}\to\gamma_{!}\mathcal{M}\simeq L(\mathcal{M}({\star}))$ for a
democratic model $\mathcal{M}$ of $\mathbb{I}$. Type lifting is immediate
because any object in $L(\mathcal{M}({\star}))/\eta(\Gamma)$ is represented by
a fibration $A\to\Gamma$ in $\mathcal{M}({\star})$. For term lifting, we also
need the fact that $\mathcal{M}({\star})$ is not only a category of fibrant
objects but also a _tribe_ [24] and in particular a _path category_ [48]. In
this special case, a section of $\eta(A)\to\eta(\Gamma)$ in
$L(\mathcal{M}({\star}))$ for a fibration $A\to\Gamma$ in
$\mathcal{M}({\star})$ is represented by a section in $\mathcal{M}({\star})$
by [48, Corollary 2.19]. ∎

This concludes the proof that trivial fibrations are weak equivalences in
$\mathbf{Th}(\mathbb{I})$. It remains to show Proposition 6.11, which follows
from the following theorem.

######  Theorem 6.17.

Any cofibrant object of $\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})$
belongs to $\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})$.

###### Proof of Proposition 6.11.

Initial objects are cofibrant, and the pushout of a cofibration along a
morphism between cofibrant objects is cofibrant. Thus, by Theorem 6.17,
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})\subset\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})$
is closed under these colimits. ∎

Theorem 6.17 is the hardest part. We may think of this theorem as a form of
_coherence problem_. A general democratic model of $\mathbb{I}_{\infty}$ may
contain a lot of non-trivial homotopies, but Theorem 6.17 says that all the
homotopies in a cofibrant democratic model of $\mathbb{I}_{\infty}$ are
trivial.

A successful approach to coherence problems in the categorical semantics of
type theory is to replace a non-split model by a split model [20, 34].
Following them, we construct, given a democratic model $\mathcal{M}$ of
$\mathbb{I}_{\infty}$, a democratic model $\operatorname{Sp}\mathcal{M}$ of
$\mathbb{I}$ equipped with a trivial fibration
$\varepsilon:\operatorname{Sp}\mathcal{M}\to\mathcal{M}$. Then Theorem 6.17
follows from a retract argument.

The construction of $\operatorname{Sp}\mathcal{M}$ crucially relies on [43]’s
result of replacing any (Grothendieck) $\infty$-topos by a well-behaved model
category called a _type-theoretic model topos_ [43]. Let $\mathcal{M}$ be a
democratic model of $\mathbb{I}_{\infty}$. Recall that it consists of a base
$\infty$-category $\mathcal{M}({\star})$, a representable map
$\mathcal{M}(\partial):\mathcal{M}(E)\to\mathcal{M}(U)$ of right fibrations
over $\mathcal{M}({\star})$, and some other structures. Since the
$\infty$-category $\mathbf{RFib}_{\mathcal{M}({\star})}$ is an $\infty$-topos,
it is a localization
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ of
some type-theoretic model topos $\mathcal{X}$ [43, Theorem 11.1]. Then there
exists a fibration $\partial_{\mathcal{X}}:E_{\mathcal{X}}\to U_{\mathcal{X}}$
between fibrant objects in $\mathcal{X}$ such that
$\gamma_{\mathcal{X}}(\partial_{\mathcal{X}})\simeq\mathcal{M}(\partial)$. We
will choose $\partial_{\mathcal{X}}$ that has a $\mathsf{1}$-type structure, a
$\mathsf{\Sigma}$-type structure, and an $\mathsf{Id}^{+}$-type structure so
that it induces a model of $\mathbb{I}$.

We remind the reader that the type-theoretic model topos $\mathcal{X}$ has
nice properties by definition [43, Definition 6.1]: the underlying
$1$-category is a Grothendieck $1$-topos, the cofibrations are the
monomorphisms, and the model structure is right proper. The right properness
in particular implies that the localization functor
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$
preserves pullbacks of fibrations and pushforwards of fibrations along
fibrations used in the definitions of $\mathsf{1}$-type,
$\mathsf{\Sigma}$-type, and $\mathsf{Id}^{+}$-type structures.

######  Lemma 6.18.

For any cofibration $i:A\to B$ between fibrant objects in $\mathcal{X}$ and
for any fibration $p:Y\to X$ in $\mathcal{X}$, the induced map

$(i^{*},p_{*}):Y^{B}\to Y^{A}\times_{X^{A}}X^{B}$

is a fibration.

###### Proof.

By an adjoint argument, it suffices to show that for any trivial cofibration
$i^{\prime}:A^{\prime}\to B^{\prime}$, the induced map

$(i^{\prime},i):A^{\prime}\times B\amalg_{A^{\prime}\times A}B^{\prime}\times
A\to B^{\prime}\times B$

is a trivial cofibration. Since the class of cofibrations are the class of
monomorphisms in the Grothendieck $1$-topos $\mathcal{X}$, the map
$(i^{\prime},i)$ is a cofibration. Since $A$ and $B$ are fibrant and since the
model structure is right proper, the maps $i^{\prime}\times A:A^{\prime}\times
A\to B^{\prime}\times A$ and $i^{\prime}\times B:A^{\prime}\times B\to
B^{\prime}\times B$ are weak equivalences. By 2-out-of-3, the map
$(i^{\prime},i)$ is a weak equivalence. ∎

######  Lemma 6.19.

For any choice of $\partial_{\mathcal{X}}$, there exists an
$\mathsf{Id}^{+}$-type structure on $\partial_{\mathcal{X}}$ sent by
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ to
the $\mathsf{Id}^{+}$-type structure on $\mathcal{M}(\partial)$.

###### Proof.

Since all the objects in $\mathcal{X}$ are cofibrant and
$\partial_{\mathcal{X}}$ is a fibration between fibrant objects, the
commutative square 11 for $\mathcal{M}(\partial)$ can be lifted to one for
$\partial_{\mathcal{X}}$. The map $\mathsf{refl}:E\to\mathsf{Id}^{*}E$ is a
monomorphism in $\mathcal{X}$ and thus a cofibration. Applying Lemma 6.18 for
the slice $\mathcal{X}/U$ instead of $\mathcal{X}$, we see that the induced
map $(\mathsf{refl}^{*},\partial_{*})$ is a fibration. The codomain of the map
$(\mathsf{refl}^{*},\partial_{*})$ is fibrant by the right properness. Hence,
the section of $(\mathsf{refl}^{*},\partial_{*})$ for $\mathcal{M}(\partial)$
can be lifted to one for $\partial_{\mathcal{X}}$. ∎

######  Lemma 6.20.

One can choose $\partial_{\mathcal{X}}$ that has a $\mathsf{1}$-type structure
and a $\mathsf{\Sigma}$-type structure sent by
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ to
those structures on $\mathcal{M}(\partial)$.

###### Proof.

A $\mathsf{1}$-type structure and a $\mathsf{\Sigma}$-type structure on
$\partial$ are a pullback of the form

${\mathrm{dom}(\partial^{\otimes n})}$${E}$${\mathrm{cod}(\partial^{\otimes
n})}$${U}$$\scriptstyle{\mathsf{p}_{n}}$$\scriptstyle{\partial^{\otimes
n}}$$\scriptstyle{\partial}$$\scriptstyle{\mathsf{\Sigma}_{n}}$

for $n=0$ and $n=2$, respectively, where $\partial^{\otimes n}$ is the
$n$-fold composition of the polynomial $\partial$. Since $\mathcal{M}$ is a
model of $\mathbb{I}_{\infty}$, the map $\mathcal{M}(\partial)$ is equipped
with such pullbacks in $\mathbf{RFib}_{\mathcal{M}({\star})}$. However, they
gives rise to only _homotopy_ pullbacks

${\mathrm{dom}(\partial_{\mathcal{X}}^{\otimes
n})}$${E_{\mathcal{X}}}$${\mathrm{cod}(\partial_{\mathcal{X}}^{\otimes
n})}$${U_{\mathcal{X}}}$$\scriptstyle{\mathsf{p}_{n}}$$\scriptstyle{\partial_{\mathcal{X}}^{\otimes
n}}$$\scriptstyle{\partial_{\mathcal{X}}}$$\scriptstyle{\mathsf{\Sigma}_{n}}$
(16)

in $\mathcal{X}$, and thus $\partial_{\mathcal{X}}$ need not have
$\mathsf{1}$-type and $\mathsf{\Sigma}$-type structures.

The idea of fixing this issue is to replace $\partial_{\mathcal{X}}$ by
another fibration $\partial_{\mathcal{X}}^{\prime}:E_{\mathcal{X}}^{\prime}\to
U_{\mathcal{X}}^{\prime}$ between fibrant objects such that the pullbacks of
$\partial_{\mathcal{X}}^{\prime}$ are the homotopy pullbacks of
$\partial_{\mathcal{X}}$. Let $\kappa$ be a regular cardinal such that
$\partial_{\mathcal{X}}$ is $\kappa$-small. By [43, Theorem 5.22], there
exists a fibration
$\partial_{\mathcal{X}}^{\kappa}:E_{\mathcal{X}}^{\kappa}\to
U_{\mathcal{X}}^{\kappa}$ between fibrant objects that classifies
$\kappa$-small fibrations. Moreover, $\partial_{\mathcal{X}}^{\kappa}$
satisfies the univalence axiom with respect to the model structure. Since
$\partial_{\mathcal{X}}$ is $\kappa$-small, we have a pullback

${E_{\mathcal{X}}}$${E_{\mathcal{X}}^{\kappa}}$${U_{\mathcal{X}}}$${U_{\mathcal{X}}^{\kappa}.}$$\scriptstyle{\partial_{\mathcal{X}}}$$\scriptstyle{\partial_{\mathcal{X}}^{\kappa}}$$\scriptstyle{\iota}$

Factor $\iota$ into a weak equivalence $\iota^{\prime}:U_{\mathcal{X}}\to
U_{\mathcal{X}}^{\prime}$ followed by a fibration
$\pi:U_{\mathcal{X}}^{\prime}\to U_{\mathcal{X}}^{\kappa}$, and define
$\partial_{\mathcal{X}}^{\prime}:E_{\mathcal{X}}^{\prime}\to
U_{\mathcal{X}}^{\prime}$ to be the pullback of
$\partial_{\mathcal{X}}^{\kappa}$ along $\pi$. Since
$\partial_{\mathcal{X}}^{\kappa}$ satisfies the univalence axiom, we can
choose $U_{\mathcal{X}}^{\prime}$ such that the maps $A\to
U_{\mathcal{X}}^{\prime}$ correspond to the triples $(B_{1},B_{2},f)$
consisting of maps $B_{1}:A\to U_{\mathcal{X}}$ and $B_{2}:A\to
U_{\mathcal{X}}^{\kappa}$ and a weak equivalence
$f:B_{1}^{*}E_{\mathcal{X}}\to B_{2}^{*}E_{\mathcal{X}}^{\kappa}$ over $A$. In
particular, we have a _generic_ homotopy pullback from a $\kappa$-small
fibration

${E_{\mathcal{X}}^{\prime}}$${E_{\mathcal{X}}}$${U_{\mathcal{X}}^{\prime}}$${U_{\mathcal{X}}}$$\scriptstyle{\partial_{\mathcal{X}}^{\prime}}$$\scriptstyle{\partial_{\mathcal{X}}}$$\scriptstyle{p}$
(17)

in the sense that any homotopy pullback from a $\kappa$-small fibration to
$\partial_{\mathcal{X}}$ factors into a strict pullback followed by the
homotopy pullback 17.

We now construct $\mathsf{1}$-type and $\mathsf{\Sigma}$-type structures on
$\partial_{\mathcal{X}}^{\prime}$. There are homotopy pullbacks as in Eq. 16
for $n=0$ and $n=2$ sent by
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ to
the $\mathsf{1}$-type and $\mathsf{\Sigma}$-type structures, respectively, on
$\mathcal{M}(\partial)$. Since $\partial_{\mathcal{X}}$ is the pullback of
$\partial_{\mathcal{X}}^{\prime}$ along the weak equivalence
$\iota^{\prime}:U_{\mathcal{X}}\to U_{\mathcal{X}}^{\prime}$, one can
construct a commutative square

${\mathrm{dom}(\partial_{\mathcal{X}}^{\otimes
n})}$${\mathrm{dom}((\partial_{\mathcal{X}}^{\prime})^{\otimes
n})}$${\mathrm{cod}(\partial_{\mathcal{X}}^{\otimes
n})}$${\mathrm{cod}((\partial_{\mathcal{X}}^{\prime})^{\otimes
n})}$$\scriptstyle{\partial_{\mathcal{X}}^{\otimes
n}}$$\scriptstyle{(\partial_{\mathcal{X}}^{\prime})^{\otimes n}}$

in which the horizontal maps are weak equivalences. Then we have a homotopy
pullback from $(\partial_{\mathcal{X}}^{\prime})^{\otimes n}$ to
$\partial_{\mathcal{X}}$, which factors into a strict pullback followed by the
homotopy pullback 17 because the composition of polynomials preserves
$\kappa$-smallness. By construction, this strict pullback is sent by
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ to
the $\mathsf{1}$-type structure on $\mathcal{M}(\partial)$ when $n=0$ and to
the $\mathsf{\Sigma}$-type structure on $\mathcal{M}(\partial)$ when $n=2$. ∎

By the preceding lemmas, we can choose $\partial_{\mathcal{X}}$ that has a
$\mathsf{1}$-type structure, a $\mathsf{\Sigma}$-type structure, and an
$\mathsf{Id}^{+}$-type structure. Then we have a morphism of $1$-categories
with representable maps $\mathbb{I}\to\mathcal{X}$, and we define
$\operatorname{Sp}\mathcal{M}$ to be the heart of the model of $\mathbb{I}$
defined by the composite
$\mathbb{I}\to\mathcal{X}\to\mathbf{RFib}_{\mathcal{X}}$ with the Yoneda
embedding. Concretely, the base category
$(\operatorname{Sp}\mathcal{M})({\star})$ is the full subcategory of
$\mathcal{X}$ spanned by the objects $\Gamma$ such that the map $\Gamma\to 1$
is a composite of pullbacks of $\partial_{\mathcal{X}}$, and the sections
$(\operatorname{Sp}\mathcal{M})({\star})/\Gamma\to(\operatorname{Sp}\mathcal{M})(U)$
and
$(\operatorname{Sp}\mathcal{M})({\star})/\Gamma\to(\operatorname{Sp}\mathcal{M})(E)$
are the maps $\Gamma\to U_{\mathcal{X}}$ and $\Gamma\to E_{\mathcal{X}}$,
respectively, in $\mathcal{X}$.

Since the localization functor
$\gamma_{\mathcal{X}}:\mathcal{X}\to\mathbf{RFib}_{\mathcal{M}({\star})}$
sends $\partial_{\mathcal{X}}$ to the representable map
$\mathcal{M}(\partial)$ and preserves pullbacks of $\partial_{\mathcal{X}}$
along maps between fibrant objects, the restriction of $\gamma_{\mathcal{X}}$
to $(\operatorname{Sp}\mathcal{M})({\star})$ factors through the Yoneda
embedding $\mathcal{M}({\star})\to\mathbf{RFib}_{\mathcal{M}({\star})}$. Let
$\varepsilon_{{\star}}:(\operatorname{Sp}\mathcal{M})({\star})\to\mathcal{M}({\star})$
be the induced functor.

${(\operatorname{Sp}\mathcal{M})({\star})}$${\mathcal{M}({\star})}$${\mathcal{X}}$${\mathbf{RFib}_{\mathcal{M}({\star})}}$$\scriptstyle{\varepsilon_{{\star}}}$$\scriptstyle{\mathbf{y}}$$\scriptstyle{\gamma_{\mathcal{X}}}$

The functor $\gamma_{\mathcal{X}}$ also induces maps
$\varepsilon_{U}:(\operatorname{Sp}\mathcal{M})(U)\to\mathcal{M}(U)$ and
$\varepsilon_{E}:(\operatorname{Sp}\mathcal{M})(E)\to\mathcal{M}(E)$ of right
fibrations over $\varepsilon_{{\star}}$, and these define a morphism
$\varepsilon:\operatorname{Sp}\mathcal{M}\to\mathcal{M}$ of models of
$\mathbb{I}_{\infty}$.

######  Lemma 6.21.

The morphism $\varepsilon:\operatorname{Sp}\mathcal{M}\to\mathcal{M}$ is a
trivial fibration.

###### Proof.

We verify type lifting and term lifting. To give type lifting, let
$\Gamma\in(\operatorname{Sp}\mathcal{M})({\star})$ be an object and
$A:\mathcal{M}({\star})/\varepsilon_{{\star}}(\Gamma)\to\mathcal{M}(U)$ a
section. Since
$\mathcal{M}({\star})/\varepsilon_{{\star}}(\Gamma)\simeq\gamma_{\mathcal{X}}(\Gamma)$
and $\mathcal{M}(U)\simeq\gamma_{\mathcal{X}}(U_{\mathcal{X}})$, the section
$A$ is represented by some map $\Gamma\to U_{\mathcal{X}}$ in $\mathcal{X}$,
that is, a section
$(\operatorname{Sp}\mathcal{M})({\star})/\Gamma\to(\operatorname{Sp}\mathcal{M})(U)$.
Term lifting can be checked in the same way. ∎

###### Proof of Theorem 6.17.

Let $\mathcal{M}$ be a cofibrant democratic model of $\mathbb{I}_{\infty}$.
Then we have a section of the trivial fibration
$\varepsilon:\operatorname{Sp}\mathcal{M}\to\mathcal{M}$. Since
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})\subset\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I}_{\infty})$
is closed under retracts, $\mathcal{M}$ belongs to
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{I})$. ∎

In conclusion we have shown that $\mathbf{Th}(\mathbb{I})$ is a category with
weak equivalences and cofibrations. Moreover, Proposition 6.11 also implies
that $\gamma_{!}\tau^{*}$ is left exact. Thus, to show that this map induces
an equivalence after localization, it is enough to show the left approximation
property. Since the first axiom is satisfied by definition, we only have to
show the second. But this is now an easy task using Lemmas 6.13, 6.14 and
6.17.

######  Lemma 6.22.

For any cofibrant $\mathbb{I}$-theory $K$ and any morphism
$f:\gamma_{!}\tau^{*}K\to L$ in $\mathbf{Th}(\mathbb{E}_{\infty})$, there
exists a morphism $f^{\prime}:K\to L^{\prime}$ in $\mathbf{Th}(\mathbb{I})$
such that $\gamma_{!}\tau^{*}L^{\prime}\simeq L$ under $\gamma_{!}\tau^{*}K$.

###### Proof.

Let $f:\gamma_{!}\tau^{*}K\to L$ be a morphism in
$\mathbf{Th}(\mathbb{E}_{\infty})$ where $K$ is a cofibrant
$\mathbb{I}$-theory. By Lemma 6.13 and the small object argument, $f$ is
written as a transfinite composite of pushouts of generating cofibrations.
Thus, it suffices to prove the case when $f$ is a pushout of a generating
cofibration. Let us assume that $f$ is a pushout of the form

${\gamma_{!}A}$${\gamma_{!}\tau^{*}K}$${\gamma_{!}B}$${L}$$\scriptstyle{g}$$\scriptstyle{\gamma_{!}i}$$\scriptstyle{f}$$\scriptstyle{h}$
(18)

where $i:A\to B$ is one of the generating cofibrations in
$\mathbf{Th}(\mathbb{I}_{\infty})$. Since $A$ is cofibrant, the transpose
$A\to\gamma^{*}\gamma_{!}\tau^{*}K$ of $g$ factors through the unit
$\tau^{*}K\to\gamma^{*}\gamma_{!}\tau^{*}K$ by Lemma 6.14. Let
$g^{\prime}:\tau_{!}A\to K$ be the transpose of the induced morphism
$A\to\tau^{*}K$ and take the pushout

${\tau_{!}A}$${K}$${\tau_{!}B}$${L^{\prime}.}$$\scriptstyle{g^{\prime}}$$\scriptstyle{\tau_{!}i}$
(19)

By Theorem 6.17, the units $A\to\tau^{*}\tau_{!}A$ and $B\to\tau^{*}\tau_{!}B$
are invertible, and $\gamma_{!}\tau^{*}$ sends the pushout 19 to the pushout
18 since $K$ is cofibrant. Hence, $\gamma_{!}\tau^{*}L^{\prime}$ is equivalent
to $L$ under $\gamma_{!}\tau^{*}K$. ∎

###### Proof of Theorem 6.2.

By Theorem 6.9, the category $\mathbf{Th}(\mathbb{I})$ is a category with weak
equivalences and cofibrations, and Proposition 6.11 implies that the functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\mathbb{I})\to\mathbf{Th}(\mathbb{E}_{\infty})$
is right exact. We checked the left approximation property in Lemma 6.22.
Thus, by Proposition 6.6, $\gamma_{!}\tau^{*}$ induces an equivalence
$L(\mathbf{Th}(\mathbb{I}))\simeq\mathbf{Th}(\mathbb{E}_{\infty})$. ∎

###  6.2 Generalizations

We end this section with discussion about generalizations of Theorem 6.2. Let
$\widetilde{\mathbb{I}}$ be an extension of $\mathbb{I}$ with some type-
theoretic structures such as $\mathsf{\Pi}$-types and (higher) inductive
types, and we similarly define extensions $\widetilde{\mathbb{I}}_{\infty}$
and $\widetilde{\mathbb{E}}_{\infty}$ of $\mathbb{I}_{\infty}$ and
$\mathbb{E}_{\infty}$, respectively. We have a span

${\widetilde{\mathbb{I}}}$${\widetilde{\mathbb{I}}_{\infty}}$${\widetilde{\mathbb{E}}_{\infty}}$$\scriptstyle{\tau}$$\scriptstyle{\gamma}$

and ask if the functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\widetilde{\mathbb{I}})\to\mathbf{Th}(\widetilde{\mathbb{E}}_{\infty})$
induces an equivalence

$L(\mathbf{Th}(\widetilde{\mathbb{I}}))\simeq\mathbf{Th}(\widetilde{\mathbb{E}}_{\infty}).$

Most part of the proof of Theorem 6.2 works also for this case, but we have to
modify Lemmas 6.15 and 6.20. For Lemma 6.15, we need to find a
$\infty$-categorical structure corresponding to
$\widetilde{\mathbb{E}}_{\infty}$-theories and show that the localization
$L(\mathcal{M}({\star}))$ for a democratic model $\mathcal{M}$ of
$\widetilde{\mathbb{I}}$ has that structure. For example, in the case when
$\widetilde{\mathbb{I}}$ is the extension $\mathbb{I}^{\mathsf{\Pi}}$ of
$\mathbb{I}$ with $\mathsf{\Pi}$-types satisfying function extensionality in
the sense of [45, Section 2.9], we have
$\mathbf{Th}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})\simeq\mathbf{LCCC}_{\infty}$
(Theorem 5.25), and by the results of [26], $L(\mathcal{M}({\star}))$ is
indeed locally cartesian closed. When we extend $\mathbb{I}$ with (higher)
inductive types, the corresponding $\infty$-categorical structure will be some
form of pullback-stable initial algebras. For Lemma 6.20, we have to choose
the fibration $\partial_{\mathcal{X}}$ such that it also has the type-
theoretic structures that $\widetilde{\mathbb{I}}$ has. In the case of
$\widetilde{\mathbb{I}}=\mathbb{I}^{\mathsf{\Pi}}$, one might want to choose
the regular cardinal $\kappa$ in the proof of Lemma 6.20 such that
$\kappa$-small fibrations are closed under pushforwards. However, there is no
guarantee of the existence of such a regular cardinal within the same
Grothendieck universe, unless the Grothendieck universe is _$1$ -accessible_,
that is, there are unboundedly many inaccessible cardinals [33]. Nevertheless,
the existence of $\operatorname{Sp}\mathcal{M}$ in a larger universe is enough
to prove Theorem 6.17, and thus we have the second part of Conjecture 3.7 of
[27] under an extra assumption on universes.

######  Theorem 6.23.

Suppose that our ambient Grothendieck universe is $1$-accessible or contained
in a larger universe. Then the functor
$\gamma_{!}\tau^{*}:\mathbf{Th}(\mathbb{I}^{\mathsf{\Pi}})\to\mathbf{Th}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})$
induces an equivalence of $\infty$-categories

$L(\mathbf{Th}(\mathbb{I}^{\mathsf{\Pi}}))\simeq\mathbf{Th}(\mathbb{E}_{\infty}^{\mathsf{\Pi}})\simeq\mathbf{LCCC}_{\infty}.$

The current proof of Lemma 6.20 has some issues when generalizing it. As we
have seen, it could cause a rise in universe levels. Furthermore, the same
proof does not work when we extend $\mathbb{I}$ with (higher) inductive types,
because having (higher) inductive types is not a closure property. One
possible approach to these issues is to refine the construction of
$\operatorname{Sp}\mathcal{M}$. The current construction does not depend on
the choice of a type-theoretic model topos $\mathcal{X}$ that presents
$\mathbf{RFib}_{\mathcal{M}({\star})}$, but there should be a convenient
choice to work with. Another approach is to give a totally different proof of
Theorem 6.17 without the use of $\operatorname{Sp}\mathcal{M}$. There has been
a syntactic approach to coherence problems initiated by [14]. In this
approach, coherence problems are solved by rewriting techniques, and we expect
that it works for a wide range of type-theoretic structures without a rise of
universe levels. Of course, we first have to develop nice syntax for
$\infty$-type theories, and this is not obvious.

##  7 Conclusion and future work

We introduced $\infty$-type theories as a higher dimensional generalization of
type theories and as an application proved [27]’s conjecture that the
$\infty$-category of small left exact $\infty$-categories is a localization of
the category of theories over Martin-Löf type theory with intensional identity
types [27]. The technique developed in this paper also works for the internal
language conjecture for locally cartesian closed $\infty$-categories, but
further generalization including (higher) inductive types is left as future
work.

###  7.1 Syntax for $\infty$-type theories

Coherence problems are often solved by syntactic arguments [14]. Therefore,
syntactic presentations of $\infty$-type theories will be helpful for solving
internal language conjectures for structured $\infty$-categories. We have not
figured out syntax for $\infty$-type theories. Here we consider one
possibility based on _logical frameworks_.

In the previous work [46], the author introduced a logical framework to define
type theories. For every signature $\Sigma$ in that logical framework, the
syntactic category $\mathbb{R}(\Sigma)$ is naturally equipped with a structure
of a category with representable maps and satisfies a certain universal
property. To define $\infty$-type theories syntactically, we modify the
logical framework as follows:

  * •

the new logical framework has intensional identity types instead of
extensional identity types;

  * •

dependent product types indexed over representable types satisfy the function
extensionality axiom.

######  Remark 7.1.

A similar kind of framework is used by [7, Section 7] to represent space-
valued models of a type theory.

######  Proposition 7.2.

Let $\Sigma$ be a signature in this new logical framework.

  1. 1.

The syntactic category $\mathbb{R}(\Sigma)$ is equipped with a structure of a
fibration category.

  2. 2.

The localization $L(\mathbb{R}(\Sigma))$ is equipped with a structure of an
$\infty$-category with representable maps.

###### Proof.

It is known [4] that the syntactic category of a type theory with intensional
identity types is a fibration category. The second claim is proved in the same
way as the fact that the localization of a locally cartesian closed fibration
category is a locally cartesian closed $\infty$-category [26, 12]. ∎

We expect that the syntactic $\infty$-category with representable maps
$L(\mathbb{R}(\Sigma))$ satisfies a universal property analogous to [46,
Theorem 5.17] so that the logical framework with intensional identity types
provides syntactic presentations of $\infty$-type theories.

## References

  * [1] M. Anel, G. Biedermann, E. Finster and A. Joyal  “Goodwillie’s calculus of functors and higher topos theory”  In _J. Topol._ 11.4, 2018, pp. 1100–1132  DOI: 10.1112/topo.12082
  * [2] Mathieu Anel, Georg Biedermann, Eric Finster and André Joyal  “A generalized Blakers-Massey theorem”  In _J. Topol._ 13.4, 2020, pp. 1521–1553  DOI: 10.1112/topo.12163
  * [3] Peter Arndt and Krzysztof Kapulkin  “Homotopy-Theoretic Models of Type Theory”  In _Typed Lambda Calculi and Applications: 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings_ Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 45–60  DOI: 10.1007/978-3-642-21691-6˙7
  * [4] Jeremy Avigad, Krzysztof Kapulkin and Peter LeFanu Lumsdaine  “Homotopy limits in type theory”  In _Mathematical Structures in Computer Science_ 25.5 Cambridge University Press, 2015, pp. 1040–1070  DOI: 10.1017/S0960129514000498
  * [5] Steve Awodey  “Natural models of homotopy type theory”  In _Mathematical Structures in Computer Science_ 28.2 Cambridge University Press, 2018, pp. 241–286  DOI: 10.1017/S0960129516000268
  * [6] Steve Awodey and Michael A. Warren  “Homotopy theoretic models of identity types”  In _Mathematical Proceedings of the Cambridge Philosophical Society_ 146.1 Cambridge University Press, 2009, pp. 45–55  DOI: 10.1017/S0305004108001783
  * [7] Rafaël Bocquet  “Coherence of strict equalities in dependent type theories”, 2020  arXiv:2010.14166v1
  * [8] Kenneth S. Brown  “Abstract homotopy theory and generalized sheaf cohomology”  In _Transactions of the American Mathematical Society_ 186 American Mathematical Society, 1973, pp. 419–458  DOI: 10.2307/1996573
  * [9] Guillaume Brunerie  “On the homotopy groups of spheres in homotopy type theory”, 2016  arXiv:1606.05916v1
  * [10] Guillaume Brunerie  “The James construction and $\pi_{4}(\mathbb{S}^{3})$ in homotopy type theory”  In _J. Automat. Reason._ 63.2, 2019, pp. 255–284  DOI: 10.1007/s10817-018-9468-2
  * [11] J.. Cartmell  “Generalised algebraic theories and contextual categories”, 1978
  * [12] Denis-Charles Cisinski  “Higher Categories and Homotopical Algebra”, Cambridge Studies in Advanced Mathematics  Cambridge University Press, 2019  DOI: 10.1017/9781108588737
  * [13] Pierre Clairambault and Peter Dybjer  “The biequivalence of locally cartesian closed categories and Martin-Löf type theories”  In _Mathematical Structures in Computer Science_ 24.6 Cambridge University Press, 2014, pp. e240606  DOI: 10.1017/S0960129513000881
  * [14] Pierre-Louis Curien  “Substitution up to Isomorphism”  In _Fundam. Inform._ 19.1/2, 1993, pp. 51–85
  * [15] Peter Dybjer  “Internal Type Theory”  In _Types for Proofs and Programs: International Workshop, TYPES ’95 Torino, Italy, June 5–8, 1995 Selected Papers_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1996, pp. 120–134  DOI: 10.1007/3-540-61780-9˙66
  * [16] Marcelo Fiore  “Discrete Generalised Polynomial Functors” Talk at ICALP 2012, 2012  URL: http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf
  * [17] Nicola Gambino and Joachim Kock  “Polynomial functors and polynomial monads”  In _Mathematical Proceedings of the Cambridge Philosophical Society_ 154.1 Cambridge University Press, 2013, pp. 153–192  DOI: 10.1017/S0305004112000394
  * [18] Richard Garner  “Combinatorial structure of type dependency”  In _Journal of Pure and Applied Algebra_ 219.6, 2015, pp. 1885–1914  DOI: 10.1016/j.jpaa.2014.07.015
  * [19] David Gepner and Joachim Kock  “Univalence in locally cartesian closed $\infty$-categories”  In _Forum Mathematicum_ 29.3, 2017  DOI: 10.1515/forum-2015-0228
  * [20] Martin Hofmann  “On the interpretation of type theory in locally cartesian closed categories”  In _Computer Science Logic_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1995, pp. 427–441  DOI: 10.1007/BFb0022273
  * [21] Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata and Peter LeFanu Lumsdaine  “A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory”  In _Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)_ ACM, New York, 2016, pp. 10  DOI: 10.1145/2933575.2934545
  * [22] Valery Isaev  “Algebraic Presentations of Dependent Type Theories”, 2018  arXiv:1602.08504v3
  * [23] André Joyal  “Notes on quasi-categories”, 2008  URL: http://www.math.uchicago.edu/~may/IMA/Joyal.pdf
  * [24] André Joyal  “Notes on clans and tribes”, 2017  arXiv:1710.10238v1
  * [25] André Joyal and Myles Tierney  “Quasi-categories vs Segal spaces”  In _Categories in algebra, geometry and mathematical physics_ 431, Contemp. Math.  Amer. Math. Soc., Providence, RI, 2007, pp. 277–326  DOI: 10.1090/conm/431/08278
  * [26] Krzysztof Kapulkin  “Locally cartesian closed quasi-categories from type theory”  In _Journal of Topology_ 10.4, 2017, pp. 1029–1049  DOI: 10.1112/topo.12031
  * [27] Krzysztof Kapulkin and Peter LeFanu Lumsdaine  “The homotopy theory of type theories”  In _Adv. Math._ 337, 2018, pp. 1–38  DOI: 10.1016/j.aim.2018.08.003
  * [28] Krzysztof Kapulkin and Peter LeFanu Lumsdaine  “The simplicial model of Univalent Foundations (after Voevodsky)”  In _Journal of the European Mathematical Society_ , 2021  DOI: 10.4171/JEMS/1050
  * [29] Krzysztof Kapulkin and Karol Szumiło  “Internal languages of finitely complete $(\infty,1)$-categories”  In _Selecta Math. (N.S.)_ 25.2, 2019, pp. Art. 3346  DOI: 10.1007/s00029-019-0480-0
  * [30] J. Lambek and P.. Scott  “Introduction to Higher Order Categorical Logic”  Cambridge University Press, 1986
  * [31] F. Lawvere  “Functorial Semantics of Algebraic Theories”, 1963  URL: http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html
  * [32] Daniel R. Licata and Michael Shulman  “Calculating the fundamental group of the circle in homotopy type theory”  In _2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)_ IEEE Computer Soc., Los Alamitos, CA, 2013, pp. 223–232  DOI: 10.1109/LICS.2013.28
  * [33] Giulio Lo Monaco  “Dependent products and 1-inaccessible universes”  In _Theory and Applications of Categories_ 37.5, 2021, pp. 107–143  URL: http://www.tac.mta.ca/tac/volumes/37/5/37-05abs.html
  * [34] Peter LeFanu Lumsdaine and Michael A. Warren  “The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories”  In _ACM Trans. Comput. Logic_ 16.3 New York, NY, USA: ACM, 2015, pp. 23:1–23:31  DOI: 10.1145/2754931
  * [35] Jacob Lurie  “Higher Algebra”, 2009  URL: http://www.math.harvard.edu/~lurie/papers/HA.pdf
  * [36] Jacob Lurie  “Higher Topos Theory”  Princeton University Press, 2009  URL: https://www.math.ias.edu/~lurie/papers/HTT.pdf
  * [37] Hoang Kim Nguyen  “Theorems in Higher Category Theory and Applications”, 2019  DOI: 10.5283/epub.38448
  * [38] Hoang Kim Nguyen, George Raptis and Christoph Schrade  “Adjoint functor theorems for $\infty$-categories”  In _Journal of the London Mathematical Society_ , 2019  DOI: 10.1112/jlms.12282
  * [39] Nima Rasekh  “Complete Segal Objects”, 2018  arXiv:1805.03561v1
  * [40] Nima Rasekh  “Univalence in Higher Category Theory”, 2021  arXiv:2103.12762v2
  * [41] Emily Riehl and Dominic Verity  “Elements of $\infty$-Category Theory”, Cambridge Studies in Advanced Mathematics  Cambridge University Press, 2022  DOI: 10.1017/9781108936880
  * [42] Michael Shulman  “Univalence for inverse diagrams and homotopy canonicity”  In _Mathematical Structures in Computer Science_ 25.05, 2015, pp. 1203–1277  DOI: 10.1017/s0960129514000565
  * [43] Michael Shulman  “All $(\infty,1)$-toposes have strict univalent universes”, 2019  arXiv:1904.07004v2
  * [44] Karol Szumiło  “Two Models for the Homotopy Theory of Cocomplete Homotopy Theories”  University of Bonn, 2014  arXiv:1411.0303v1
  * [45] The Univalent Foundations Program  “Homotopy Type Theory: Univalent Foundations of Mathematics”, 2013  URL: http://homotopytypetheory.org/book/
  * [46] Taichi Uemura  “A General Framework for the Semantics of Type Theory”, 2019  arXiv:1904.04097v2
  * [47] Taichi Uemura  “The universal exponentiable arrow”  In _Journal of Pure and Applied Algebra_ 226.7, 2022, pp. 106991  DOI: 10.1016/j.jpaa.2021.106991
  * [48] Benno Berg and Ieke Moerdijk  “Exact completion of path categories and algebraic set theory: Part I: Exact completion of path categories”  In _Journal of Pure and Applied Algebra_ 222.10, 2018, pp. 3137–3181  DOI: 10.1016/j.jpaa.2017.11.017
  * [49] Vladimir Voevodsky  “B-systems”, 2014  arXiv:1410.5389v1
  * [50] Mark Weber  “Polynomials in categories with pullbacks”  In _Theory and Applications of Categories_ 30.16, 2015, pp. 533–598  URL: http://www.tac.mta.ca/tac/volumes/30/16/30-16abs.html