#  $\infty$-type theories

Hoang Kim Nguyen  Taichi Uemura

###### Abstract

We introduce $\infty$-type theories as an $\infty$-categorical generalization
of the categorical definition of type theories introduced by the second named
author. We establish analogous results to the previous work including the
construction of initial models of $\infty$-type theories, the construction of
internal languages of models of $\infty$-type theories, and the theory-model
correspondence for $\infty$-type theories. Some structured
$(\infty,1)$-categories are naturally regarded as models of some $\infty$-type
theories. Thus, since every (1-categorical) type theory is in particular an
$\infty$-type theory, $\infty$-type theories provide a unified framework for
connections between type theories and $(\infty,1)$-categorical structures. As
an application we prove Kapulkin and Lumsdaine’s conjecture that the dependent
type theory with intensional identity types gives internal languages for
$(\infty,1)$-categories with finite limits.

##  1 Introduction

_Type theory_ and _higher category theory_ are closely related: dependent type
theories with intensional identity types provide a syntactic way of reasoning
about $(\infty,1)$-categories. This is known as the family of _internal
language conjectures_ and has led for example to syntactic developments of
classical material in homotopy theory such as the homotopy groups of spheres
[9, 10, 32] and the Blakers-Massey Theorem [21], just to name a few. These
proofs often lead to new perspectives on classical material and their nature
makes them applicable to a wider class of $(\infty,1)$-categories, importing
ideas from the homotopy theory of spaces to other $(\infty,1)$-categories, see
for example [1] and [2]. One of the main appeals of type theory for higher
category theory and homotopy theory is thus the usage of this type theoretic
language to reason in a synthetic way. On the other hand, higher categories
will be useful for the study of type theories. For example, one can expect a
conceptual proof of Voevodsky’s homotopy canonicity conjecture that any closed
term of the type of natural numbers is homotopic to a numeral using a higher
dimensional analogue of the Freyd cover [30].

However, internal language conjectures are still open problems in _homotopy
type theory_ [45]. The advantage of type-theoretic languages, that a lot of
equations _strictly_ hold in type theories so that a lot of trivial homotopies
in $(\infty,1)$-categories can be eliminated, is at the same time the main
difficulty of internal language conjectures. One has to justify interpreting
strict equality in type theories as homotopies in $(\infty,1)$-categories.
This is an $\infty$-dimensional version of the _coherence problem_ in the
categorical semantics of type theories.

An internal language conjecture should be formulated as an equivalence between
an $(\infty,1)$-category of theories and an $(\infty,1)$-category of
structured $(\infty,1)$-categories. Currently, only a few internal language
conjectures have been made precise. [27] made precise formulations of the
simplest cases and conjectured that the $(\infty,1)$-category of theories over
Martin-Löf type theory with intensional identity types (and dependent function
types with function extensionality) is equivalent to the $(\infty,1)$-category
of small $(\infty,1)$-categories with finite limits (and pushforwards). In
this paper, we prove [27]’s conjecture by introducing a novel
$\infty$-dimensional generalization of type theories which we call _$\infty$
-type theories_.

The basic strategy for proving [27]’s conjecture is to decompose the
equivalence to be proved into smaller pieces. An existing approach is to
introduce $1$-categorical presentations of $(\infty,1)$-categories with finite
limits. It had already been shown by [44] that $(\infty,1)$-categories with
finite limits are equivalent to categories of fibrant objects in the sense of
[8]. [29] then proved that categories of fibrant objects are equivalent to
[24]’s tribes [24]. Tribes are considered as $1$-categorical models of the
type theory, but a full proof of the equivalence between tribes and theories
has not yet been achieved.

Although this approach is natural for those who know the homotopical
interpretation of intensional identity types [6, 3, 42], $1$-categorical
models of intensional identity types are not convenient to work with. A
problem is that $1$-categories of $1$-categorical models of type theories need
not be rich enough to calculate the $(\infty,1)$-categories they present. It
is also unclear if this approach can be generalized to internal language
conjectures for richer type theories.

In this paper we seek another path. The key idea is to introduce a notion of
_$\infty$ -type theories_, an $\infty$-dimensional generalization of type
theories. Intuitively, an $\infty$-type theory is a kind of type theory but
equality is like homotopies rather than strict one. Ordinary type theories are
considered as truncated $\infty$-type theories in the sense that all
homotopies are trivial.

Our proof strategy is as follows. Let $\mathbb{I}$ denote the type theory with
intensional identity types. We introduce an $\infty$-type theory
$\mathbb{I}_{\infty}$ which is analogous to $\mathbb{I}$ but without
truncation. Because $\mathbb{I}_{\infty}$ is already a higher dimensional
object, it is straightforward to interpret $\mathbb{I}_{\infty}$ in
$(\infty,1)$-categories with finite limits. The internal language conjecture
is then reduced to a coherence problem between $\mathbb{I}$ and
$\mathbb{I}_{\infty}$: how to interpret $\mathbb{I}$ in models of
$\mathbb{I}_{\infty}$. Although this coherence problem is as difficult as the
original internal language conjecture, this reduction is an important step.
Since the problem is now formulated in the language of $\infty$-type theories
and related concepts, our proof strategy is easily generalized to internal
language conjectures for richer type theories. When we extend $\mathbb{I}$ by
some type constructors, we just extend $\mathbb{I}_{\infty}$ in the same way.

A solution to coherence problems in the $1$-categorical semantics of type
theories given by [20] is to replace a “non-split” model, in which equality
between types is up to isomorphism, by an equivalent “split” model, in which
equality between types is strict. In our approach, models of
$\mathbb{I}_{\infty}$ are like non-split models of $\mathbb{I}$, so we
consider replacing a model of $\mathbb{I}_{\infty}$ by an equivalent model of
$\mathbb{I}$. Splitting techniques for $(\infty,1)$-categorical structures
have not yet been fully developed except for some presentable
$(\infty,1)$-categories considered by [19, 43]. Since we have to split small
$(\infty,1)$-categories which are usually non-presentable, their results
cannot directly apply. However, as he already mentioned in [43, Remark 1.4],
[43]’s result on splitting presentable $(\infty,1)$-toposes can be used for
splitting small $(\infty,1)$-categories by embedding them into presheaf
$(\infty,1)$-toposes.

#### Organization

In Section 2 we fix notations and remember some concepts in
$(\infty,1)$-category theory. Relevant concepts to this paper are _$\infty$
-cosmoi_ [41], _compactly generated_ $(\infty,1)$-categories, _exponentiable_
arrows, and _representable maps_ between right fibrations.

We introduce the notion of an $\infty$-type theory in Section 3. It is defined
as an $(\infty,1)$-category with a certain structure, generalizing the
categorical definition of type theories introduced by the second named author
[46]. There are two important notions around $\infty$-type theories: _models_
and _theories_. The notion of models we have in mind is a generalization of
categories with families [15] and, equivalently, natural models [5, 16]. The
notion of theories is close to the essentially algebraic definitions of
theories given by [18, 22, 49].

In Section 4 we prove $\infty$-analogue of the main results of the previous
work [46]. Given an $\infty$-type theory $\mathbb{T}$, we construct a functor
that assigns to each model of $\mathbb{T}$ a $\mathbb{T}$-theory called the
_internal language_ of the model. The internal language functor has a fully
faithful left adjoint which constructs a _syntactic model_ from a
$\mathbb{T}$-theory. We further characterize the image of the left adjoint.

We study some concrete $\infty$-type theories in Section 5. The most basic
example is $\mathbb{E}_{\infty}$, the $\infty$-analogue of Martin-Löf type
theory with _extensional_ identity types. We show that
$\mathbb{E}_{\infty}$-theories are equivalent to $(\infty,1)$-categories with
finite limits (Theorem 5.15), which is an $\infty$-analogue of the result of
[13]. This is to be an intermediate step toward [27]’s conjecture, but it also
has an interesting corollary. One can derive a new universal property of the
$(\infty,1)$-category of small $(\infty,1)$-categories with finite limits from
a universal property of $\mathbb{E}_{\infty}$ (Corollary 5.21). We also study
a couple of examples of $\infty$-type theories with dependent function types.
Finally in Section 6 we prove [27]’s conjecture.

##  2 Preliminaries

###  2.1 $\infty$-categories

For concreteness, we will work with _$\infty$ -categories_, also called
_quasicategories_ in the literature, [23, 36, 12] as models for
$(\infty,1)$-categories. An $\infty$-category is a simplicial set satisfying
certain horn filling conditions. We recollect some standard definitions and
notations.

######  Definition 2.1.

  1. 1.

Given an $\infty$-category $\mathcal{C}$ and a simplicial set $A$, we denote
$\mathbf{Fun}(A,\mathcal{C})$ the internal hom of simplicial sets, which is
itself an $\infty$-category and models the $\infty$-category of functors and
natural transformations.

  2. 2.

For an $\infty$-category $\mathcal{C}$, we denote by $\mathcal{C}^{\simeq}$
the largest $\infty$-groupoid (Kan complex) contained in $\mathcal{C}$.
Furthermore we write
$\mathrm{k}(\mathcal{C},\mathcal{D}):=\mathbf{Fun}(\mathcal{C},\mathcal{D})^{\simeq}$.

  3. 3.

For an $\infty$-category $\mathcal{C}$, we denote by $C^{\triangleright}$ the
join $\mathcal{C}\star\Delta^{0}$.

  4. 4.

We denote by $\mathbf{Cat}_{\infty}$ the $\infty$-category of small
$\infty$-categories. This is obtained as the homotopy coherent nerve of the
simplicial category with objects given by small $\infty$-categories and hom
simplicial sets given by $\mathrm{k}(\mathcal{C},\mathcal{D})$.

  5. 5.

We denote by $\mathbf{CAT}_{\infty}$ the $\infty$-category of (possibly large)
$\infty$-categories obtained in a similar way.

  6. 6.

We denote by $\mathbf{S}$ the $\infty$-category of small $\infty$-groupoids
obtained as the homotopy coherent nerve of the simplicial category with
objects small Kan complexes and hom simplicial sets given by the internal hom
of simplicial sets.

Although we chose to work with $\infty$-categories, we will primarily use the
language of the formal category theory of $\infty$-categories as expressed by
$\infty$-cosmoi. Therefore, most of our constructions, statements and proofs
are independent of the model.

###  2.2 $\infty$-cosmoi

An _$\infty$ -cosmos_ [41] is, roughly, a complete $(\infty,2)$-category with
enough structure to do formal category theory. More concretely, an
$\infty$-cosmos $\mathcal{K}$ is a simplicially enriched category such that
for any pair of objects $\mathcal{C},\mathcal{D}\in\mathcal{K}$, the hom
simplicial set $\mathcal{K}(\mathcal{C},\mathcal{D})$ is an $\infty$-category.
$\mathcal{K}$ is also equipped a class of morphisms called isofibrations, and
all small $(\infty,1)$-categorical limits are constructible from products and
pullbacks of isofibrations. Moreover, $\mathcal{K}$ has cotensors with small
simplicial sets $A\pitchfork\mathcal{C}$ characterized by the equivalence
(isomorphism, in fact) of $\infty$-categories

$\mathcal{K}(\mathcal{D},A\pitchfork\mathcal{C})\simeq\mathbf{Fun}(A,\mathcal{K}(\mathcal{D},\mathcal{C})).$

Given an $\infty$-category, we may take its _homotopy category_ , which is
just an ordinary category. Applying this to the hom spaces of an
$\infty$-cosmos gives rise to a 2-category. Adjunctions and equivalences in
$\infty$-cosmoi are then defined in the usual way using this 2-category.

######  Example 2.2.

We denote by $\mathfrak{CAT}_{\infty}$ the $\infty$-cosmos of (possibly large)
$\infty$-categories. That is, $\mathfrak{CAT}_{\infty}$ is the simplicial
category with objects (possibly large) $\infty$-categories and hom simplicial
sets $\mathbf{Fun}(\mathcal{C},\mathcal{D})$. The cotensor
$A\pitchfork\mathcal{C}$ in $\mathfrak{CAT}_{\infty}$ is given by the functor
$\infty$-category $\mathbf{Fun}(A,\mathcal{C})$ and adjunctions and
equivalences agree with the standard notions of $\infty$-categories.

Cartesian fibrations and right fibrations in $\infty$-cosmoi are characterized
by analogy with those in complete 2-categories. Here we prefer to work with
versions of these concepts that are invariant under equivalence. The following
definition coincides with [41]’s when $F$ is an isofibration.

######  Definition 2.3.

A functor $F\colon\mathcal{C}\to\mathcal{D}$ in an $\infty$-cosmos
$\mathcal{K}$ is said to be a _cartesian fibration_ if the functor

$(\mathrm{ev}_{1},F_{\ast})\colon\Delta^{1}\pitchfork\mathcal{C}\to\mathcal{C}\times_{\mathcal{D}}\Delta^{1}\pitchfork\mathcal{D}$

has a right adjoint with invertible counit. A _fibred functor_ between
cartesian fibrations is a morphism in $\mathcal{K}^{\to}$ that commutes with
the right adjoint of $(\mathrm{ev}_{1},F_{\ast})$. A cartesian fibration is a
_right fibration_ if $(\mathrm{ev}_{1},F_{\ast})$ is an equivalence.

For a small $\infty$-category $\mathcal{C}$, we denote by
$\mathbf{CartFib}_{\mathcal{C}}\subset\mathbf{Cat}_{\infty}/\mathcal{C}$ the
$\infty$-category of cartesian fibrations over $\mathcal{C}$ and fibred
functors over $\mathcal{C}$. We denote by
$\mathbf{RFib}_{\mathcal{C}}\subset\mathbf{CartFib}_{\mathcal{C}}$ the full
subcategory spanned by the right fibrations over $\mathcal{C}$. Note that any
functor between right fibrations over $\mathcal{C}$ is automatically a fibred
functor, so $\mathbf{RFib}_{\mathcal{C}}$ is a full subcategory of
$\mathbf{Cat}_{\infty}/\mathcal{C}$. We write
$\mathbf{RFib}\subset\mathcal{C}_{\infty}^{\to}$ for the full subcategory
spanned by the right fibrations.

###  2.3 Compactly generated $\infty$-categories

######  Definition 2.4 ([36, Definition 5.5.7.1 and Theorem 5.5.1.1]).

An $\infty$-category $\mathcal{C}$ is said to be _compactly generated_ if it
is an $\omega$-accessible localization of
$\mathbf{Fun}(\mathcal{D}^{\mathrm{op}},\mathbf{S})$, that is, a reflective
full subcategory of $\mathbf{Fun}(\mathcal{D}^{\mathrm{op}},\mathbf{S})$
closed under filtered colimits, for some small $\infty$-category
$\mathcal{D}$. The subcategory of $\mathbf{CAT}_{\infty}$ spanned by the
compactly generated $\infty$-categories and $\omega$-accessible right adjoints
is denoted by $\mathbf{Pr}^{R}_{\omega}$. We will moreover denote by
$\mathfrak{Pr}^{R}_{\omega}\subset\mathfrak{CAT}_{\infty}$ the locally full
subcategory spanned by the compactly generated $\infty$-categories and
$\omega$-accessible right adjoints.

Recall [36, Proposition 5.5.7.6] that
$\mathbf{Pr}^{R}_{\omega}\subset\mathbf{CAT}_{\infty}$ is closed under small
limits. By definition, compactly generated $\infty$-categories are closed in
$\mathfrak{CAT}_{\infty}$ under cotensors with small simplicial sets. Hence,
the subcategory $\mathfrak{Pr}^{R}_{\omega}\subset\mathfrak{CAT}_{\infty}$ is
an $\infty$-cosmos, and the inclusion
$\mathfrak{Pr}^{R}_{\omega}\to\mathfrak{CAT}_{\infty}$ preserves the
structures of $\infty$-cosmoi and reflects equivalences.

######  Example 2.5.

The $\infty$-category $\mathbf{S}$ of small spaces is compactly generated. The
$\infty$-category $\mathbf{Cat}_{\infty}$ of small $\infty$-categories is
compactly generated, and the functor
$\mathrm{k}(\Delta^{n},{-}):\mathbf{Cat}_{\infty}\to\mathbf{S}$ sending an
$\infty$-category $\mathcal{C}$ to the space of $n$-cells of $\mathcal{C}$ is
an $\omega$-accessible right adjoint. This is because $\mathbf{Cat}_{\infty}$
is regarded as an $\omega$-accessible localization of
$\mathbf{Fun}(\Delta^{\mathrm{op}},\mathbf{S})$ using the equivalence of
quasicategories and complete Segal spaces [25].

######  Example 2.6.

For a small $\infty$-category $\mathcal{C}$, the $\infty$-category
$\mathbf{CartFib}_{\mathcal{C}}$ of cartesian fibrations over $\mathcal{C}$
and fibred functors over $\mathcal{C}$ is compactly generated as
$\mathbf{CartFib}_{\mathcal{C}}\simeq\mathbf{Fun}(\mathcal{C}^{\mathrm{op}},\mathbf{Cat}_{\infty})$.
The forgetful functor
$\mathbf{CartFib}_{\mathcal{C}}\to\mathbf{Cat}_{\infty}/\mathcal{C}$ is an
$\omega$-accessible right adjoint. To see this, observe that this forgetful
functor is the right derived functor of the forgetful functor

$\mathbf{SSet}^{+}/\mathcal{C}^{\sharp}\to\mathbf{SSet}/\mathcal{C}$

which is a right Quillen functor with respect to the cartesian model structure
and the slice model structure of the Joyal model structure on
$\mathbf{SSet}$[36, Proposition 3.1.5.2] or [37, Proposition 3.1.18]. The
functor $\mathbf{SSet}^{+}/\mathcal{C}^{\sharp}\to\mathbf{SSet}/\mathcal{C}$
preserves filtered colimits, and filtered colimits are homotopy colimits in
both model structures, from which it follows that the right derived functor
preserves filtered colimits.

######  Example 2.7.

We define a subcategory $\mathbf{LAdj}\subset\mathbf{Cat}_{\infty}^{\to}$ to
be the pullback

${\mathbf{LAdj}}$${\mathbf{CartFib}_{\Delta^{1}}}$${\mathbf{Cat}_{\infty}^{\to}}$${\mathbf{coCartFib}_{\Delta^{1}}}$${\mathbf{Cat}_{\infty}/\Delta^{1}.}$$\scriptstyle{\simeq}$

By construction, $\mathbf{LAdj}$ is compactly generated, and the forgetful
functor $\mathbf{LAdj}\to\mathbf{Cat}_{\infty}^{\to}$ is a conservative,
$\omega$-accessible right adjoint. Since a functor
$F:\mathcal{E}\to\Delta^{1}$ that is both a cocartesian fibration and a
cartesian fibration can be identified with an adjunction between the fibers
over $0$ and $1$, the $\infty$-category $\mathbf{LAdj}$ can be described as
follows:

  * •

the objects are the functors $F:\mathcal{C}\to\mathcal{D}$ that have a right
adjoint $F^{*}$;

  * •

the morphisms
$(F_{1}:\mathcal{C}_{1}\to\mathcal{D}_{1})\to(F_{2}:\mathcal{C}_{2}\to\mathcal{D}_{2})$
are the squares

${\mathcal{C}_{1}}$${\mathcal{C}_{2}}$${\mathcal{D}_{1}}$${\mathcal{D}_{2}}$$\scriptstyle{G}$$\scriptstyle{F_{1}}$$\scriptstyle{F_{2}}$$\scriptstyle{H}$

satisfying the Beck-Chevalley condition: the canonical natural transformation

${\mathcal{C}_{1}}$${\mathcal{C}_{2}}$${\mathcal{D}_{1}}$${\mathcal{D}_{2}}$$\scriptstyle{G}$$\scriptstyle{F_{1}^{*}}$$\scriptstyle{H}$$\scriptstyle{F_{2}^{*}}$

is invertible.

We use Example 2.7 to verify that an $\infty$-category whose objects are small
$\infty$-categories with a certain structure defined by adjunction is
compactly generated.

######  Example 2.8.

For a finitely presentable simplicial set $A$, we define
$\mathbf{Lex}_{\infty}^{(A)}$ to be the pullback

${\mathbf{Lex}_{\infty}^{(A)}}$${\mathbf{LAdj}}$${\mathbf{Cat}_{\infty}}$${\mathbf{Cat}_{\infty}^{\to}.}$$\scriptstyle{\mathcal{C}\mapsto(\delta:\mathcal{C}\to
A\pitchfork\mathcal{C})}$

$\mathbf{Lex}_{\infty}^{(A)}$ is the $\infty$-category of small
$\infty$-categories with limits of shape $A$. We define the $\infty$-category
$\mathbf{Lex}_{\infty}$ of small left exact $\infty$-categories to be the wide
pullback of $\mathbf{Lex}_{\infty}^{(A)}$ over $\mathbf{Cat}_{\infty}$ for all
finitely presentable simplicial sets $A$. By construction,
$\mathbf{Lex}_{\infty}^{(A)}$ and $\mathbf{Lex}_{\infty}$ are compactly
generated, and the forgetful functors to $\mathbf{Cat}_{\infty}$ are
conservative, $\omega$-accessible right adjoints.

We remark that codomain functors are always cartesian fibrations in
$\mathfrak{Pr}^{R}_{\omega}$.

######  Proposition 2.9.

For a compactly generated $\infty$-category $\mathcal{C}$, the functor
$\mathrm{cod}:\mathcal{C}^{\to}\to\mathcal{C}$ is a cartesian fibration in
$\mathfrak{Pr}^{R}_{\omega}$.

###### Proof.

Recall that finite limits commute with filtered colimits in any compactly
generated $\infty$-category $\mathcal{C}$. This implies that $\mathcal{C}$ is
finitely complete in the $\infty$-cosmos $\mathfrak{Pr}^{R}_{\omega}$ (that
is, the diagonal functor $\mathcal{C}\to A\pitchfork\mathcal{C}$ has a right
adjoint for every finitely presentable simplicial set $A$). Hence, the
codomain functor $\mathcal{C}^{\to}\to\mathcal{C}$ is a cartesian fibration. ∎

###  2.4 Exponentiable arrows

######  Definition 2.10.

An arrow $u:x\to y$ in a left exact $\infty$-category $\mathcal{C}$ is said to
be _exponentiable_ if the pullback functor
$u^{*}:\mathcal{C}/y\to\mathcal{C}/x$ has a right adjoint. If this is the
case, we refer to the right adjoint of $u^{*}$ as the _pushforward along $u$_
and denote it by $u_{*}:\mathcal{C}/x\to\mathcal{C}/y$.

######  Definition 2.11.

For an exponentiable arrow $u:x\to y$ in a left exact $\infty$-category
$\mathcal{C}$, the _associated polynomial functor_
$\mathbf{P}_{u}:\mathcal{C}\to\mathcal{C}$ is the composite

${\mathcal{C}}$${\mathcal{C}/x}$${\mathcal{C}/y}$${\mathcal{C}}$$\scriptstyle{x^{*}}$$\scriptstyle{u_{*}}$$\scriptstyle{y_{!}}$

where $x^{*}$ is the pullback along $x\to 1$ and $y_{!}$ is the forgetful
functor.

Recall that polynomials can be _composed_ [17, 50]: given two exponentiable
arrows $u_{1}:x_{1}\to y_{1}$ and $u_{2}:x_{2}\to y_{2}$, we have an
exponentiable arrow $u_{1}\otimes u_{2}$ such that $\mathbf{P}_{u_{1}\otimes
u_{2}}\simeq\mathbf{P}_{u_{1}}\circ\mathbf{P}_{u_{2}}$. We may also concretely
define $u_{1}\otimes u_{2}$ as follows: $\mathrm{cod}(u_{1}\otimes
u_{2})=\mathbf{P}_{u_{1}}y_{2}$; $\mathrm{dom}(u_{1}\otimes u_{2})$ is the
pullback

${\mathrm{dom}(u_{1}\otimes
u_{2})}$${x_{2}}$${\mathbf{P}_{u_{1}}y_{2}\times_{y_{1}}x_{1}}$${y_{2};}$$\scriptstyle{u_{2}}$$\scriptstyle{\mathrm{ev}}$

$u_{1}\otimes u_{2}$ is the composite $\mathrm{dom}(u_{1}\otimes
u_{2})\to\mathbf{P}_{u_{1}}y_{2}\times_{y_{1}}x_{1}\to\mathbf{P}_{u_{1}}y_{2}=\mathrm{cod}(u_{1}\otimes
u_{2})$.

###  2.5 Representable maps of right fibrations

We review the notion of a _representable map_ of right fibrations, which is a
generalization of a representable map of discrete fibrations over a
$1$-category. We think of a representable map of right fibrations as an
$\infty$-categorical analogue of a natural model of type theory [5] and a
category with families [15].

######  Definition 2.12.

We say a map $f:A\to B$ of right fibrations over an $\infty$-category
$\mathcal{C}$ is _representable_ if it has a right adjoint.

######  Proposition 2.13.

Let $\pi:A\to\mathcal{C}$ be a right fibration between $\infty$-categories. A
functor $f:B\to A$ is a right fibration if and only if the composite $\pi
f:B\to\mathcal{C}$ is. Consequently, we have a canonical equivalence of
$\infty$-categories

$\mathbf{RFib}_{\mathcal{C}}/A\simeq\mathbf{RFib}_{A}.$

###### Proof.

By definition. ∎

######  Corollary 2.14.

A representable map $f:A\to B$ of right fibrations over an $\infty$-category
$\mathcal{C}$ is exponentiable, and the pushforward along $f$ is given by the
pullback along the right adjoint $\delta:B\to A$ of $f$.

${\mathbf{RFib}_{\mathcal{C}}/A\simeq\mathbf{RFib}_{A}}$

$\dashv$

${\mathbf{RFib}_{B}\simeq\mathbf{RFib}_{\mathcal{C}}/B}$$\scriptstyle{\delta^{*}}$$\scriptstyle{f^{*}}$

######  Corollary 2.15.

Representable maps of right fibrations over an $\infty$-category $\mathcal{C}$
are stable under pullbacks: if

${A_{1}}$${A_{2}}$${B_{1}}$${B_{2}}$$\scriptstyle{g}$$\scriptstyle{f_{1}}$$\scriptstyle{f_{2}}$$\scriptstyle{h}$

is a pullback in $\mathbf{RFib}_{\mathcal{C}}$ and $f_{2}$ is representable,
then $f_{1}$ is representable. Moreover, if this is the case, the square
satisfies the Beck-Chevalley condition.

###### Proof.

By Proposition 2.13, the functor $h$ is a right fibration. Thus, the right
adjoint of $f_{2}$ lifts to a fibred right adjoint of $f_{1}$.

${A_{1}}$

$\dashv$

${B_{1}}$${A_{2}}$

$\dashv$

${B_{2}}$$\scriptstyle{f_{1}}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{f_{2}}$

∎

######  Proposition 2.16.

A map $f:A\to B$ of right fibrations over an $\infty$-category $\mathcal{C}$
is representable if and only if, for any section $b:\mathcal{C}/y\to B$, the
pullback $b^{*}A$ is a representable right fibration over $\mathcal{C}$.

###### Proof.

For a section $b:\mathcal{C}/y\to B$, an arrow $u:fa\to b$ in $B$ for some
$a\in A$ corresponds to a square

${\mathcal{C}/x}$${A}$${\mathcal{C}/y}$${B.}$$\scriptstyle{a}$$\scriptstyle{u}$$\scriptstyle{f}$$\scriptstyle{b}$
(1)

$(a,u)$ is a universal arrow from $f$ to $b$ if and only if Eq. 1 is a
pullback. ∎

##  3 $\infty$-type theories

We introduce notions of an _$\infty$ -type theory_, a _theory_ over an
$\infty$-type theory and a _model_ of an $\infty$-type theory, translating the
previous work of the second author [46] into the language of
$\infty$-categories. The idea is to extend the functorial semantics of
algebraic theories [31]. Algebraic theories are identified with categories
with finite products, and models of an algebraic theory are identified with
functors into the category of sets preserving finite products. For type
theories, it is natural to identify models of a type theory with functors into
presheaf categories, because (extensions of) natural models [5] and categories
with families [15] are diagrams in presheaf categories. Since representable
maps of presheaves play a special role in the natural model semantics, some
arrows in the source category should be specified to be sent to representable
maps. This motivates the following definitions.

######  Definition 3.1.

An _$\infty$ -category with representable maps_ is a pair $(\mathcal{C},R)$
where $\mathcal{C}$ is an $\infty$-category and $R\subseteq
k(\Delta^{1},\mathcal{C})$ is a subspace of the space of arrows of
$\mathcal{C}$ satisfying the conditions below. Arrows in $R$ are called
_representable arrows_.

  1. 1.

$\mathcal{C}$ has finite limits.

  2. 2.

All the identities are representable and representable arrows are closed under
composition.

  3. 3.

Representable arrows are stable under pullbacks.

  4. 4.

Representable arrows are exponentiable.

A _morphism of $\infty$-categories with representable maps_ is a functor
preserving representable arrows, finite limits and pushforwards along
representable arrows.

######  Example 3.2.

For a small $\infty$-category $\mathcal{C}$, the $\infty$-category
$\mathbf{RFib}_{\mathcal{C}}$ of small right fibrations over $\mathcal{C}$ is
an $\infty$-category with representable maps in which a map is representable
if it has a right adjoint.

######  Definition 3.3.

An _$\infty$ -type theory_ is an $\infty$-category with representable maps
whose underlying $\infty$-category is small. A _morphism of $\infty$-type
theories_ is a morphism of $\infty$-categories with representable maps. By an
_$n$ -type theory_ for $1\leq n<\infty$, we mean an $\infty$-type theory whose
underlying $\infty$-category is an $n$-category.

######  Example 3.4.

The type theories in the sense of the previous work [46] are the $1$-type
theories.

######  Definition 3.5.

Let $\mathbb{T}$ be an $\infty$-type theory.

  * •

A _model of $\mathbb{T}$_ consists of an $\infty$-category
$\mathcal{M}({\star})$ with a terminal object and a morphism of
$\infty$-categories with representable maps
$\mathcal{M}:\mathbb{T}\to\mathbf{RFib}_{\mathcal{M}({\star})}$.

  * •

A _theory over $\mathbb{T}$_ or a _$\mathbb{T}$ -theory_ is a left exact
functor $K:\mathbb{T}\to\mathbf{S}$.

######  Example 3.6.

We will construct in Section 3.1 a presentable $\infty$-category
$\mathbf{TT}_{\infty}$ of $\infty$-type theories and their morphisms, so we
have various _free constructions_ of $\infty$-type theories. For example,
there is an $\infty$-type theory $\mathbb{G}_{\infty}$ freely generated by one
representable arrow $\partial:E\to U$. Indeed, the functor
$\mathbf{TT}_{\infty}\to\mathbf{S}$ that sends an $\infty$-type theory
$\mathbb{T}$ to the space of representable arrows in $\mathbb{T}$ preserves
limits and filtered colimits, and thus it is representable by presentability.
The universal property of $\mathbb{G}_{\infty}$ asserts that a morphism
$\mathbb{G}_{\infty}\to\mathcal{C}$ of $\infty$-categories with representable
maps is completely determined by the image of the representable arrow
$\partial\in\mathbb{G}_{\infty}$. Thus, a model of $\mathbb{G}_{\infty}$
consists of the following data:

  * •

an $\infty$-category $\mathcal{M}({\star})$ with a terminal objects;

  * •

a representable map $\mathcal{M}(\partial):\mathcal{M}(E)\to\mathcal{M}(U)$ of
right fibrations over $\mathcal{M}({\star})$.

In other words, a model of $\mathbb{G}_{\infty}$ is an $\infty$-categorical
analogue of a natural model [5, 16]. One may think of an object
$\Gamma\in\mathcal{M}({\star})$ as a context, a section
$A:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(U)$ as a type over $\Gamma$, and
a section $a:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(E)$ as a term over
$\Gamma$. The representability of $\mathcal{M}(\partial)$ is used for modeling
context comprehension: for a section
$A:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(U)$, the representing object for
$A^{*}\mathcal{M}(E)$ is though of as the context $(\Gamma,x:A)$ with $x$ a
fresh variable.

It is not simple to describe a $\mathbb{G}_{\infty}$-theory, but we could say
that the $\infty$-category of $\mathbb{G}_{\infty}$-theories is an
$\infty$-analogue of the category of generalized algebraic theories [11].
Indeed, the second named author showed in [47] that the category of
generalized algebraic theories is equivalent to the category of left exact
functors $\mathbb{G}\to\mathbf{Set}$ where $\mathbb{G}$ is the left exact
category freely generated by an exponentiable arrow.

In Sections 3.1, 3.2 and 3.3 below, we will construct an $\infty$-category
$\mathbf{TT}_{\infty}$ of $\infty$-type theories, an $\infty$-category
$\mathbf{Th}(\mathbb{T})$ of $\mathbb{T}$-theories and an $\infty$-category
$\mathbf{Mod}(\mathbb{T})$ of models of $\mathbb{T}$. These
$\infty$-categories are constructed inside the $\infty$-cosmos
$\mathfrak{Pr}^{R}_{\omega}$ of compactly generated $\infty$-categories and
$\omega$-accessible right adjoints. In Section 3.4 we give a universal
property of $\mathbf{Mod}(\mathbb{T})$ as an object of
$\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}$ from which for
example it follows that the assignment
$\mathbb{T}\mapsto\mathbf{Mod}(\mathbb{T})$ takes colimits to limits. In
Section 3.5 we see that a slice of the underlying $\infty$-category of an
$\infty$-type theory is naturally equipped with a structure of $\infty$-type
theory and has a useful universal property.

###  3.1 The $\infty$-category of $\infty$-type theories

We construct an $\infty$-category $\mathbf{TT}_{\infty}$ of $\infty$-type
theories and their morphisms.

######  Definition 3.7.

Let $\mathbf{Cat}^{+}_{\infty}$ be the pullback

${\mathbf{Cat}^{+}_{\infty}}$${(\mathbf{S}^{\to})_{\leq-1}}$${\mathbf{Cat}_{\infty}}$${\mathbf{S}}$$\scriptstyle{\mathrm{cod}}$$\scriptstyle{\mathrm{k}(\Delta^{1},{-})}$

where $(\mathbf{S}^{\to})_{\leq-1}$ denotes the full subcategory of
$\mathbf{S}^{\to}$ spanned by the $(-1)$-truncated maps of spaces which is an
$\omega$-accessible localization of $\mathbf{S}^{\to}$.
$\mathbf{Cat}^{+}_{\infty}$ is the $\infty$-category of small
$\infty$-categories equipped with a subspace of arrows. We define
$\mathbf{Lex}^{+}_{\infty}$ to be the full subcategory of
$\mathbf{Lex}_{\infty}\times_{\mathbf{Cat}_{\infty}}\mathbf{Cat}^{+}_{\infty}$
spanned by the left exact $\infty$-categories with a class of arrows closed
under composition and stable under pullbacks.

The inclusion
$\mathbf{Lex}^{+}_{\infty}\to\mathbf{Lex}_{\infty}\times_{\mathbf{Cat}_{\infty}}\mathbf{Cat}^{+}_{\infty}$
has a left adjoint by taking the closure of the specified subspace of arrows
under composition and pullbacks, and $\mathbf{Lex}^{+}_{\infty}$ is closed in
$\mathbf{Lex}_{\infty}\times_{\mathbf{Cat}_{\infty}}\mathbf{Cat}^{+}_{\infty}$
under filtered colimits. Hence, $\mathbf{Lex}^{+}_{\infty}$ is compactly
generated, and the inclusion
$\mathbf{Lex}^{+}_{\infty}\to\mathbf{Lex}_{\infty}\times_{\mathbf{Cat}_{\infty}}\mathbf{Cat}_{\infty}^{+}$
is an $\omega$-accessible right adjoint.

Let $(\mathcal{C},R)$ be an object of $\mathbf{Lex}_{\infty}^{+}$. Since
$\mathcal{C}$ has finite limits, we have a functor $\theta(\mathcal{C},R)$
between isofibrations over $R$ whose fiber over $(u:x\to y)\in R$ is the
pullback functor $u^{*}:\mathcal{C}/y\to\mathcal{C}/x$. An $\infty$-type
theory is nothing but an object $(\mathcal{C},R)$ of
$\mathbf{Lex}_{\infty}^{+}$ such that $\theta(\mathcal{C},R)$ has a fiberwise
right adjoint. We show that this condition is equivalent to the condition that
the functor has a right adjoint.

######  Proposition 3.8.

Let

${\mathcal{C}}$${\mathcal{D}}$${A}$$\scriptstyle{F}$

be a functor between isofibrations in $\mathfrak{CAT}_{\infty}$ such that $A$
is an $\infty$-groupoid. The following are equivalent:

  1. 1.

the functor $F:\mathcal{C}\to\mathcal{D}$ has a right adjoint;

  2. 2.

for every point $a\in A$, the functor between fibers
$F_{a}:\mathcal{C}_{a}\to\mathcal{D}_{a}$ has a right adjoint.

###### Proof.

Suppose that each $F_{a}:\mathcal{C}_{a}\to\mathcal{D}_{a}$ has a right
adjoint $G_{a}$ with counit $\varepsilon_{a,y}:F_{a}(G_{a}(y))\to y$. It
suffices to see that $\varepsilon_{a,y}$ is universal in $\mathcal{D}$. Let
$x\in\mathcal{C}_{a^{\prime}}$ be an object in another fiber and consider the
induced map

$\mathcal{C}(x,G_{a}(y))\to\mathcal{D}(F_{a^{\prime}}(x),y).$

This is a map over $A(a^{\prime},a)$, and thus it suffices to show that this
is fiberwise an equivalence. Since $A$ is an $\infty$-groupoid and since
$\mathcal{C}\to A$ and $\mathcal{D}\to A$ are isofibrations, the fibers over
$p\in A(a^{\prime},a)$ are equivalent to the fibers over $\mathrm{id}\in
A(a,a)$, but the map between the fibers over $\mathrm{id}$ is the equivalence
$\mathcal{C}_{a}(x,G_{a}(y))\simeq\mathcal{D}_{a}(G_{a}(x),y)$.

Suppose that $F$ has a right adjoint $G:\mathcal{D}\to\mathcal{C}$ with counit
$\varepsilon:FG\Rightarrow\mathrm{id}$. Since $A$ is an $\infty$-groupoid, the
natural transformation

${\mathcal{D}}$${\mathcal{C}}$${\mathcal{D}}$${A}$$\scriptstyle{G}$$\scriptstyle{F}$$\scriptstyle{\varepsilon}$

is invertible. Then, since $\mathcal{C}\to A$ and $\mathcal{D}\to A$ are
isofibrations, one can replace $G$ and $\varepsilon$ by a functor
$G^{\prime}:\mathcal{D}\to\mathcal{C}$ and a natural transformation
$\varepsilon^{\prime}:FG^{\prime}\Rightarrow\mathrm{id}$, respectively, over
$A$. Then $G^{\prime}$ and $\varepsilon^{\prime}$ give a fiberwise right
adjoint of $F$. ∎

######  Remark 3.9.

The proposition also holds more generally when $A$ is an $\infty$-category.
See [35, Proposition 7.3.2.1].

The functor $\theta(\mathcal{C},R)$ is constructed as follows. Since
$\mathcal{C}$ has finite limits, the functor
$(\Delta^{1}\times\Delta^{1})\pitchfork\mathcal{C}\to\Lambda^{2}_{2}\pitchfork\mathcal{C}$
sending a square to its bottom and right edges has a right adjoint. Composing
the right adjoint and the functor
$(\Delta^{1}\times\Delta^{1})\pitchfork\mathcal{C}\to\Lambda^{2}_{1}\pitchfork\mathcal{C}$
sending a square to its bottom and left edges, we have a functor

$\theta^{\prime}:\Lambda^{2}_{2}\pitchfork\mathcal{C}\to\Lambda^{2}_{1}\pitchfork\mathcal{C}$

over $\Delta^{\\{1,2\\}}\pitchfork\mathcal{C}$. The functor
$\theta(\mathcal{C},R)$ is then the pullback of $\theta^{\prime}$ along the
inclusion $R\to\Delta^{\\{1,2\\}}\pitchfork\mathcal{C}$. This construction is
functorial and preserves limits and filtered colimits, yielding a functor
$\theta:\mathbf{Lex}_{\infty}^{+}\to\Delta^{2}\pitchfork\mathbf{Cat}_{\infty}$
in $\mathfrak{Pr}^{R}_{\omega}$.

######  Definition 3.10.

We define $\mathbf{TT}_{\infty}$ to be the pullback

${\mathbf{TT}_{\infty}}$${\mathbf{LAdj}}$${\mathbf{Lex}_{\infty}^{+}}$${\Delta^{2}\pitchfork\mathbf{Cat}_{\infty}}$${\Delta^{\\{0,1\\}}\pitchfork\mathbf{Cat}_{\infty}.}$$\scriptstyle{\theta}$

By Proposition 3.8, the objects of $\mathbf{TT}_{\infty}$ are precisely the
$\infty$-type theories. It is also straightforward to see that the morphisms
of $\mathbf{TT}_{\infty}$ are precisely the morphisms of $\infty$-type
theories.

###  3.2 The $\infty$-category of theories over an $\infty$-type theory

######  Definition 3.11.

For an $\infty$-type theory $\mathbb{T}$, we define $\mathbf{Th}(\mathbb{T})$
to be the full subcategory of $\mathbf{Fun}(\mathbb{T},\mathbf{S})$ spanned by
the functors preserving finite limits.

By definition, $\mathbf{Th}(\mathbb{T})$ is compactly generated, and the
inclusion $\mathbf{Th}(\mathbb{T})\to\mathbf{Fun}(\mathbb{T},\mathbf{S})$ is
an $\omega$-accessible right adjoint. The $\infty$-category
$\mathbf{Th}(\mathbb{T})$ has the following alternative definitions:

  * •

$\mathbf{Th}(\mathbb{T})$ is the cocompletion of $\mathbb{T}^{\mathrm{op}}$
under filtered colimits;

  * •

$\mathbf{Th}(\mathbb{T})$ is the $\omega$-free cocompletion of
$\mathbb{T}^{\mathrm{op}}$, that is, the initial cocomplete $\infty$-category
equipped with a functor from $\mathbb{T}^{\mathrm{op}}$ preserving finite
colimits.

###  3.3 The $\infty$-category of models of an $\infty$-type theory

We construct an $\infty$-category $\mathbf{Mod}(\mathbb{T})$ of models of an
$\infty$-type theory $\mathbb{T}$. The following description of
$\mathbf{Mod}(\mathbb{T})$ is based on unpublished work by John Bourke and the
second named author on the $2$-category of $1$-models of a $1$-type theory.

Let $\mathbb{T}$ be an $\infty$-type theory. Recall that a functor to a slice
$\infty$-category $F^{\prime}:\mathcal{C}\to\mathcal{D}/y$ corresponds to a
functor $F:\mathcal{C}^{\triangleright}\to\mathcal{D}$ that sends
${\star}\in\mathcal{C}^{\triangleright}$ to $y$. Then a model $\mathcal{M}$ of
$\mathbb{T}$ can be regarded as a functor
$\mathcal{M}:\mathbb{T}^{\triangleright}\to\mathbf{Cat}_{\infty}$ satisfying
the following conditions:

  1. 1.

$\mathcal{M}({\star})$ has a terminal object;

  2. 2.

for every object $x\in\mathbb{T}$, the functor
$\mathcal{M}(x)\to\mathcal{M}({\star})$ is a right fibration;

  3. 3.

for every finite diagram $x:A\to\mathbb{T}$, the canonical functor
$\mathcal{M}(\lim_{A}x)\to\lim_{A^{\triangleright}}\mathcal{M}x^{\triangleright}$
is an equivalence;

  4. 4.

for every representable arrow $u:x\to y$ in $\mathbb{T}$, the functor
$\mathcal{M}(u):\mathcal{M}(x)\to\mathcal{M}(y)$ has a right adjoint
$\delta_{u}:\mathcal{M}(y)\to\mathcal{M}(x)$;

  5. 5.

for every pair of arrows $u:x\to y$ and $v:y\to z$ with $v$ representable, the
canonical functor $\mathcal{M}(v_{*}x)\to\delta_{v}^{*}\mathcal{M}(x)$ is an
equivalence (recall that the pushforward along $\mathcal{M}(v)$ in
$\mathbf{RFib}_{\mathcal{M}({\star})}$ is given by the pullback along
$\delta_{v}$).

From this description, we will define $\mathbf{Mod}(\mathbb{T})$ as a
subcategory of
$\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$.

######  Definition 3.12.

We define $\mathbf{Mod}_{\lx@cref{refnum}{item:3}}(\mathbb{T})$ to be the
pullback

${\mathbf{Mod}_{\lx@cref{refnum}{item:3}}(\mathbb{T})}$${\mathbf{Lex}_{\infty}^{(\emptyset)}}$${\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})}$${\mathbf{Cat}_{\infty}.}$$\scriptstyle{\mathrm{ev}_{{\star}}}$

######  Definition 3.13.

For an object $x\in\mathbb{T}$, we define
$\mathbf{Mod}_{\lx@cref{refnum}{item:4}}^{x}(\mathbb{T})$ to be the pullback

${\mathbf{Mod}_{\lx@cref{refnum}{item:4}}^{x}(\mathbb{T})}$${\mathbf{RFib}}$${\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})}$${\mathbf{Cat}_{\infty}^{\to}}$$\scriptstyle{\mathrm{ev}_{(x\to{*})}}$

and $\mathbf{Mod}_{\lx@cref{refnum}{item:4}}(\mathbb{T})$ to be the wide
pullback of $\mathbf{Mod}_{\lx@cref{refnum}{item:4}}^{x}(\mathbb{T})$ over
$\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$ for all
objects $x\in\mathbb{T}$.

######  Definition 3.14.

For a finite diagram $x:A\to\mathbb{T}$, we define
$\mathbf{Mod}_{\lx@cref{refnum}{item:5}}^{(A,x)}(\mathbb{T})$ to be the
pullback

${\mathbf{Mod}_{\lx@cref{refnum}{item:5}}^{(A,x)}(\mathbb{T})}$${\mathbf{Cat}_{\infty}^{\simeq}}$${\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})}$${\mathbf{Cat}_{\infty}^{\to}}$$\scriptstyle{(\mathrm{ev}_{\lim_{A}x}\Rightarrow\lim_{A^{\triangleright}}\mathrm{ev}_{x^{\triangleright}})}$

and $\mathbf{Mod}_{\lx@cref{refnum}{item:5}}(\mathbb{T})$ to be the wide
pullback of $\mathbf{Mod}_{\lx@cref{refnum}{item:5}}^{(A,x)}(\mathbb{T})$ over
$\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$ for all
finite diagrams $(A,x:A\to\mathbb{T})$.

######  Definition 3.15.

For a representable arrow $u:x\to y$ in $\mathbb{T}$, we define
$\mathbf{Mod}_{\lx@cref{refnum}{item:6}}^{u}(\mathbb{T})$ to be the pullback

${\mathbf{Mod}_{\lx@cref{refnum}{item:6}}^{u}(\mathbb{T})}$${\mathbf{LAdj}}$${\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})}$${\mathbf{Cat}_{\infty}^{\to}}$$\scriptstyle{\mathrm{ev}_{u}}$

and $\mathbf{Mod}_{\lx@cref{refnum}{item:6}}(\mathbb{T})$ to be the wide
pullback of $\mathbf{Mod}_{\lx@cref{refnum}{item:6}}^{u}(\mathbb{T})$ over
$\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$ for all
representable arrows $u$ in $\mathbb{T}$.

######  Definition 3.16.

We denote by $\mathbf{Mod}_{-\lx@cref{refnum}{item:7}}(\mathbb{T})$ the wide
pullback of $\mathbf{Mod}_{\lx@cref{refnum}{item:3}}(\mathbb{T})$,
$\mathbf{Mod}_{\lx@cref{refnum}{item:4}}(\mathbb{T})$,
$\mathbf{Mod}_{\lx@cref{refnum}{item:5}}(\mathbb{T})$ and
$\mathbf{Mod}_{\lx@cref{refnum}{item:6}}(\mathbb{T})$ over
$\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$. By
construction, $\mathbf{Mod}_{-\lx@cref{refnum}{item:7}}(\mathbb{T})$ is the
$\infty$-category of functors
$\mathcal{M}:\mathbb{T}^{\triangleright}\to\mathbf{Cat}_{\infty}$ satisfying
Items 1, 2, 3 and 4.

######  Definition 3.17.

For a pair of composable arrows $u:x\to y$ and $v:y\to z$ in $\mathbb{T}$ with
$v$ representable, we define
$\mathbf{Mod}_{\lx@cref{refnum}{item:7}}^{(u,v)}(\mathbb{T})$ to be the
pullback

${\mathbf{Mod}_{\lx@cref{refnum}{item:7}}^{(u,v)}(\mathbb{T})}$${\mathbf{Cat}_{\infty}^{\simeq}}$${\mathbf{Mod}_{-\lx@cref{refnum}{item:7}}(\mathbb{T})}$${\mathbf{Cat}_{\infty}^{\to}}$$\scriptstyle{(\mathrm{ev}_{v_{*}x}\Rightarrow\delta_{v}^{*}\mathrm{ev}_{x})}$

and $\mathbf{Mod}(\mathbb{T})$ to be the wide pullback of
$\mathbf{Mod}_{\lx@cref{refnum}{item:7}}^{(u,v)}(\mathbb{T})$ over
$\mathbf{Mod}_{-\lx@cref{refnum}{item:7}}(\mathbb{T})$ for all pairs $(u,v)$
of composable arrows in $\mathbb{T}$ with $v$ representable.

By construction, the $\infty$-category $\mathbf{Mod}(\mathbb{T})$ is compactly
generated, and the forgetful functor
$\mathbf{Mod}(\mathbb{T})\to\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$
is a conservative, $\omega$-accessible right adjoint. Moreover, the objects of
$\mathbf{Mod}(\mathbb{T})$ are the models of $\mathbb{T}$ and the morphisms in
$\mathbf{Mod}(\mathbb{T})$ are described as follows. Let $\mathcal{M}$ and
$\mathcal{N}$ be models of $\mathbb{T}$ and
$F:\mathcal{M}\Rightarrow\mathcal{N}:\mathbb{T}^{\triangleright}\to\mathbf{Cat}_{\infty}$
be a natural transformation. Then $F$ is in $\mathbf{Mod}(\mathbb{T})$ if and
only if the following conditions hold:

  * •

the component $F({\star}):\mathcal{M}({\star})\to\mathcal{N}({\star})$
preserves terminal objects;

  * •

for any representable arrow $u:x\to y$ in $\mathbb{T}$, the square

${\mathcal{M}(x)}$${\mathcal{N}(x)}$${\mathcal{M}(y)}$${\mathcal{N}(y)}$$\scriptstyle{F(x)}$$\scriptstyle{\mathcal{M}(u)}$$\scriptstyle{\mathcal{N}(u)}$$\scriptstyle{F(y)}$

satisfies the Beck-Chevalley condition.

###  3.4 Universal property of $\mathbf{Mod}(\mathbb{T})$

We give a universal property of $\mathbf{Mod}(\mathbb{T})$ seen as an object
of $\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}$. A consequence
is that the assignment $\mathbb{T}\mapsto\mathbf{Mod}(\mathbb{T})$ takes
colimits of $\infty$-type theories to limits of $\infty$-categories over
$\mathbf{Lex}_{\infty}^{(\emptyset)}$ (Corollary 3.23).

######  Definition 3.18.

For a functor $\mathcal{C}:\mathcal{I}\to\mathbf{Cat}_{\infty}$, we denote by
$\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$ the full subcategory
of $\mathbf{Fun}(\mathcal{I},\mathbf{Cat}_{\infty})/\mathcal{C}$ spanned by
the natural transformations
$\pi:A\Rightarrow\mathcal{C}:\mathcal{I}\to\mathbf{Cat}_{\infty}$ whose
components are right fibrations. In other words,
$\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$ is the fiber of the
functor
$\mathbf{Fun}(\mathcal{I},\mathrm{cod}):\mathbf{Fun}(\mathcal{I},\mathbf{RFib})\to\mathbf{Fun}(\mathcal{I},\mathbf{Cat}_{\infty})$
over the object
$\mathcal{C}\in\mathbf{Fun}(\mathcal{I},\mathbf{Cat}_{\infty})$. We say a map
$f:A\to B$ in $\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$ is
_representable_ if every component $f(i):A(i)\to B(i)$ is a representable map
of right fibrations over $\mathcal{C}(i)$ and if every naturality square

${A(i)}$${A(j)}$${B(i)}$${B(j)}$$\scriptstyle{A(\alpha)}$$\scriptstyle{f(i)}$$\scriptstyle{f(j)}$$\scriptstyle{B(\alpha)}$

satisfies the Beck-Chevalley condition.

######  Proposition 3.19.

Representable maps in $\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$
are closed under composition and stable under pullbacks.

###### Proof.

Let

${A_{1}}$${A_{2}}$${B_{1}}$${B_{2}}$$\scriptstyle{g}$$\scriptstyle{f_{1}}$$\scriptstyle{f_{2}}$$\scriptstyle{h}$

be a pullback in $\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$ and
suppose that $f_{2}$ is representable. By Corollary 2.15, every
$f_{1}(i):A_{1}(i)\to B_{1}(i)$ is a representable map of right fibrations
over $\mathcal{C}(i)$, and the square

${A_{1}(i)}$${A_{2}(i)}$${B_{1}(i)}$${B_{2}(i)}$$\scriptstyle{g(i)}$$\scriptstyle{f_{1}(i)}$$\scriptstyle{f_{2}(i)}$$\scriptstyle{h(i)}$

satisfies the Beck-Chevalley condition. It remains to show that, for any arrow
$\alpha:i\to j$ in $\mathcal{I}$, the square

${A_{1}(i)}$${A_{1}(j)}$${B_{1}(i)}$${B_{1}(j)}$$\scriptstyle{A_{1}(\alpha)}$$\scriptstyle{f_{1}(i)}$$\scriptstyle{f_{1}(j)}$$\scriptstyle{B_{1}(\alpha)}$

satisfies the Beck-Chevalley condition. Since a map of right fibrations over a
fixed base is conservative, it suffices to show that the composite of squares

${A_{1}(i)}$${A_{1}(j)}$${A_{2}(j)}$${B_{1}(i)}$${B_{1}(j)}$${B_{2}(j)}$$\scriptstyle{A_{1}(\alpha)}$$\scriptstyle{f_{1}(i)}$$\scriptstyle{g(j)}$$\scriptstyle{f_{1}(j)}$$\scriptstyle{f_{2}(j)}$$\scriptstyle{B_{1}(\alpha)}$$\scriptstyle{h(j)}$

satisfies the Beck-Chevalley condition, but this is true by the Beck-Chevalley
condition for $f_{2}$. ∎

######  Proposition 3.20.

A representable map in $\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$
is exponentiable, and the pushforward is given by the pullback along the right
adjoint.

###### Proof.

The same as Corollary 2.14. ∎

######  Proposition 3.21.

For a functor $\mathcal{C}:\mathcal{I}\to\mathbf{Cat}_{\infty}$, the
$\infty$-category $\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$
together with the class of representable maps is an $\infty$-category with
representable maps. For a functor $F:\mathcal{I}^{\prime}\to\mathcal{I}$, the
functor
$F^{*}:\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}\to\mathbf{Fun}(\mathcal{I}^{\prime},\mathbf{RFib})_{\mathcal{C}F}$
defined by the precomposition of $F$ is a morphism of $\infty$-categories with
representable maps.

###### Proof.

By definition. ∎

Let $\mathbb{T}$ be an $\infty$-type theory and
$\mathcal{C}:\mathcal{I}\to\mathbf{Lex}_{\infty}^{(\emptyset)}$ a functor. We
have equivalences

$\displaystyle\quad\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}((\mathcal{I},\mathcal{C}),(\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty}),\mathrm{ev}_{{\star}}))$
$\displaystyle\simeq$ {transposition}
$\displaystyle\quad\\{{\star}\\}/\mathbf{CAT}_{\infty}((\mathbb{T}^{\triangleright},\\{{\star}\\}),(\mathbf{Fun}(\mathcal{I},\mathbf{Cat}_{\infty}),\mathcal{C}))$
$\displaystyle\simeq$ {adjunction of join and slice}
$\displaystyle\quad\mathbf{CAT}_{\infty}(\mathbb{T},\mathbf{Fun}(\mathcal{I},\mathbf{Cat}_{\infty})/\mathcal{C}).$

######  Proposition 3.22.

Let $\mathbb{T}$ be an $\infty$-type theory and
$\mathcal{C}:\mathcal{I}\to\mathbf{Lex}_{\infty}^{(\emptyset)}$ a functor. A
functor
$F:\mathcal{I}\to\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$
over $\mathbf{Lex}_{\infty}^{(\emptyset)}$ factors through
$\mathbf{Mod}(\mathbb{T})$ if and only if its transpose
$\widetilde{F}:\mathbb{T}\to\mathbf{Fun}(\mathcal{I},\mathbf{Cat}_{\infty})/\mathcal{C}$
factors through $\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}$ and is
a morphism of $\infty$-categories with representable maps. Consequently, we
have an equivalence

$\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}((\mathcal{I},\mathcal{C}),(\mathbf{Mod}(\mathbb{T}),\mathrm{ev}_{{\star}}))\simeq\mathbf{REP}_{\infty}(\mathbb{T},\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}}).$

###### Proof.

Immediate from the definition of models of $\mathbb{T}$. ∎

######  Corollary 3.23.

$\mathbf{Mod}:\mathbf{TT}_{\infty}^{\mathrm{op}}\to\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}$
preserves limits.

###  3.5 Slice $\infty$-type theories

######  Definition 3.24.

For an $\infty$-category with representable maps $\mathcal{C}$ and an object
$x\in\mathcal{C}$, we regard the slice $\mathcal{C}/x$ as an $\infty$-category
with representable maps in which an arrow is representable if it is
representable in $\mathcal{C}$.

The goal of this subsection is to show that $\mathcal{C}/x$ is the
$\infty$-category with representable maps obtained from $\mathcal{C}$ by
freely adjoining a global section of $x$ (Proposition 3.27). We first recall a
universal property of a slice of a left exact $\infty$-category.

######  Proposition 3.25.

Let $\mathcal{C}$ be a left exact $\infty$-category and $x\in\mathcal{C}$ an
object. We denote by $x^{*}:\mathcal{C}\to\mathcal{C}/x$ the pullback functor
along $x\to 1$ and $\delta_{x}:1\to x^{*}x$ the arrow in $\mathcal{C}/x$ which
is the diagonal arrow $x\to x\times x$ in $\mathcal{C}$. For a left exact
$\infty$-category $\mathcal{D}$ and a left exact functor
$F:\mathcal{C}\to\mathcal{D}$, the map

$\mathcal{C}/\mathbf{LEX}_{\infty}(\mathcal{C}/x,\mathcal{D})\ni G\mapsto
G(\delta_{x})\in\mathcal{D}(1,Fx)$ (2)

is an equivalence of spaces.

###### Proof.

An object of $\mathcal{C}/\mathbf{LEX}_{\infty}(\mathcal{C}/x,\mathcal{D})$ is
a left exact functor $G:\mathcal{C}/x\to\mathcal{D}$ equipped with an
invertible natural transformation $\sigma:G\circ x^{*}\Rightarrow F$. By the
adjunction $x_{!}\dashv x^{*}$, such a natural transformation $\sigma$
corresponds to a natural transformation $\widetilde{\sigma}:G\Rightarrow
F\circ x_{!}$. One can check that $\sigma:G\circ x^{*}\Rightarrow F$ is
invertible if and only if $\widetilde{\sigma}:G\Rightarrow F\circ x_{!}$ is a
cartesian natural transformation, that is, any naturality square is a
pullback. Therefore, the statement is equivalent to that, given a global
section $u:1\to Fx$, the space of pairs $(G,\sigma)$ consisting of a left
exact functor $G:\mathcal{C}/x\to\mathcal{D}$ and a cartesian natural
transformation $\sigma:G\Rightarrow F\circ x_{!}$ extending $u$ is
contractible.

Since $\mathcal{D}$ has finite limits, the evaluation at the terminal object
of $\mathcal{C}/x$ defines a cartesian fibration
$\mathbf{Fun}(\mathcal{C}/x,\mathcal{D})\to\mathcal{D}$ in which a natural
transformation $\sigma:G_{1}\Rightarrow G_{2}$ is cartesian if and only if the
naturality square

${G_{1}y}$${G_{2}y}$${G_{1}1}$${G_{2}1}$$\scriptstyle{\sigma}$$\scriptstyle{\sigma}$

is a pullback for any object $y\in\mathcal{C}/x$, which is equivalent to that
$\sigma$ is a cartesian natural transformation. Therefore, given a functor
$G_{2}:\mathcal{C}/x\to\mathcal{D}$ and an arrow $u:x^{\prime}\to G_{2}1$, the
space of pairs $(G_{1},\sigma)$ consisting of a functor
$G_{1}:\mathcal{C}/x\to\mathcal{D}$ and a cartesian natural transformation
$\sigma$ extending $u$ is contractible. When $G_{2}=F\circ x_{!}$, the functor
$G_{1}$ must preserve pullbacks since $G_{2}$ does. If, in addition,
$x^{\prime}\simeq 1$, then $G_{1}$ preserves terminal objects, and thus it is
left exact. We conclude that, given an arrow $u:1\to Fx\simeq F(x_{!}1)$, the
space of pairs $(G,\sigma)$ consisting of a left exact functor
$G:\mathcal{C}/x\to\mathcal{D}$ and a cartesian natural transformation
$\sigma:G\Rightarrow F\circ x_{!}$ extending $u$ is contractible, as we have a
unique cartesian lift $G\Rightarrow F\circ x_{!}$ and $G$ must be left exact.
∎

From this proof, we can extract the inverse of the map 2: it is given by

$\mathcal{D}(1,Fx)\ni u\mapsto u^{*}\circ
F/x\in\mathcal{C}/\mathbf{LEX}_{\infty}(\mathcal{C}/x,\mathcal{D})$

where $F/x:\mathcal{C}/x\to\mathcal{D}/Fx$ is the functor induced by $F$.

######  Definition 3.26.

We denote by $\mathbf{REP}_{\infty}$ the $\infty$-category of large
$\infty$-categories with representable maps and their morphisms.

######  Proposition 3.27.

Let $\mathcal{C}$ be an $\infty$-category with representable maps and
$x\in\mathcal{C}$ an object.

  1. 1.

The functor $x^{*}:\mathcal{C}\to\mathcal{C}/x$ is a morphism of
$\infty$-categories with representable maps.

  2. 2.

For an $\infty$-category with representable maps $\mathcal{D}$ and a morphism
$F:\mathcal{C}\to\mathcal{D}$, the map

$\mathcal{C}/\mathbf{REP}_{\infty}(\mathcal{C}/x,\mathcal{D})\ni G\mapsto
G(\delta_{x})\in\mathcal{D}(1,Fx)$

is an equivalence of spaces.

###### Proof.

Item 1 is because pullbacks preserve all limits and all pushforwards. Item 2
follows from Proposition 3.25, because $u^{*}\circ
F/x:\mathcal{C}/x\to\mathcal{D}$ is a morphism of $\infty$-categories with
representable maps for every global section $u:1\to Fx$. ∎

Proposition 3.27 can be reformulated as follows. Let $\langle\Box\rangle$ be
the free $\infty$-type theory generated by one object $\Box$ and
$\langle\widetilde{\Box}:1\to\Box\rangle$ the free $\infty$-type theory
generated by one object $\Box$ and one global section $\widetilde{\Box}$ of
$\Box$. By definition, a morphism $\langle\Box\rangle\to\mathcal{C}$
corresponds to an object of $\mathcal{C}$, and a morphism
$\langle\widetilde{\Box}:1\to\Box\rangle\to\mathcal{C}$ corresponds to a pair
$(x,u)$ consisting of an object $x$ of $\mathcal{C}$ and a global section
$u:1\to x$. Then, for an $\infty$-category with representable maps
$\mathcal{C}$ and an object $x\in\mathcal{C}$, we can form a square

${\langle\Box\rangle}$${\mathcal{C}}$${\langle\widetilde{\Box}:1\to\Box\rangle}$${\mathcal{C}/x.}$$\scriptstyle{x}$$\scriptstyle{x^{*}}$$\scriptstyle{\delta_{x}}$
(3)

Proposition 3.27 is equivalent to that, for any $\infty$-category with
representable maps, the diagram

${\mathbf{REP}_{\infty}(\mathcal{C}/x,\mathcal{D})}$${\mathbf{REP}_{\infty}(\langle\widetilde{\Box}:1\to\Box\rangle,\mathcal{D})}$${\mathbf{REP}_{\infty}(\mathcal{C},\mathcal{D})}$${\mathbf{REP}_{\infty}(\langle\Box\rangle,\mathcal{D})}$

induced by Eq. 3 is a pullback of spaces. In other words:

######  Proposition 3.28.

For an $\infty$-category with representable maps $\mathcal{C}$ and an object
$x\in\mathcal{C}$, Eq. 3 is a pushout in $\mathbf{REP}_{\infty}$.

Using Proposition 3.22 and its corollary, we have the following description of
$\mathbf{Mod}(\mathbb{T}/x)$ for an $\infty$-type theory $\mathbb{T}$ and an
object $x\in\mathbb{T}$. We first observe:

  1. 1.

$\mathbf{Mod}(\langle\Box\rangle)\simeq\mathbf{RFib}^{\prime}$ where
$\mathbf{RFib}^{\prime}$ is the base change of $\mathbf{RFib}$ along the
forgetful functor
$\mathbf{Lex}_{\infty}^{(\emptyset)}\to\mathbf{Cat}_{\infty}$;

  2. 2.

$\mathbf{Mod}(\langle\widetilde{\Box}:1\to\Box\rangle)\simeq\mathbf{RFib}^{\prime}_{\bullet}$
where $\mathbf{RFib}^{\prime}_{\bullet}$ is the $\infty$-category of right
fibrations $A\to\mathcal{C}$ with a terminal object in $\mathcal{C}$ and a
global section $a:\mathcal{C}\to A$.

These follow from Proposition 3.22, for example

$\displaystyle\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}((\mathcal{I},\mathcal{C}),(\mathbf{Mod}(\langle\Box\rangle),\mathrm{ev}_{{\star}}))$
$\displaystyle\simeq{}$
$\displaystyle\mathbf{REP}_{\infty}(\langle\Box\rangle,\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}})$
$\displaystyle\simeq{}$
$\displaystyle(\mathbf{Fun}(\mathcal{I},\mathbf{RFib})_{\mathcal{C}})^{\simeq}$
$\displaystyle\simeq{}$
$\displaystyle\mathbf{CAT}_{\infty}/\mathbf{Lex}_{\infty}^{(\emptyset)}((\mathcal{I},\mathcal{C}),(\mathbf{RFib}^{\prime},\mathrm{cod}))$

for any $\mathcal{C}:\mathcal{I}\to\mathbf{Lex}_{\infty}^{(\emptyset)}$. Then,
by Corollaries 3.23 and 3.28, we have:

######  Proposition 3.29.

For any $\infty$-type theory $\mathbb{T}$ and any object $x\in\mathbb{T}$, we
have a pullback

${\mathbf{Mod}(\mathbb{T}/x)}$${\mathbf{RFib}^{\prime}_{\bullet}}$${\mathbf{Mod}(\mathbb{T})}$${\mathbf{Mod}(\langle\Box\rangle)}$${\mathbf{RFib}^{\prime}.}$$\scriptstyle{x^{*}}$$\scriptstyle{\simeq}$

##  4 The theory-model correspondence

Given an $\infty$-type theory $\mathbb{T}$, we establish an adjunction between
the $\infty$-category of $\mathbb{T}$-theories and the $\infty$-category of
models of $\mathbb{T}$. The right adjoint assigns an _internal language_ to
each model of $\mathbb{T}$, and the left adjoint assigns a _syntactic model_
to each $\mathbb{T}$-theory. Not all models of $\mathbb{T}$ are syntactic
ones. We give a characterization of syntactic models.

All the results in this section are $\infty$-categorical analogues of results
from the previous work of the second author [46], but proofs are simplified
and improved.

  * •

In the previous work $(2,1)$-categorical (co)limits are distinguished from
$1$-categorical (co)limits, but there is no such difference in the
$\infty$-categorical setting.

  * •

In the previous work the left adjoint of the internal language functor is made
by hand, but in this work we construct the internal language functor inside
the $\infty$-cosmos $\mathfrak{Pr}^{R}_{\omega}$, so it has a left adjoint by
definition. Therefore, all we have to do is to analyze the unit and counit of
the adjunction.

Let $\mathbb{T}$ be an $\infty$-type theory. Since the base $\infty$-category
$\mathcal{M}({\star})$ of a model $\mathcal{M}$ of $\mathbb{T}$ has a terminal
object $1:\Delta^{0}\to\mathcal{M}({\star})$, we have a natural transformation

${\mathbf{Mod}(\mathbb{T})}$${\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})}$${\Delta^{0}}$${\mathbf{Cat}_{\infty}.}$$\scriptstyle{\mathrm{ev}_{{\star}}}$$\scriptstyle{\Delta^{0}}$$\scriptstyle{1}$

Since $\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})$ is the
pullback

${\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})}$${\mathbf{Fun}(\mathbb{T},\mathbf{Cat}_{\infty})^{\to}}$${\mathbf{Cat}_{\infty}}$${\mathbf{Fun}(\mathbb{T},\mathbf{Cat}_{\infty}),}$$\scriptstyle{\mathrm{ev}_{{\star}}}$$\scriptstyle{\mathrm{cod}}$$\scriptstyle{\delta}$

the functor
$\mathrm{ev}_{{\star}}:\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})\to\mathbf{Cat}_{\infty}$
is a cartesian fibration in $\mathfrak{Pr}^{R}_{\omega}$. Thus, the natural
transformation $1$ induces an $\omega$-accessible right adjoint
$1^{*}:\mathbf{Mod}(\mathbb{T})\to(\Delta^{0})^{*}\mathbf{Fun}(\mathbb{T}^{\triangleright},\mathbf{Cat}_{\infty})\simeq\mathbf{Fun}(\mathbb{T},\mathbf{Cat}_{\infty})$.
By the definition of a model of $\mathbb{T}$, the functor
$1^{*}:\mathbf{Mod}(\mathbb{T})\to\mathbf{Fun}(\mathbb{T},\mathbf{Cat}_{\infty})$
factors through
$\mathbf{Th}(\mathbb{T})=\mathbf{Lex}(\mathbb{T},\mathbf{S})\subset\mathbf{Fun}(\mathbb{T},\mathbf{Cat}_{\infty})$.
We denote this functor $\mathbf{Mod}(\mathbb{T})\to\mathbf{Th}(\mathbb{T})$ by
$\mathrm{L}$. By definition, $\mathrm{L}(\mathcal{M})$ is the composite

${\mathbb{T}}$${\mathbf{RFib}_{\mathcal{M}({\star})}}$${\mathbf{S}}$$\scriptstyle{\mathcal{M}}$$\scriptstyle{1^{*}}$

where $1^{*}A$ is the fiber over $1\in\mathcal{M}({\star})$ for a right
fibration $A$ over $\mathcal{M}({\star})$. As the functor
$\mathrm{L}:\mathbf{Mod}(\mathbb{T})\to\mathbf{Th}(\mathbb{T})$ lies in
$\mathfrak{Pr}^{R}_{\omega}$, it has a left adjoint
$\mathcal{F}:\mathbf{Th}(\mathbb{T})\to\mathbf{Mod}(\mathbb{T})$.

######  Definition 4.1.

For a model $\mathcal{M}$ of $\mathbb{T}$, the $\mathbb{T}$-theory
$\mathrm{L}(\mathcal{M})$ is called the _internal language of $\mathcal{M}$_.
For a theory $K$ over $\mathbb{T}$, we call $\mathcal{F}(K)$ the _syntactic
model_ generated by a $\mathbb{T}$-theory $K$.

In this section, we prove the following:

  1. 1.

the unit of the adjunction $\mathcal{F}\dashv\mathrm{L}$ is invertible, so the
functor $\mathcal{F}:\mathbf{Th}(\mathbb{T})\to\mathbf{Mod}(\mathbb{T})$ is
fully faithful;

  2. 2.

the essential image of
$\mathcal{F}:\mathbf{Th}(\mathbb{T})\to\mathbf{Mod}(\mathbb{T})$ is the class
of democratic models of $\mathbb{T}$ defined below.

Consequently, the adjunction $\mathcal{F}\dashv\mathrm{L}$ induces an
equivalence between $\mathbf{Th}(\mathbb{T})$ and the full subcategory of
$\mathbf{Mod}(\mathbb{T})$ spanned by the democratic models of $\mathbb{T}$.
We define the notion of a democratic model in Section 4.1. The components of
the unit $\eta:\mathrm{id}\Rightarrow\mathrm{L}\mathcal{F}$ are completely
determined by the components at the representable $\mathbb{T}$-theories
${\mathbb{T}}(x,{-})$, because $\mathbf{Th}(\mathbb{T})$ is the cocompletion
of $\mathbb{T}^{\mathrm{op}}$ under filtered colimits and the right adjoint
$\mathrm{L}:\mathbf{Mod}(\mathbb{T})\to\mathbf{Th}(\mathbb{T})$ preserves
filtered colimits. We thus study in details the syntactic model generated by a
representable $\mathbb{T}$-theory. In Section 4.2 we concretely describe the
initial model of $\mathbb{T}$ which is the syntactic model generated by the
initial $\mathbb{T}$-theory ${\mathbb{T}}(1,{-})$. We then generalize it in
Section 4.3 to a description of the syntactic model generated by an arbitrary
representable $\mathbb{T}$-theory. Finally we prove the main results in
Section 4.4.

###  4.1 Democratic models

For a model $\mathcal{M}$ of an $\infty$-type theory, we think of an object
$\Gamma\in\mathcal{M}({\star})$ as a context (see Example 3.6), but contexts
from the syntax of type theory satisfy an additional property: every context
is obtained from the empty context by context comprehension. A model of an
$\infty$-type theory satisfying this property is said to be _democratic_ ,
generalizing the notion of a democratic category with families [13].

######  Definition 4.2.

Let $\mathcal{M}$ be a model of $\mathbb{T}$, $u:x\to y$ a representable arrow
in $\mathbb{T}$, $\Gamma\in\mathcal{M}({\star})$ an object and
$b:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(y)$ a section. Let
$\delta_{u}:\mathcal{M}(y)\to\mathcal{M}(x)$ be the right adjoint of
$\mathcal{M}(u)$. Then the counit
$\mathrm{p}_{u}(b):\mathcal{M}(u)(\delta_{u}(b))\to b$ is a pullback square

${\mathcal{M}({\star})/\\{b\\}_{u}}$${\mathcal{M}(x)}$${\mathcal{M}({\star})/\Gamma}$${\mathcal{M}(y).}$$\scriptstyle{\delta_{u}(b)}$$\scriptstyle{\mathrm{p}_{u}(b)}$$\scriptstyle{\mathcal{M}(u)}$$\scriptstyle{b}$

We refer to the object $\\{b\\}_{u}$ the _context comprehension of $b$ with
respect to $u$_.

######  Definition 4.3.

Let $\mathcal{M}$ be a model of $\mathbb{T}$. The class of _contextual objects
of $\mathcal{M}$_ is the smallest replete class of objects of
$\mathcal{M}({\star})$ containing the terminal object and closed under context
comprehension.

In other words, the contextual objects of $\mathcal{M}$ are inductively
defined as follows:

  * •

the terminal object $1\in\mathcal{M}({\star})$ is contextual;

  * •

if $\Gamma\in\mathcal{M}({\star})$ is a contextual object, $u:x\to y$ is a
representable arrow in $\mathbb{T}$ and
$b:\mathcal{M}({\star})/\Gamma\to\mathcal{M}(y)$ is a section, then the
context comprehension $\\{b\\}_{u}$ is contextual;

  * •

if $\Gamma\in\mathcal{M}({\star})$ is a contextual object and
$\Gamma\simeq\Delta$, then $\Delta$ is contextual.

######  Definition 4.4.

We call a model $\mathcal{M}$ _democratic_ if all the objects of
$\mathcal{M}({\star})$ are contextual. We denote by
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})$ the full subcategory of
$\mathbf{Mod}(\mathbb{T})$ spanned by the democratic models.

One can always find a largest democratic model contained in an arbitrary model
of $\mathbb{T}$.

######  Definition 4.5.

For a model $\mathcal{M}$ of $\mathbb{T}$, we define a model
$\mathcal{M}^{\heartsuit}$ of $\mathbb{T}$ called the _heart of $\mathcal{M}$_
as follows:

  * •

the base $\infty$-category $\mathcal{M}^{\heartsuit}({\star})$ is the full
subcategory of $\mathcal{M}({\star})$ spanned by the contextual objects;

  * •

the functor
$\mathcal{M}^{\heartsuit}:\mathbb{T}\to\mathbf{RFib}_{\mathcal{M}^{\heartsuit}(*)}$
is the composite with the pullback along the inclusion
$\mathcal{M}^{\heartsuit}({\star})\to\mathcal{M}({\star})$

${\mathbb{T}}$${\mathbf{RFib}_{\mathcal{M}({\star})}}$${\mathbf{RFib}_{\mathcal{M}^{\heartsuit}({\star})}.}$$\scriptstyle{\mathcal{M}}$

$\mathcal{M}^{\heartsuit}$ is indeed a model of $\mathbb{T}$, and the
inclusion $\mathcal{M}^{\heartsuit}\hookrightarrow\mathcal{M}$ is a morphism
of models of $\mathbb{T}$. By definition, the functor
$\mathcal{M}^{\heartsuit}:\mathbb{T}\to\mathbf{RFib}_{\mathcal{M}^{\heartsuit}(*)}$
preserves finite limits. Since $\mathcal{M}^{\heartsuit}({\star})$ is closed
under context comprehension, for a representable arrow $u:x\to y$ in
$\mathbb{T}$, the composite
$\mathcal{M}^{\heartsuit}(y)\hookrightarrow\mathcal{M}(y)\overset{\delta_{u}}{\longrightarrow}\mathcal{M}(x)$
factors through $\mathcal{M}^{\heartsuit}(x)\hookrightarrow\mathcal{M}(x)$

${\mathcal{M}^{\heartsuit}(y)}$${\mathcal{M}^{\heartsuit}(x)}$${\mathcal{M}(y)}$${\mathcal{M}(x).}$$\scriptstyle{\delta_{u}}$

This means that
$\mathcal{M}^{\heartsuit}(u):\mathcal{M}^{\heartsuit}(x)\to\mathcal{M}^{\heartsuit}(y)$
has a right adjoint, and the square

${\mathcal{M}^{\heartsuit}(x)}$${\mathcal{M}(x)}$${\mathcal{M}^{\heartsuit}(y)}$${\mathcal{M}(y)}$$\scriptstyle{\mathcal{M}^{\heartsuit}(u)}$$\scriptstyle{\mathcal{M}(u)}$

satisfies the Beck-Chevalley condition. Since the pushforward along
$\mathcal{M}^{\heartsuit}(u)$ is given by the pullback along its right adjoint
$\delta_{u}$, we see that
$\mathcal{M}^{\heartsuit}:\mathbb{T}\to\mathbf{RFib}_{\mathcal{M}^{\heartsuit}({\star})}$
preserves pushforwards along representable maps.

######  Proposition 4.6.

For a democratic model $\mathcal{M}$ of $\mathbb{T}$ and an arbitrary model
$\mathcal{N}$ of $\mathbb{T}$, the inclusion
$\mathcal{N}^{\heartsuit}\hookrightarrow\mathcal{N}$ induces an equivalence of
spaces

$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})(\mathcal{M},\mathcal{N}^{\heartsuit})\simeq\mathbf{Mod}(\mathbb{T})(\mathcal{M},\mathcal{N}).$

In other words, $({-})^{\heartsuit}$ is a right adjoint of the inclusion
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\hookrightarrow\mathbf{Mod}(\mathbb{T})$.

###### Proof.

Because any morphism of models of $\mathbb{T}$ preserves contextual objects,
any morphism $\mathcal{M}\to\mathcal{N}$ from a democratic model $\mathcal{M}$
factors through $\mathcal{N}^{\heartsuit}$. ∎

###  4.2 The initial model

######  Definition 4.7.

Recall that the Yoneda embedding
$\mathbf{y}_{\mathbb{T}}:\mathbb{T}\to\mathbf{RFib}_{\mathbb{T}}$ preserves
all existing limits and pushforwards. Therefore, the pair
$(\mathbb{T},\mathbf{y}_{\mathbb{T}})$ is regarded as a model of $\mathbb{T}$.
We define the _initial model_ $\mathcal{I}(\mathbb{T})$ to be the heart of the
model $(\mathbb{T},\mathbf{y}_{\mathbb{T}})$.

The goal of this subsection is to show that $\mathcal{I}(\mathbb{T})$ is
indeed an initial object of $\mathbf{Mod}(\mathbb{T})$.

By definition, the model $\mathcal{I}(\mathbb{T})$ is described as follows:

  * •

the base $\infty$-category is $\mathbb{T}_{r}$, the full subcategory of
$\mathbb{T}$ spanned by the objects $x$ such that the arrow $x\to 1$ is
representable;

  * •

$\mathcal{I}(\mathbb{T})(y)=\mathbb{T}_{r}/y$ defined by the pullback

${\mathbb{T}_{r}/y}$${\mathbb{T}/y}$${\mathbb{T}_{r}}$${\mathbb{T}}$

for $y\in\mathbb{T}$.

Alternatively, the functor
$\mathcal{I}(\mathbb{T}):\mathbb{T}\to\mathbf{RFib}_{\mathbb{T}_{r}}$ is
defined as the left Kan extension of the Yoneda embedding
$\mathbf{y}_{\mathbb{T}_{r}}:\mathbb{T}_{r}\to\mathbf{RFib}_{\mathbb{T}_{r}}$
along the inclusion $\mathbb{T}_{r}\hookrightarrow\mathbb{T}$.

${\mathbb{T}_{r}}$${\mathbf{RFib}_{\mathbb{T}_{r}}}$${\mathbb{T}}$$\scriptstyle{\mathbf{y}_{\mathbb{T}_{r}}}$$\scriptstyle{\mathcal{I}(\mathbb{T})}$$\scriptstyle{\simeq}$

######  Theorem 4.8.

For an $\infty$-type theory $\mathbb{T}$, the model $\mathcal{I}(\mathbb{T})$
is an initial object in $\mathbf{Mod}(\mathbb{T})$.

###### Proof.

We first note that, since $\mathbf{Mod}(\mathbb{T})$ has finite limits, it
suffices to show that $\mathcal{I}(\mathbb{T})$ is an initial object in the
homotopy category of $\mathbf{Mod}(\mathbb{T})$ [38, Proposition 2.2.2], that
is, for any model $\mathcal{M}$ of $\mathbb{T}$, there exists a morphism
$\mathcal{I}(\mathbb{T})\to\mathcal{M}$ and any two morphisms
$\mathcal{I}(\mathbb{T})\to\mathcal{M}$ are equivalent.

Let $\mathcal{M}$ be a model of $\mathbb{T}$. Suppose that we have a morphism
$G:\mathcal{I}(\mathbb{T})\to\mathcal{M}$. It is regarded as a pair
$(G({\star}),G)$ consisting of a functor
$G({\star}):\mathbb{T}_{r}\to\mathcal{M}({\star})$ and a natural
transformation $G:\mathcal{I}(\mathbb{T})\Rightarrow
G({\star})^{*}\mathcal{M}:\mathbb{T}\to\mathbf{RFib}_{\mathbb{T}_{r}}$.

The Beck-Chevalley condition for a representable arrow $v:y\to z$ in
$\mathbb{T}$ means that, for any object $(u:x\to z)\in\mathbb{T}_{r}/z$, the
square

${\mathcal{M}({\star})/G({\star})(u^{*}y)}$${\mathcal{M}(y)}$${\mathcal{M}({\star})/G({\star})(x)}$${\mathcal{M}(z)}$$\scriptstyle{G(u^{*}y)(v^{*}u)}$$\scriptstyle{u^{*}v}$$\scriptstyle{\mathcal{M}(v)}$$\scriptstyle{G({\star})(u)}$

is a pullback. From the special case when $z$ is the terminal object, we see
that the canonical map
$G(y)(\mathrm{id}_{y}):\mathcal{M}({\star})/G({\star})(y)\to\mathcal{M}(y)$ is
an equivalence for every object $y\in\mathbb{T}_{r}$. In other words, the
diagram

${\mathbb{T}_{r}}$${\mathcal{M}({\star})}$${\mathbb{T}}$${\mathbf{RFib}_{\mathcal{M}({\star})}}$$\scriptstyle{G({\star})}$$\scriptstyle{\mathbf{y}_{\mathcal{M}({\star})}}$$\scriptstyle{\mathcal{M}}$

commutes up to equivalence, and we have an equivalence

$\leavevmode\hbox to85.64pt{\vbox
to87.95pt{\pgfpicture\makeatletter\hbox{\hskip
42.81879pt\lower-43.97473pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.81879pt}{-43.97473pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
9.25768pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.95213pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{T}_{r}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
9.25768pt\hfil&\hfil\hskip 39.27776pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.97224pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathcal{M}({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.27779pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
7.91666pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.61111pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{T}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.91666pt\hfil&\hfil\hskip 45.5611pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.25558pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
21.56113pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 42.20517pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.89966pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathbb{T}_{r}}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
18.2052pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-24.10344pt}{29.05309pt}\pgfsys@lineto{5.37991pt}{29.05309pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.5799pt}{29.05309pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.38588pt}{33.15585pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{G({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-33.56111pt}{20.04793pt}\pgfsys@lineto{-33.56111pt}{2.88217pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{1.0}{0.0}{-33.56111pt}{20.04793pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-33.56111pt}{2.68219pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{20.19337pt}\pgfsys@lineto{21.25766pt}{2.99329pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{2.7933pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{11.13641pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbf{y}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-25.44446pt}{-5.71082pt}\pgfsys@lineto{-0.90343pt}{-5.71082pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-0.70345pt}{-5.71082pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.1823pt}{-3.35805pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathcal{M}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{}{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-30.33914pt}{-12.07053pt}\pgfsys@curveto{-24.6596pt}{-28.15631pt}{-13.91798pt}{-37.34781pt}{2.45927pt}{-40.3989pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9831}{-0.18315}{0.18315}{0.9831}{2.65585pt}{-40.43552pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-33.28296pt}{-38.73462pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathcal{I}(\mathbb{T})}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.54965pt}{-28.77908pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{-15.57053pt}\pgfsys@lineto{21.25766pt}{-32.77061pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{-32.9706pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{-26.58582pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{G({\star})^{*}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.33746pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-13.19688pt}{-27.30531pt}\pgfsys@lineto{3.6706pt}{-16.73631pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.5375pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{-13.19688pt}{-27.30531pt}\pgfsys@lineto{3.6706pt}{-16.73631pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8474}{0.53098}{-0.53098}{0.8474}{3.67058pt}{-16.73633pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ }
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.68938pt}{-19.08516pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{G}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\simeq\leavevmode\hbox
to85.64pt{\vbox to87.95pt{\pgfpicture\makeatletter\hbox{\hskip
42.81879pt\lower-43.97473pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.81879pt}{-43.97473pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
9.25768pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.95213pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{T}_{r}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
9.25768pt\hfil&\hfil\hskip 39.27776pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.97224pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathcal{M}({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.27779pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 45.5611pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.25558pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
21.56113pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 43.59406pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.28854pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathbb{T}_{r}},}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
19.59409pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-24.10344pt}{29.05309pt}\pgfsys@lineto{5.37991pt}{29.05309pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.5799pt}{29.05309pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.38588pt}{33.15585pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{G({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{}{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-32.51814pt}{21.48784pt}\pgfsys@curveto{-31.74622pt}{-3.74373pt}{-20.77353pt}{-21.47337pt}{1.11125pt}{-33.2314pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8809}{-0.4733}{0.4733}{0.8809}{1.28741pt}{-33.32605pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-34.04541pt}{-16.31465pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbf{y}_{\mathbb{T}_{r}}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.22394pt}{-8.59523pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{20.19337pt}\pgfsys@lineto{21.25766pt}{2.99329pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{2.7933pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{11.13641pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbf{y}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.33746pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-18.87117pt}{-6.51065pt}\pgfsys@lineto{9.62169pt}{18.73729pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.5375pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{-18.87117pt}{-6.51065pt}\pgfsys@lineto{9.62169pt}{18.73729pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.74844}{0.6632}{-0.6632}{0.74844}{9.62169pt}{18.73729pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ }
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.60406pt}{10.94412pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{G({\star})_{1}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{-15.57053pt}\pgfsys@lineto{21.25766pt}{-32.77061pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{-32.9706pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{-26.58582pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{G({\star})^{*}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

where $G({\star})_{1}$ is the natural transformation
$G({\star})_{x,y}:\mathbb{T}_{r}(x,y)\to\mathcal{M}({\star})(G({\star})(x),G({\star})(y))$.
Hence, $G({\star}):\mathbb{T}_{r}\to\mathcal{M}({\star})$ is uniquely
determined, and then $G:\mathcal{I}(\mathbb{T})\Rightarrow
G({\star})^{*}\mathcal{M}:\mathbb{T}\to\mathbf{RFib}_{\mathbb{T}_{r}}$ is
uniquely determined because
$\mathcal{I}(\mathbb{T}):\mathbb{T}\to\mathbf{RFib}_{\mathbb{T}_{r}}$ is the
left Kan extension of the Yoneda embedding
$\mathbb{T}_{r}:\mathbb{T}_{r}\to\mathbf{RFib}_{\mathbb{T}_{r}}$ along the
inclusion $\mathbb{T}_{r}\hookrightarrow\mathbb{T}$. This shows that morphisms
$\mathcal{I}(\mathbb{T})\to\mathcal{M}$ are unique up to equivalence.

It suffices now to construct a morphism
$F:\mathcal{I}(\mathbb{T})\to\mathcal{M}$ of models of $\mathbb{T}$. We first
construct a functor $F({\star}):\mathbb{T}_{r}\to\mathcal{M}({\star})$. For an
object $x\in\mathbb{T}_{r}$, the map
$\mathcal{M}(x)\to\mathcal{M}(1)\simeq\mathcal{M}({\star})$ of right
fibrations over $\mathcal{M}({\star})$ is representable. Thus, since
$\mathcal{M}({\star})$ has a terminal object, the right fibration
$\mathcal{M}(x)$ is representable. Hence, the restriction of
$\mathcal{M}:\mathbb{T}\to\mathbf{RFib}_{\mathcal{M}({\star})}$ along the
inclusion $\mathbb{T}_{r}\to\mathbb{T}$ factors as a functor
$F({\star}):\mathbb{T}_{r}\to\mathcal{M}({\star})$ followed by the Yoneda
embedding.

${\mathbb{T}_{r}}$${\mathcal{M}({\star})}$${\mathbb{T}}$${\mathbf{RFib}_{\mathcal{M}({\star})}}$$\scriptstyle{F({\star})}$$\scriptstyle{\mathbf{y}_{\mathcal{M}({\star})}}$$\scriptstyle{\mathcal{M}}$

We then define a natural transformation $F:\mathcal{I}(\mathbb{T})\Rightarrow
F({\star})^{*}\mathcal{M}:\mathbb{T}\to\mathbf{RFib}_{\mathbb{T}_{r}}$ to be
the one whose restriction to $\mathbb{T}_{r}$ is the natural transformation
$F({\star}):\mathbf{y}_{\mathbb{T}_{r}}\Rightarrow
F({\star})^{*}\mathcal{M}F({\star}):\mathbb{T}_{r}\to\mathbf{RFib}_{\mathbb{T}_{r}}$.

$\leavevmode\hbox to85.64pt{\vbox
to87.95pt{\pgfpicture\makeatletter\hbox{\hskip
42.81879pt\lower-43.97473pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.81879pt}{-43.97473pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
9.25768pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.95213pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{T}_{r}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
9.25768pt\hfil&\hfil\hskip 39.27776pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.97224pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathcal{M}({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.27779pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
7.91666pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.61111pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{T}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.91666pt\hfil&\hfil\hskip 45.5611pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.25558pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
21.56113pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 42.20517pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.89966pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathbb{T}_{r}}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
18.2052pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-24.10344pt}{29.05309pt}\pgfsys@lineto{5.37991pt}{29.05309pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.5799pt}{29.05309pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.37082pt}{33.15585pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{F({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-33.56111pt}{20.04793pt}\pgfsys@lineto{-33.56111pt}{2.88217pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{1.0}{0.0}{-33.56111pt}{20.04793pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-33.56111pt}{2.68219pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{20.19337pt}\pgfsys@lineto{21.25766pt}{2.99329pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{2.7933pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{11.13641pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbf{y}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-25.44446pt}{-5.71082pt}\pgfsys@lineto{-0.90343pt}{-5.71082pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-0.70345pt}{-5.71082pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.1823pt}{-3.35805pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathcal{M}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{}{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-30.33914pt}{-12.07053pt}\pgfsys@curveto{-24.6596pt}{-28.15631pt}{-13.91798pt}{-37.34781pt}{2.45927pt}{-40.3989pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9831}{-0.18315}{0.18315}{0.9831}{2.65585pt}{-40.43552pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-33.28296pt}{-38.73462pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathcal{I}(\mathbb{T})}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.54965pt}{-28.77908pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{-15.57053pt}\pgfsys@lineto{21.25766pt}{-32.77061pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{-32.9706pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{-26.58582pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{F({\star})^{*}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.33746pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-13.19688pt}{-27.30531pt}\pgfsys@lineto{3.6706pt}{-16.73631pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.5375pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{-13.19688pt}{-27.30531pt}\pgfsys@lineto{3.6706pt}{-16.73631pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8474}{0.53098}{-0.53098}{0.8474}{3.67058pt}{-16.73633pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ }
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.65926pt}{-19.08516pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{F}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\simeq\leavevmode\hbox
to85.64pt{\vbox to87.95pt{\pgfpicture\makeatletter\hbox{\hskip
42.81879pt\lower-43.97473pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.81879pt}{-43.97473pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
9.25768pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.95213pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbb{T}_{r}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
9.25768pt\hfil&\hfil\hskip 39.27776pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.97224pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathcal{M}({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.27779pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 45.5611pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.25558pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
21.56113pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 42.20517pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.89966pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathbf{RFib}_{\mathbb{T}_{r}}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
18.2052pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-24.10344pt}{29.05309pt}\pgfsys@lineto{5.37991pt}{29.05309pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.5799pt}{29.05309pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.37082pt}{33.15585pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{F({\star})}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{}{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-32.51814pt}{21.48784pt}\pgfsys@curveto{-31.38574pt}{-4.22656pt}{-19.98303pt}{-22.10927pt}{2.49763pt}{-33.8013pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.88718}{-0.46143}{0.46143}{0.88718}{2.67503pt}{-33.89357pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-33.44019pt}{-16.80484pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbf{y}_{\mathbb{T}_{r}}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-20.61871pt}{-9.08542pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{20.19337pt}\pgfsys@lineto{21.25766pt}{2.99329pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{2.7933pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{11.13641pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbf{y}_{\mathcal{M}({\star})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.33746pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-18.26595pt}{-6.94325pt}\pgfsys@lineto{9.90851pt}{18.71504pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.5375pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{-18.26595pt}{-6.94325pt}\pgfsys@lineto{9.90851pt}{18.71504pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.73935}{0.67332}{-0.67332}{0.73935}{9.9085pt}{18.71504pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ }
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.13791pt}{10.72783pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{F({\star})_{1}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.25766pt}{-15.57053pt}\pgfsys@lineto{21.25766pt}{-32.77061pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{21.25766pt}{-32.9706pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.61043pt}{-26.58582pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{F({\star})^{*}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

In order to show that $F$ is a morphism of models of $\mathbb{T}$, it remains
to prove that $F({\star}):\mathbb{T}_{r}\to\mathcal{M}({\star})$ preserves
terminal objects and that $F$ satisfies the Beck-Chevalley condition for
representable arrows. The first claim is clear by definition. For the second,
we have to show that, for any representable arrow $v:y\to z$ in $\mathbb{T}$,
the square

${\mathbb{T}_{r}/y}$${\mathcal{M}(y)}$${\mathbb{T}_{r}/z}$${\mathcal{M}(z)}$$\scriptstyle{F(y)}$$\scriptstyle{v}$$\scriptstyle{\mathcal{M}(v)}$$\scriptstyle{F(z)}$

satisfies the Beck-Chevalley condition. It suffices to show that, for any
arrow $u:x\to z$ with $x\in\mathbb{T}_{r}$, the composite of squares

${\mathbb{T}_{r}/u^{*}y}$${\mathbb{T}_{r}/y}$${\mathcal{M}(y)}$${\mathbb{T}_{r}/x}$${\mathbb{T}_{r}/z}$${\mathcal{M}(z)}$$\scriptstyle{v^{*}u}$$\scriptstyle{u^{*}v}$$\scriptstyle{F(y)}$$\scriptstyle{v}$$\scriptstyle{\mathcal{M}(v)}$$\scriptstyle{u}$$\scriptstyle{F(z)}$
(4)

satisfies the Beck-Chevalley condition. By the definition of $F$, Eq. 4 is
equivalent to

${\mathbb{T}_{r}/u^{*}y}$${\mathcal{M}(*)/F({\star})(u^{*}y)}$${\mathcal{M}(u^{*}y)}$${\mathcal{M}(y)}$${\mathbb{T}_{r}/x}$${\mathcal{M}(*)/F({\star})(x)}$${\mathcal{M}(x)}$${\mathcal{M}(z).}$$\scriptstyle{F({\star})}$$\scriptstyle{u^{*}v}$$\scriptstyle{\simeq}$$\scriptstyle{F({\star})(u^{*}v)}$$\scriptstyle{\mathcal{M}(v^{*}u)}$$\scriptstyle{\mathcal{M}(u^{*}v)}$$\scriptstyle{\mathcal{M}(v)}$$\scriptstyle{F({\star})}$$\scriptstyle{\simeq}$$\scriptstyle{\mathcal{M}(u)}$
(5)

The right square of Eq. 5 satisfies the Beck-Chevalley condition by Corollary
2.15. The middle square satisfies the Beck-Chevalley condition as the
horizontal maps are equivalences. The Beck-Chevalley condition for the left
square asserts that $F({\star})$ preserves pullbacks of representable arrows
in $\mathbb{T}_{r}$, which is true by the definition of $F({\star})$. ∎

###  4.3 Syntactic models generated by representable theories

We describe the model $\mathcal{F}(\mathbf{y}(x))$ for $x\in\mathbb{T}$, where
$\mathbf{y}:\mathbb{T}^{\mathrm{op}}\to\mathbf{Th}(\mathbb{T})\subset\mathbf{Fun}(\mathbb{T},\mathbf{S})$
is the Yoneda embedding.

######  Proposition 4.9.

For an object $x$ of $\mathbb{T}$, we have a pullback

${\mathbf{Mod}(\mathbb{T}/x)}$${\mathbf{y}(x)/\mathbf{Th}(\mathbb{T})}$${\mathbf{Mod}(\mathbb{T})}$${\mathbf{Th}(\mathbb{T}).}$$\scriptstyle{\mathrm{L}}$

###### Proof.

Recall (Proposition 3.29) that we have a pullback

${\mathbf{Mod}(\mathbb{T}/x)}$${\mathbf{RFib}^{\prime}_{\bullet}}$${\mathbf{Mod}(\mathbb{T})}$${\mathbf{RFib}^{\prime}.}$$\scriptstyle{x^{*}}$

For an object $(A\to\mathcal{C})\in\mathbf{RFib}^{\prime}$, the fiber of
$\mathbf{RFib}^{\prime}_{\bullet}$ over $(A\to\mathcal{C})$ is the space of
global sections of $A$. Since the base $\infty$-category $\mathcal{C}$ has a
terminal object $1$, that space is equivalent to the fiber of $A$ over $1$. In
other words, we have a pullback

${\mathbf{RFib}^{\prime}_{\bullet}}$${1/\mathbf{S}}$${\mathbf{RFib}^{\prime}}$${\mathbf{S}.}$$\scriptstyle{1^{*}}$

By the definition of $\mathrm{L}$, the composite $1^{*}\circ x^{*}$ is
equivalent to the composite

${\mathbf{Mod}(\mathbb{T})}$${\mathbf{Th}(\mathbb{T})}$${\mathbf{S}.}$$\scriptstyle{\mathrm{L}}$$\scriptstyle{\mathrm{ev}_{x}}$

By Yoneda, we have a pullback

${\mathbf{y}(x)/\mathbf{Th}(\mathbb{T})}$${1/\mathbf{S}}$${\mathbf{Th}(\mathbb{T})}$${\mathbf{S},}$$\scriptstyle{\mathrm{ev}_{x}}$

and then we get a pullback as in the statement. ∎

By Proposition 4.9, we get an equivalence

$\mathbf{Mod}(\mathbb{T}/x)\simeq(\mathbf{y}(x)\downarrow\mathrm{L}).$

Since $\mathcal{F}(\mathbf{y}(x))$ is the initial object of
$(\mathbf{y}(x)\downarrow\mathrm{L})$, it is obtained from the initial model
$\mathcal{I}(\mathbb{T}/x)$ of $\mathbb{T}/x$ by restricting the morphism of
$\infty$-categories with representable maps
$\mathcal{I}(\mathbb{T}/x):\mathbb{T}/x\to\mathbf{RFib}_{\mathcal{I}(\mathbb{T}/x)({\star})}$
along $x^{*}:\mathbb{T}\to\mathbb{T}/x$. We thus have a concrete description
of $\mathcal{F}(\mathbf{y}(x))$ as follows:

  * •

the base $\infty$-category $\mathcal{F}(\mathbf{y}(x))({\star})$ is the full
subcategory of $\mathbb{T}/x$ spanned by the representable arrows over $x$;

  * •

for objects $y\in\mathbb{T}$ and $(u:x^{\prime}\to
x)\in\mathcal{F}(\mathbf{y}(x))({\star})$, the fiber of
$\mathcal{F}(\mathbf{y}(x))(y)$ over $u$ is
$\mathbb{T}/x(u,x^{*}y)\simeq\mathbb{T}(x^{\prime},y)$.

###  4.4 The equivalence of theories and democratic models

######  Proposition 4.10.

The unit of the adjunction
$\mathcal{F}\dashv\mathrm{L}:\mathbf{Th}(\mathbb{T})\to\mathbf{Mod}(\mathbb{T})$
is invertible. Consequently, the left adjoint
$\mathcal{F}:\mathbf{Th}(\mathbb{T})\to\mathbf{Mod}(\mathbb{T})$ is fully
faithful.

###### Proof.

Since both functors $\mathcal{F}$ and $\mathrm{L}$ preserves filtered
colimits, it suffices to show that the unit
$\eta_{K}:K\to\mathrm{L}(\mathcal{F}(K))$ is invertible for every
representable functor $K:\mathbb{T}\to\mathbf{S}$. From the description of
$\mathcal{F}(\mathbf{y}(x))$ in Section 4.3, we have that
$\mathrm{L}(\mathcal{F}(\mathbf{y}(x)))(y)\simeq\mathbb{T}(x,y)=\mathbf{y}(x)(y)$
and $\eta_{\mathbf{y}(x)}$ is just the identity. ∎

######  Proposition 4.11.

The functor $\mathcal{F}:\mathbf{Th}(\mathbb{T})\to\mathbf{Mod}(\mathbb{T})$
factors through
$\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\subset\mathbf{Mod}(\mathbb{T})$.

###### Proof.

Since $\mathbf{Mod}^{\mathrm{dem}}(\mathbb{T})\subset\mathbf{Mod}(\mathbb{T})$
is a coreflective subcategory by Proposition 4.6, it is closed under colimits.