Institute for Computing and Information Sciences, Radboud University,
Nijmegen, The Netherlands and https://nmvdw.github.io<EMAIL_ADDRESS>https://orcid.org/0000-0003-1146-4161 This research was supported by the NWO
project “The Power of Equality” OCENW.M20.380, which is financed by the Dutch
Research Council (NWO). Niels van der Weide <ccs2012> <concept>
<concept_id>10003752.10003790.10002990</concept_id>uni <concept_desc>Theory of
computation Logic and verification</concept_desc>
<concept_significance>300</concept_significance> </concept> <concept>
<concept_id>10003752.10003790.10011740</concept_id> <concept_desc>Theory of
computation Type theory</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[300]Theory of computation Logic and verification [500]Theory of computation
Type theory [cite=UniMath]Softwarehttps://doi.org/10.5281/zenodo.8427604

###### Acknowledgements.

The author thanks the anonymous reviewers of the HoTT/UF workshop for their
useful comments, and Nima Rasekh for useful discussions. The author also
thanks the Coq developers for providing the Coq proof assistant and their
continuous support to keep compatible with Coq. John Q. Open and Joan R.
Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT
2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Univalent Enriched Categories and the Enriched Rezk Completion

Niels van der Weide

###### Abstract

Enriched categories are categories whose sets of morphisms are enriched with
extra structure. Such categories play a prominent role in the study of higher
categories, homotopy theory, and the semantics of programming languages. In
this paper, we study univalent enriched categories. We prove that all
essentially surjective and fully faithful functors between univalent enriched
categories are equivalences, and we show that every enriched category admits a
Rezk completion. Finally, we use the Rezk completion for enriched categories
to construct univalent enriched Kleisli categories.

###### keywords:

enriched categories, univalent categories, homotopy type theory, univalent
foundations, Rezk completion

###### category:

##  1 Introduction

Over the years, category theory [16] has established itself as a powerful
mathematical framework with a wide variety of applications. The applications
of category theory range from pure mathematics [9, 35] to computer science
[21, 23, 24, 25]. This study resulted in the development of various notions of
categories.

One of these notions is given by _enriched categories_. Enriched categories
are categories whose morphisms are equipped with additional structure.
Examples of such categories are plentiful. For instance, in the study of the
semantics of effectful programming languages, one uses categories enriched
over _directed complete partial orders_ (DCPOs) [23, 24, 25]. The type of
morphisms in categories enriched over DCPOs is given by a DCPO, and thus
fixpoint equations of morphisms can be solved in such categories [34]. For
similar purposes, categories enriched over partial orders have been used [19].
Other applications of enriched categories appear in homological algebra [35]
where one is interested in categories enriched over abelian groups, abstract
homotopy theory [9] where one looks at categories enriched over simplicial
sets, and higher category theory [14] where one consider categories enriched
over categories.

#### Univalent Foundations.

Throughout this paper, we work in univalent foundations [26, 29]. Univalent
foundations is an extension of dependent Martin-Löf Type Theory [17] with the
_univalence axiom_. This axiom says that the identity of types is the same
equivalences between them. More specifically, we have a map that sends
identities $A=B$ to equivalences $A\simeq B$, and the univalence axiom states
that this map is an equivalence. Concretely, this means that properties of
types are invariant under equivalence and that two types share the same
properties whenever we have an equivalence between them.

Univalent foundations is especially interesting for the study of category
theory. In category theory, objects are viewed up to isomorphism: whenever
there is an isomorphism between two objects, they share the same categorical
properties. This is known as the _principle of equivalence_ , and this
principle is made precise using _univalent categories_.

#### Univalent Categories.

In univalent foundations, the “correct” notion of category is given by
univalent categories. Given two objects $x$ and $y$ in a category, we have a
map sending identities $x=y$ to isomorphisms $x\cong y$. In a univalent
category, this mapping is required to be an equivalence: identities between
objects are thus the same as isomorphisms. Hence, whenever two objects are
isomorphic, they satisfy the same properties. Semantically, this is the
correct notion of category, because in the simplicial set model, univalent
categories correspond to set-theoretic categories [11].

There are several consequences of univalence for categories. For instance, we
have a _structure identity principle_ for univalent categories. This principle
says that the identity type of two categories is equivalent to the type of
adjoint equivalences between them [2]. As a consequence, one gets that
whenever two categories are equivalent, then the have the same properties.
Another consequence is that every essentially surjective fully faithful
functor is an adjoint equivalence as well. Usually, one uses the axiom of
choice to prove this principle, but if the domain is univalent, then one can
constructively prove this fact. Finally, every category is weakly equivalent
to a univalent one, which is called its _Rezk completion_ [2].

While most categories that one encounters in practice are univalent (e.g.,
Eilenberg-Moore categories and functor categories), some are not. An example
is given by the Kleisli category. Usually, the Kleisli category
$\mathsf{K}(\mathsf{T})$ of a monad $\mathsf{T}$ on a category $\mathsf{C}$ is
defined to be the category whose objects are objects of $\mathsf{C}$ and whose
morphisms from $x$ to $y$ are morphisms $x\rightarrow\mathsf{T}\>y$ in
$\mathsf{C}$. However, this does not give rise to a univalent category in
general. One can give an alternative presentation of the Kleisli category as a
full subcategory $\mathsf{Kleisli}(\mathsf{T})$ of the Eilenberg-Moore
category to obtain a univalent category [4]. To prove the desired theorems
about $\mathsf{Kleisli}(\mathsf{T})$, one uses that it is the Rezk completion
of $\mathsf{K}(\mathsf{T})$ [30].

#### Univalent Enriched Categories.

In this paper, we develop enriched category theory in univalent foundations.
More specifically, we define univalent enriched categories, and we prove
analogous theorems for univalent enriched categories as for univalent
categories. We show that univalent enriched categories satisfy a structure
identity principle, that every essentially surjective fully faithful functor
is an adjoint equivalence, and that every enriched category admits a Rezk
completion. We also use apply these theorems to construct univalent enriched
Kleisli categories.

#### Related work.

While there are numerous libraries that contain a formalization of categories,
enriched categories have gotten less attention. Several libraries, such as
Agda categories [10] using Agda [22], mathlib [18] using Lean, and the
category-theory library [36] in Coq [28], contain a couple of basic
definitions. In , Satoshi Kura also formalized several basic concepts of
enriched categories. However, none of the aforementioned formalizations
consider much of the theory of enriched categories, and they do not consider
univalent enriched categories. In addition, we use enrichments (Definition
2.2), while the other formalizations use the definition as given by Kelly
[12]. Enrichments have been used in the setting of skew-enriched categories
[5], and, with a slightly different definition, in the study of strong monads
[20, Definition 5.1].

#### Formalization.

The results in this paper are formalized in the Coq [28] proof assistant using
the library [33]. Definitions and theorems are accompanied with links to their
corresponding identifier in the formalization, and these links are underlined.
The tool coqwc reports the following number of lines of code in the
formalization.

         spec    proof comments
        17855     9242      520 total

Beside what is discussed in this paper, the formalization also contains
(weighted) limits and colimits in enriched categories and models of the
enriched effect calculus [7].

#### Contributions and Overview.

The contributions of this paper are as follows.

  * •

A construction of the bicategory of univalent enriched categories (Definition
2.5) and a proof that this bicategory is univalent (2.6);

  * •

a construction of the image factorization system of enriched categories
(Section 4);

  * •

a proof that all fully faithful and essentially surjective enriched functors
are adjoint equivalences (4.8);

  * •

a construction of the Rezk completion for enriched categories (Section 5) and
a proof of its universal property (5.5);

  * •

a construction of Kleisli objects (Section 6) in the bicategory of univalent
enriched categories.

In Section 3, we discuss numerous examples of enriched categories.

##  2 The Bicategory of Enriched Categories

In the remainder of this paper, we study univalent enriched categories, and in
this section, we discuss a structure identity principle for univalent enriched
categories, which says that identity of univalent enriched categories is the
same as equivalence. Before we do so, we briefly recall _monoidal categories_
to fix the notation for the remainder of the paper [3, 16].

######  Definition 2.1.

A monoidal category consists of a category $\mathsf{V}$ together with

  * •

an object $\mathbb{1}_{\mathsf{V}}:\mathsf{V}$;

  * •

a bifunctor $-\otimes-:\mathsf{V}\times\mathsf{V}\rightarrow\mathsf{V}$;

  * •

isomorphisms $\mathsf{l}_{x}:\mathbb{1}_{\mathsf{V}}\otimes x\rightarrow x$,
$\mathsf{r}_{x}:x\otimes\mathbb{1}_{V}\rightarrow x$, and
$\mathsf{a}_{x,y,z}:(x\otimes y)\otimes z\rightarrow x\otimes(y\otimes z)$;

such that $\mathsf{l}_{-}$, $\mathsf{r}_{-}$, and $\mathsf{a}_{-,-,-}$ are
natural and such that the triangle and pentagon laws hold.

A symmetric monoidal category is a monoidal category $\mathsf{V}$ together
with morphisms $\mathsf{s}_{x,y}:x\otimes y\rightarrow y\otimes x$, such that
$\mathsf{s}_{x,y}$ and $\mathsf{s}_{y,x}$ are inverses, $\mathsf{s}_{-,-}$ is
natural, and satisfies the hexagon law.

A symmetric monoidal closed category is a symmetric monoidal category
$\mathsf{V}$ such that for every $x:\mathsf{V}$ the functor $x\otimes-$ has a
right adjoint.

If we have a symmetric monoidal closed category, then we have internal homs
$x\multimap y$. We also have evaluation morphisms $\epsilon_{x,y}:(x\multimap
y)\otimes x\rightarrow y$, and an internal lambda abstraction operation
$\lambda(f):x\rightarrow y\multimap z$ for every $f:x\otimes y\rightarrow z$.

Usually, a $\mathsf{V}$-enriched category consists of a collection objects
together with a hom-object $\mathcal{E}(x,y)$ in $\mathsf{V}$ for all $x$ and
$y$, such that we have appropriate identity morphisms and a composition
operation [12]. Every enriched category $\mathcal{E}$ has an underlying
category, which has the same collection of objects and whose morphisms from
$x$ to $y$ are morphism $\mathbb{1}\rightarrow\mathcal{E}(x,y)$ in
$\mathsf{V}$.

However, we take a slightly different approach: we use _enrichments_. An
enrichment for a category $\mathsf{C}$ consists of a hom-object
$\mathcal{E}(x,y)$ in $\mathsf{V}$ for all $x$ and $y$, such that we have the
appropriate identity and composition morphisms and such that $\mathsf{C}$ is
equivalent to the underlying category of the corresponding enriched category.
As such, we view an enriched category as a category together with extra
structure. This viewpoint also determines our notion of univalence for
enriched categories: a univalent enriched category is an enriched category
such that its underlying category is univalent. Note that our notion of
univalence is similar to completeness for enriched $\infty$-categories [8].
Using enrichments, we can equivalently phrase univalent enriched categories as
a univalent category together with an enrichment.

######  Definition 2.2.

Let $\mathsf{V}$ be a monoidal category and let $\mathsf{C}$ be a category. A
$\mathsf{V}$-enrichment $\mathcal{E}$ for $\mathsf{C}$ consists of

  * •

for all objects $x,y:\mathsf{C}$ an object $\mathcal{E}(x,y):\mathsf{V}$;

  * •

for every object $x:\mathsf{C}$ a morphism
$\mathsf{id}^{\mathsf{e}}_{\mathcal{E}}(x):\mathbb{1}_{V}\rightarrow\mathcal{E}(x,x)$;

  * •

for all objects $x,y,z:\mathsf{C}$ a morphism
$\mathsf{comp}_{\mathcal{E}}(x,y,z):\mathcal{E}(y,z)\otimes\mathcal{E}(x,y)\rightarrow\mathcal{E}(x,z)$;

  * •

for all morphisms $f:x\rightarrow y$ in $\mathsf{C}$ a morphism
$\overrightarrow{f}:\mathbb{1}_{V}\rightarrow\mathcal{E}(x,y)$;

  * •

for every morphism $f:\mathbb{1}_{V}\rightarrow\mathcal{E}(x,y)$ a morphism
$\overleftarrow{f}:x\rightarrow y$ in $\mathsf{C}$.

In addition, we require that $\overrightarrow{\overleftarrow{f}}=f$ and
$\overleftarrow{\overrightarrow{f}}=f$ and that the following diagrams
commute.

${{\mathbb{1}\otimes\mathcal{E}(x,y)}}$${{\mathcal{E}(y,y)\otimes\mathcal{E}(x,y)}}$${{\mathcal{E}(x,y)}}$$\scriptstyle{\mathsf{id}^{\mathsf{e}}(y)\otimes\operatorname{id}}$$\scriptstyle{\mathsf{comp}(x,y,y)}$$\scriptstyle{\mathsf{l}_{\mathcal{E}(x,y)}}$
${{\mathcal{E}(x,y)\otimes\mathbb{1}}}$${{\mathcal{E}(x,y)\otimes\mathcal{E}(x,x)}}$${{\mathcal{E}(x,y)}}$$\scriptstyle{\operatorname{id}{}\otimes\mathsf{id}^{\mathsf{e}}(x)}$$\scriptstyle{\mathsf{comp}(x,x,y)}$$\scriptstyle{\mathsf{r}_{\mathcal{E}(x,y)}}$
${{(\mathcal{E}(y,z)\otimes\mathcal{E}(x,y))\otimes\mathcal{E}(w,x)}}$${{\mathcal{E}(y,z)\otimes(\mathcal{E}(x,y)\otimes\mathcal{E}(w,x))}}$${{\mathcal{E}(y,z)\otimes\mathcal{E}(w,y)}}$${{\mathcal{E}(x,z)\otimes\mathcal{E}(w,x)}}$${{\mathcal{E}(w,z)}}$$\scriptstyle{\mathsf{a}}$$\scriptstyle{\operatorname{id}\otimes\mathsf{comp}(w,x,y)}$$\scriptstyle{\mathsf{comp}(w,y,z)}$$\scriptstyle{\mathsf{comp}(x,y,z)\otimes\operatorname{id}{}}$$\scriptstyle{\mathsf{comp}(w,x,z)}$

When it is clear from the context, we leave the arguments of $\mathsf{comp}$
and $\mathsf{id}^{\mathsf{e}}$ implicit. In the remainder, we use the
following operations fir $\mathsf{V}$-enrichment $\mathcal{E}$ for a category
$\mathsf{C}$. Given an object $w$ and a morphism $f:x\rightarrow y$, we define
$f^{\mathsf{pre}}$ as the following composition.

${{\mathcal{E}(w,x)}}$${{\mathbb{1}\otimes\mathcal{E}(w,x)}}$${{\mathcal{E}(x,y)\otimes\mathcal{E}(w,x)}}$${{\mathcal{E}(w,y)}}$$\scriptstyle{\mathsf{l}^{-1}}$$\scriptstyle{\overrightarrow{f}\otimes\operatorname{id}{}}$$\scriptstyle{\mathsf{comp}}$

For all objects $z$ and morphisms $f:x\rightarrow y$, we define
$f^{\mathsf{post}}$ as the following composition.

${{\mathcal{E}(y,z)}}$${{\mathcal{E}(y,z)\otimes\mathbb{1}}}$${{\mathcal{E}(y,z)\otimes\mathcal{E}(x,y)}}$${{\mathcal{E}(x,z)}}$$\scriptstyle{\mathsf{r}^{-1}}$$\scriptstyle{\operatorname{id}\otimes\overrightarrow{f}}$$\scriptstyle{\mathsf{comp}}$

The reason why we use enrichments over the usual definition, is because it
simplifies the proof of the structure identity principle for enriched
categories. A structure identity principle is already present for univalent
categories [2, Theorem 6.17], which can be reused directly if we define
enriched categories as pairs of univalent categories together with an
enrichment. However, if we would use the definition in [12] instead, then
reusing this principle would be more cumbersome and thus the desired proof
would be more involved.

To phrase the structure identity principle for enriched categories, we use
_univalent bicategories_. More specifically, this principle for enriched
categories is expressed by saying that the bicategory of enriched categories
is univalent, We define the bicategory of enriched categories using _displayed
bicategories_ [1]. A displayed bicategory over a bicategory $\mathsf{B}$
represents structures and properties to be added to objects, 1-cells, and
2-cells in $\mathsf{B}$. In our case, we define a displayed bicategory
$\mathsf{dEnrichCat}_{\mathsf{V}}$ over the bicategory $\mathsf{UnivCat}$ of
univalent categories, and then $\mathsf{EnrichCat}_{\mathsf{V}}$ is total
bicategory of $\mathsf{dEnrichCat}_{\mathsf{V}}$. The displayed objects over a
univalent category $\mathsf{C}$ are $\mathsf{V}$-enrichments for $\mathsf{C}$,
the displayed 1-cells over a functor are enrichments for functors and the
displayed 2-cells over a natural transformation are proofs that this
transformation is enriched.

Note that from the machinery of displayed bicategories, we get a pseudofunctor
$\mathsf{Und}_{\mathsf{V}}:\mathsf{EnrichCat}_{\mathsf{V}}\rightarrow\mathsf{UnivCat}$,
which sends every enriched category to its underlying category. Using this
pseudofunctor, we can understand an enrichment for $\mathsf{C}$ to be an
object in the fiber of $\mathsf{C}$ along $\mathsf{Und}_{\mathsf{V}}$.

######  Definition 2.3.

Suppose that we have $\mathsf{V}$-enrichments $\mathcal{E}_{1}$ and
$\mathcal{E}_{2}$ for $\mathsf{C}_{1}$ and $\mathsf{C}_{2}$ respectively. A
$\mathsf{V}$-enrichment $\mathcal{F}$ for a functor
$\mathsf{F}:\mathsf{C}_{1}\rightarrow\mathsf{C}_{2}$ from $\mathcal{E}_{1}$ to
$\mathcal{E}_{2}$ is a family of morphisms
$\mathcal{F}(x,y):\mathcal{E}_{1}(x,y)\rightarrow\mathcal{E}_{2}(\mathsf{F}\>x,\mathsf{F}\>y)$
such that the following diagrams commute

${\mathbb{1}}$${{\mathcal{E}_{1}(x,x)}}$${{\mathcal{E}_{2}(\mathsf{F}\>x,\mathsf{F}\>x)}}$$\scriptstyle{\mathsf{id}^{\mathsf{e}}}$$\scriptstyle{\mathcal{F}(x,x)}$$\scriptstyle{\mathsf{id}^{\mathsf{e}}}$
${{\mathcal{E}_{1}(y,z)\otimes\mathcal{E}_{1}(x,y)}}$${{\mathcal{E}_{1}(x,z)}}$${{\mathcal{E}_{2}(\mathsf{F}\>y,\mathsf{F}\>z)\otimes\mathcal{E}_{2}(\mathsf{F}\>x,\mathsf{F}\>y)}}$${{\mathcal{E}_{2}(\mathsf{F}\>x,\mathsf{F}\>z)}}$$\scriptstyle{\mathsf{comp}}$$\scriptstyle{\mathcal{F}(x,z)}$$\scriptstyle{\mathcal{F}(y,z)\otimes\mathcal{F}(x,y)}$$\scriptstyle{\mathsf{comp}}$

In addition, we require that
$\overrightarrow{\mathsf{F}\>f}=\overrightarrow{f}\cdot\mathcal{F}(x,y)$.

######  Definition 2.4.

Let $\mathcal{F}_{1}$ and $\mathcal{F}_{2}$ be $\mathsf{V}$-enrichments for
functors
$\mathsf{F}_{1},\mathsf{F}_{2}:\mathsf{C}_{1}\rightarrow\mathsf{C}_{2}$ from
$\mathcal{E}_{1}$ to $\mathcal{E}_{2}$. A natural transformation
$\tau:F_{1}\Rightarrow F_{2}$ is called $\mathsf{V}$-enriched whenever the
following diagram commutes

${{\mathcal{E}_{1}(x,y)\otimes\mathbb{1}}}$${{\mathcal{E}_{2}(\mathsf{F}_{2}\>x,\mathsf{F}_{2}\>y)\otimes\mathcal{E}_{2}(\mathsf{F}_{1}\>x,\mathsf{F}_{2}\>x)}}$${{\mathcal{E}_{1}(x,y)}}$${{\mathcal{E}_{2}(\mathsf{F}_{1}\>x,\mathsf{F}_{2}\>y)}}$${{\mathbb{1}\otimes\mathcal{E}_{1}(x,y)}}$${{\mathcal{E}_{2}(\mathsf{F}_{1}\>y,\mathsf{F}_{2}\>y)\otimes\mathcal{E}_{2}(\mathsf{F}_{1}\>x,\mathsf{F}_{1}\>y)}}$$\scriptstyle{\mathsf{r}^{-1}}$$\scriptstyle{\mathcal{F}_{2}\otimes\overrightarrow{\tau\>x}}$$\scriptstyle{\mathsf{comp}}$$\scriptstyle{\mathsf{l}^{-1}}$$\scriptstyle{\overrightarrow{\tau\>y}\otimes\mathcal{F}_{1}}$$\scriptstyle{\mathsf{comp}}$

Note that the condition for $\mathsf{V}$-enriched natural transformations can
equivalently formulated as follows.

${{\mathcal{E}_{1}(x,y)}}$${{\mathcal{E}_{2}(\mathsf{F}_{1}\>x,\mathsf{F}_{1}\>y)}}$${{\mathcal{E}_{2}(\mathsf{F}_{2}\>x,\mathsf{F}_{2}\>y)}}$${{\mathcal{E}_{2}(\mathsf{F}_{1}\>x,\mathsf{F}_{2}\>y)}}$$\scriptstyle{\mathcal{F}_{1}}$$\scriptstyle{\mathcal{F}_{2}}$$\scriptstyle{(\tau\>x)^{\mathsf{pre}}}$$\scriptstyle{(\tau\>y)^{\mathsf{post}}}$
(1)

Now we have everything in place to define the bicategory of enriched
categories.

######  Definition 2.5.

Let $\mathsf{V}$ be a monoidal category. We define the displayed bicategory
$\mathsf{dEnrichCat}_{\mathsf{V}}$ of enrichments over $\mathsf{UnivCat}$ as
follows.

  * •

The displayed objects over a category $\mathsf{C}$ are
$\mathsf{V}$-enrichments for $\mathsf{C}$;

  * •

the displayed 1-cells over a functor
$\mathsf{F}:\mathsf{C}_{1}\rightarrow\mathsf{C}_{2}$ from $\mathcal{E}_{1}$ to
$\mathcal{E}_{2}$ are $\mathsf{V}$-enrichments for $\mathsf{F}$ from
$\mathsf{C}_{1}$ to $\mathsf{C}_{2}$;

  * •

the displayed 2-cells over a natural transformation
$\tau:\mathsf{F}_{1}\Rightarrow\mathsf{F}_{2}$ from $\mathcal{F}_{1}$ to
$\mathcal{F}_{2}$ are proofs that $\tau$ is $\mathsf{V}$-enriched.

The bicategory of enriched categories is defined to be the total bicategory of
$\mathsf{dEnrichCat}_{\mathsf{V}}$, and we denote it by
$\mathsf{EnrichCat}_{\mathsf{V}}$. Its objects are univalent
$\mathsf{V}$-enriched categories, and we call the 1-cells and 2-cells of
$\mathsf{EnrichCat}_{\mathsf{V}}$ enriched functors and enriched
transformations respectively.

Note that by construction a univalent $\mathsf{V}$-enriched category is the
same as a univalent category together with a $\mathsf{V}$-enrichment. In
addition, our univalence condition for $\mathsf{V}$-enriched categories has no
local variant in contrast to univalence for bicategories [1], since we only
look at enrichments over monoidal 1-categories.

To show that Definition 2.5 actually gives rise to a displayed bicategory, one
also needs to construct enrichments for the identity and composition, and one
need to prove that the identity transformation is enriched and that enriched
transformations are preserved under composition and whiskering. Details on
this construction are left to the formalization.

######  $\blacktriangleright$ Theorem 2.6.

If $\mathsf{V}$ is a univalent monoidal category, then the bicategory
$\mathsf{EnrichCat}_{\mathsf{V}}$ is univalent.

######  $\blacktriangleright$ Proposition 2.7.

Let $\tau:\mathcal{F}_{1}\Rightarrow\mathcal{F}_{2}$ be a 2-cell in
$\mathsf{EnrichCat}_{\mathsf{V}}$. Then $\tau$ is invertible if the natural
transformation underlying $\tau$ is a natural isomorphism.

##  3 Examples of Enriched Categories

Before we continue our study of univalent enriched categories, we first look
at numerous examples of enrichments that we use in the remainder of this
paper. In Section 3.2, we characterize enrichments over a large class of
structures.

###  3.1 General Examples

######  Example 3.1.

Let $\mathsf{V}$ be a symmetric monoidal closed category. We define a
$\mathsf{V}$-enrichment for $\mathsf{V}$, which we call the self-enrichment
and denote by $\mathsf{self}(\mathsf{V})$, as follows.

  * •

We define $\mathsf{self}(\mathsf{V})(x,y)$ to be $x\multimap y$.

  * •

The enriched identity $\mathsf{id}^{\mathsf{e}}(x):\mathbb{1}\rightarrow
x\multimap x$ is defined to be $\lambda(\mathsf{l}_{x})$.

  * •

The composition $\mathsf{comp}(x,y,z):y\multimap z\otimes x\multimap
y\rightarrow x\multimap z$ is the exponential transpose of the following
composition of morphisms.

${{((y\multimap z)\otimes(x\multimap y))\otimes x}}$${{(y\multimap
z)\otimes((x\multimap y)\otimes x)}}$${{(y\multimap z)\otimes
y}}$${z}$$\scriptstyle{\mathsf{a}}$$\scriptstyle{\operatorname{id}\otimes\epsilon}$$\scriptstyle{\epsilon}$

  * •

Given $f:x\rightarrow y$, we define $\overrightarrow{f}:\mathbb{1}\rightarrow
x\multimap y$ to be $\lambda(\mathsf{l}_{x}\cdot f)$.

  * •

For $f:\mathbb{1}\rightarrow x\multimap y$, we define $\overleftarrow{f}$ to
be the following composition of morphisms.

${x}$${{\mathbb{1}\otimes x}}$${{(x\multimap y)\otimes
x}}$${y}$$\scriptstyle{\mathsf{l}^{-1}_{x}}$$\scriptstyle{f\otimes\operatorname{id}_{x}}$$\scriptstyle{\epsilon}$

If we assume that $\mathsf{V}$ is univalent, then $\mathsf{self}(\mathsf{V})$
is a univalent enriched category.

######  Example 3.2.

Let $\mathsf{C}$ be a category together with a $\mathsf{V}$-enrichment
$\mathcal{E}$, and let $\mathsf{P}$ be a predicate on the objects of
$\mathsf{C}$. From all of this, we obtain a $\mathsf{V}$-enrichment
$\mathsf{FSub}_{\mathsf{e}}(\mathsf{P})$ for the full subcategory
$\mathsf{FSub}(\mathsf{P})$, such that
$\mathsf{FSub}_{\mathsf{e}}(\mathsf{P})(x,y)\coloneqq\mathcal{E}(x,y)$. If
$\mathsf{C}$ is univalent, then the full subcategory of $\mathsf{C}$ is also
univalent, and in that case, this construction gives rise to a univalent
enriched category.

######  Example 3.3.

Suppose that $\mathsf{V}$ is a symmetric monoidal category, and let
$\mathsf{C}$ be a category together with a $\mathsf{V}$-enrichment
$\mathcal{E}$. We define the $\mathsf{V}$-enrichment
$\mathcal{E}^{\mathsf{op}}$, called the opposite enrichment, for
$\mathsf{C}^{\mathsf{op}}$ as follows.

  * •

$\mathcal{E}^{\mathsf{op}}(x,y)\coloneqq\mathcal{E}(y,x)$;

  * •

$\mathsf{id}^{\mathsf{e}}_{\mathcal{E}^{\mathsf{op}}}(x)\coloneqq\mathsf{id}^{\mathsf{e}}_{\mathcal{E}}(x)$;

  * •

$\mathsf{comp}_{\mathcal{E}^{\mathsf{op}}}(x,y,z)\coloneqq\leavevmode\hbox
to242.44pt{\vbox to17.42pt{\pgfpicture\makeatletter\hbox{\hskip
121.21758pt\lower-8.75955pt\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}{-121.21758pt}{-8.65971pt}\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
38.9977pt\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}{-34.69215pt}{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{E}(z,y)\otimes\mathcal{E}(y,x)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
38.9977pt\hfil&\hfil\hskip 62.99767pt\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}{-34.69215pt}{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{E}(y,x)\otimes\mathcal{E}(z,y)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
38.9977pt\hfil&\hfil\hskip 43.22218pt\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}{-14.91667pt}{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{E}(z,x)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
19.22221pt\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{-43.02219pt}{-6.15971pt}\pgfsys@lineto{-19.82217pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.6222pt}{-6.15971pt}\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}{-32.60275pt}{-3.80695pt}\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{\mathsf{s}}$} }}\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{58.97318pt}{-6.15971pt}\pgfsys@lineto{82.17319pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{82.37317pt}{-6.15971pt}\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}{62.60649pt}{-2.44586pt}\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{\mathsf{comp}}$} }}\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}}$

The operations $\overrightarrow{f}$ and $\overleftarrow{f}$ in
$\mathcal{E}^{\mathsf{op}}$ are inherited from $\mathcal{E}$. In addition,
$\mathcal{E}^{\mathsf{op}}$ gives rise to a univalent enriched category if
$\mathsf{C}$ is univalent.

In fact, using Example 3.3 one can construct a duality involution on
$\mathsf{EnrichCat}_{\mathsf{V}}$.

######  Example 3.4.

Suppose that $\mathsf{V}$ is a symmetric monoidal category that has
equalizers, and suppose that we have two enriched functors
$\mathcal{F}_{1},\mathcal{F}_{2}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$.
We have the category $\mathsf{Dialg}(\mathcal{F}_{1},\mathcal{F}_{2})$ of
dialgebras whose objects are pairs $(x,f)$ consisting of an object
$x:\mathcal{E}_{1}$ together with a morphism
$f:\mathcal{F}_{1}\>x\rightarrow\mathcal{F}_{2}\>x$. Morphisms from $(x,f)$ to
$(y,g)$ are morphisms $h:x\rightarrow y$ such that the following diagram
commutes.

${{\mathcal{F}_{1}\>x}}$${{\mathcal{F}_{1}\>y}}$${{\mathcal{F}_{2}\>x}}$${{\mathcal{F}_{2}\>y}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\mathcal{F}_{1}\>h}$$\scriptstyle{\mathcal{F}_{2}\>h}$

We define a $\mathsf{V}$-enrichment
$\mathsf{Dialg}_{\mathsf{e}}(\mathcal{F}_{1},\mathcal{F}_{2})$ for
$\mathsf{Dialg}(\mathcal{F}_{1},\mathcal{F}_{2})$. Suppose that we have
objects $(x,f)$ and $(y,g)$ in
$\mathsf{Dialg}(\mathcal{F}_{1},\mathcal{F}_{2})$. We define the object
$\mathsf{Dialg}_{\mathsf{e}}(\mathcal{F}_{1},\mathcal{F}_{2})((x,f),(y,g))$ as
the equalizer of the following diagram.

${{\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{1}\>y)}}$${{\mathsf{Dialg}_{\mathsf{e}}(\mathcal{F}_{1},\mathcal{F}_{2})((x,f),(y,g))}}$${{\mathcal{E}_{1}(x,y)}}$${{\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{2}\>y)}}$${{\mathcal{E}_{2}(\mathcal{F}_{2}\>x,\mathcal{F}_{2}\>y)}}$$\scriptstyle{\mathcal{F}_{1}}$$\scriptstyle{\mathcal{F}_{2}}$$\scriptstyle{g^{\mathsf{post}}}$$\scriptstyle{f^{\mathsf{pre}}}$

To define the enriched identity and composition morphisms, one uses the
universal property of equalizers. If $\mathsf{C}$ is univalent, then so is the
category of dialgebras, and in that case,
$\mathsf{Dialg}_{\mathsf{e}}(\mathcal{F}_{1},\mathcal{F}_{2})$ is a univalent
enriched category.

Using Example 3.4, one can show that the bicategory
$\mathsf{EnrichCat}_{\mathsf{V}}$ has inserters.

######  Example 3.5.

Let $\mathsf{V}$ be a complete symmetric monoidal category, and suppose that
we have enriched categories $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$. Note that
we have a category $[\mathcal{E}_{1},\mathcal{E}_{2}]$ whose objects are given
by enriched functors from $\mathcal{E}_{1}$ to $\mathcal{E}_{2}$, and whose
morphisms are given by enriched natural transformations. We define a
$\mathsf{V}$-enrichment $\mathsf{EFunctor}(\mathcal{E}_{1},\mathcal{E}_{2})$
for $[\mathcal{E}_{1},\mathcal{E}_{2}]$ as the equalizer of the morphisms
displayed below.

${{\prod_{x:\mathcal{E}_{1}}\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{2}\>x)}}$${{\prod_{x,y:\mathcal{E}_{1}}\mathcal{E}_{1}(x,y)\multimap\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{2}\>y)}}$$\scriptstyle{g}$$\scriptstyle{f}$

Here $f$ is defined to be the following composition of morphisms

${{\prod_{x:\mathcal{E}_{1}}\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{2}\>x)}}$${{\mathcal{E}_{2}(\mathcal{F}_{1}\>y,\mathcal{F}_{2}\>y)}}$${{\mathcal{E}_{1}(x,y)\multimap\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{2}\>y)}}$$\scriptstyle{\pi_{y}}$$\scriptstyle{\varphi}$

where $\varphi$ is the exponential transpose of

${{\mathcal{E}_{2}(\mathcal{F}_{1}\>y,\mathcal{F}_{2}\>y)\otimes\mathcal{E}_{1}(x,y)}}$${{\mathcal{E}_{2}(\mathcal{F}_{1}\>y,\mathcal{F}_{2}\>y)\otimes\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{1}\>y)}}$${{\mathcal{E}_{2}(\mathcal{F}_{1}\>x,\mathcal{F}_{2}\>y).}}$$\scriptstyle{\operatorname{id}{}\otimes\mathcal{F}_{1}}$$\scriptstyle{\mathsf{comp}}$

We define $g$ analogously. The fact that $[\mathcal{E}_{1},\mathcal{E}_{2}]$
is univalent, follows from the fact that $\mathsf{EnrichCat}_{\mathsf{V}}$ is
univalent (2.6).

Inspired by Example 3.5, we can refine Example 3.1. More specifically, given a
small category $\mathsf{C}$, we define a $\mathsf{V}$-enrichment for the
functor category from $\mathsf{C}$ to $\mathsf{V}$. The construction is
analogous to Example 3.5, and details can be found in the formalization.

Finally, we look at the change of base operation for enriched categories, and
for this operation, a subtlety arises. Given a lax monoidal functor
$\mathsf{F}:\mathsf{V}_{1}\rightarrow\mathsf{V}_{2}$, our goal is to define a
pseudofunctor
$\mathsf{EnrichCat}_{\mathsf{V}_{1}}\rightarrow\mathsf{EnrichCat}_{\mathsf{V}_{2}}$.
On objects, this operation acts as follows: given a univalent category
$\mathsf{C}$ together with an enrichment $\mathcal{E}$, then we get an
enriched category $\mathsf{F}^{*}(\mathcal{E})$ whose objects are objects in
$\mathsf{C}$ and such that
$\mathsf{F}^{*}(\mathcal{E})(x,y)=\mathsf{F}\>(\mathcal{E}(x,y))$. However,
the underlying category of this enriched category is not necessarily
univalent. For instance, if we take $\mathsf{F}$ to be the unique monoidal
functor from $\mathsf{Set}$ to the terminal category, then the underlying
category of $\mathsf{F}^{*}(\mathcal{E})$ would have sets as objects, and
inhabitants of the unit type as the morphisms. For this reason, we add a
restriction to $\mathsf{F}$ in order to define the change of base of enriched
categories.

######  Definition 3.6.

Let $\mathsf{F}:\mathsf{V}_{1}\rightarrow\mathsf{V}_{2}$ by a lax monoidal
functor. We say that $\mathsf{F}$ preserves underlying categories if for all
$x:\mathsf{V}_{1}$ the function that sends morphisms
$f:\mathbb{1}_{\mathsf{V}_{1}}\rightarrow x$ to
${{\mathbb{1}_{\mathsf{V}_{2}}}}$${{\mathsf{F}\>\mathbb{1}_{\mathsf{V}_{1}}}}$${{\mathsf{F}\>x}}$$\scriptstyle{\epsilon_{\mathsf{F}}}$$\scriptstyle{\mathsf{F}\>f}$
is an equivalence of types. If we have
$f:\mathbb{1}_{\mathsf{V}_{2}}\rightarrow\mathsf{F}\>x$, then we denote the
action of the inverse by $\zeta_{\mathsf{F}}(f)$.

The requirement in Definition 3.6 says that the underlying category is
preseerved by change of base along $\mathsf{F}$. With this additional
assumption, we define the change of base of enriched categories.

######  Example 3.7.

Let $\mathsf{F}:\mathsf{V}_{1}\rightarrow\mathsf{V}_{2}$ by a lax monoidal
functor that preserves underlying categories, and let $\mathsf{C}$ be a
category together with a $\mathsf{V}$-enrichment $\mathcal{E}$. We define the
change-of-base enrichment $\mathsf{F}^{*}(\mathcal{E})$ for $\mathsf{C}$ as
follows. The hom-object $\mathsf{F}^{*}(\mathcal{E})(x,y)$ is defined to be
$\mathsf{F}\>(\mathcal{E}(x,y))$, and the enriched identity
$\mathsf{id}^{\mathsf{e}}(x)$ is defined as the composition

${{\mathbb{1}_{\mathsf{V}_{2}}}}$${{\mathsf{F}\>\mathbb{1}_{\mathsf{V}_{1}}}}$${{\mathsf{F}\>(\mathcal{E}(x,x))}}$$\scriptstyle{\epsilon_{\mathsf{F}}}$$\scriptstyle{\mathsf{F}\>(\mathsf{id}^{\mathsf{e}}(x))}$

Composition is defined similarly.

${{\mathsf{F}\>(\mathcal{E}(y,z))\otimes\mathsf{F}\>(\mathcal{E}(x,y))}}$${{\mathsf{F}\>(\mathcal{E}(y,z)\otimes\mathcal{E}(x,y))}}$${{\mathsf{F}\>(\mathcal{E}(x,y))}}$$\scriptstyle{\mathsf{F}\>\mathsf{comp}}$$\scriptstyle{\mu_{\mathsf{F}}}$

If we have a morphism $f:x\rightarrow y$, then we define $\overrightarrow{f}$
to be

${{\mathbb{1}_{\mathsf{V}_{2}}}}$${{\mathsf{F}\>\mathbb{1}_{\mathsf{V}_{1}}}}$${{\mathsf{F}\>(\mathcal{E}(x,x)).}}$$\scriptstyle{\epsilon_{\mathsf{F}}}$$\scriptstyle{\mathsf{F}\>(\overrightarrow{f})}$

Finally, for a morphism
$f:\mathbb{1}_{\mathsf{V}_{2}}\rightarrow\mathsf{F}\>(\mathcal{E}(x,x))$, we
define $\overleftarrow{f}$ to be $\overleftarrow{\zeta_{\mathsf{F}}(f)}$. Note
that here we use that $\mathsf{F}$ preserves underlying categories. In
addition, if we assume that $\mathsf{C}$ is univalent, then we get a univalent
enriched category $\mathsf{F}^{*}(\mathcal{E})$.

###  3.2 Enrichments over Structures

Next we characterize two classes of enrichments. First, we characterize
enrichments for the category $\mathsf{Set}$ of sets equipped with its
cartesian monoidal structure.

######  $\blacktriangleright$ Proposition 3.8.

Let $\mathsf{C}$ be a category. The type of $\mathsf{Set}$-enrichments for
$\mathsf{C}$ is contractible.

From Proposition 3.8, we can conclude that the type of categories is
equivalent to the type of $\mathsf{Set}$-enriched categories. Second, we
characterize enrichments for structured sets with a cartesian monoidal
structure. To do so, we first define a general notion of structured sets.

######  Definition 3.9.

A cartesian notion of structure $\mathcal{S}$ consists of

  * •

a set $\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$ of structures on $\mathsf{X}$ for
every set $\mathsf{X}$;

  * •

a proposition
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{Y}})}(f)$ which
represents that $f$ is a structure preserving map from
$\mathsf{p}_{\mathsf{X}}$ to $\mathsf{p}_{\mathsf{Y}}$, for all functions
$f:\mathsf{X}\rightarrow\mathsf{X}$ and structures
$\mathsf{p}_{\mathsf{X}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$ and
$\mathsf{p}_{\mathsf{Y}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{Y}$;

  * •

an inhabitant
$\mathsf{p}_{\mathsf{unit}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{unit}$;

  * •

a structure
$\mathsf{p}_{\mathsf{X}}\times\mathsf{p}_{\mathsf{Y}}:\mathsf{P}_{\mathcal{S}}\>(\mathsf{X}\times\mathsf{Y})$
for all $\mathsf{p}_{\mathsf{X}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$ and
$\mathsf{p}_{\mathsf{Y}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{Y}$,.

This data is required to satisfy the following axioms.

  * •

For every set $\mathsf{X}$ and structure
$\mathsf{p}_{\mathsf{X}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$, we have
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{X}})}(\operatorname{id}_{\mathsf{X}})$;

  * •

for all functions $f:\mathsf{X}\rightarrow\mathsf{Y}$ and
$g:\mathsf{Y}\rightarrow\mathsf{Z}$ such that
$\mathsf{H}_{(\mathsf{P}_{\mathcal{S}}\>\mathsf{X},\mathsf{P}_{\mathcal{S}}\>\mathsf{Y})}(f)$
and
$\mathsf{H}_{(\mathsf{P}_{\mathcal{S}}\>\mathsf{Y},\mathsf{P}_{\mathcal{S}}\>\mathsf{Z})}(g)$,
we have
$\mathsf{H}_{(\mathsf{P}_{\mathcal{S}}\>\mathsf{X},\mathsf{P}_{\mathcal{S}}\>\mathsf{Z})}(g\circ
f)$;

  * •

given structures
$\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{X}}^{\prime}:\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$
such that
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{X}^{\prime}})}(\operatorname{id}_{\mathsf{X}})$
and
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}^{\prime}},\mathsf{p}_{\mathsf{X}})}(\operatorname{id}_{\mathsf{X}})$,
we have $\mathsf{p}_{\mathsf{X}}=\mathsf{p}_{\mathsf{X}}^{\prime}$;

  * •

given a structure
$\mathsf{p}_{\mathsf{X}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$ on a set
$\mathsf{X}$, we have
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{unit}})}(\lambda(x:\mathsf{X}).\mathbf{\mathsf{tt}})$
where $\mathbf{\mathsf{tt}}$ is the unique element of $\mathsf{unit}$;

  * •

given structures
$\mathsf{p}_{\mathsf{X}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{X}$ and
$\mathsf{p}_{\mathsf{Y}}:\mathsf{P}_{\mathcal{S}}\>\mathsf{Y}$ on sets
$\mathsf{X}$ and $\mathsf{Y}$ respectively, we have
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}}\times\mathsf{p}_{\mathsf{Y}},\mathsf{p}_{\mathsf{X}})}(\pi_{1})$
and
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}}\times\mathsf{p}_{\mathsf{Y}},\mathsf{p}_{\mathsf{Y}})}(\pi_{2})$;

  * •

for all functions $f:\mathsf{X}\rightarrow\mathsf{Y}$ and
$g:\mathsf{X}\rightarrow\mathsf{Z}$ such that
$\mathsf{H}_{(\mathsf{P}_{\mathcal{S}}\>\mathsf{X},\mathsf{P}_{\mathcal{S}}\>\mathsf{Y})}(f)$
and
$\mathsf{H}_{(\mathsf{P}_{\mathcal{S}}\>\mathsf{X},\mathsf{P}_{\mathcal{S}}\>\mathsf{Z})}(g)$,
we have
$\mathsf{H}_{(\mathsf{P}_{\mathcal{S}}\>\mathsf{X},\mathsf{p}_{\mathsf{Y}}\times\mathsf{p}_{\mathsf{Z}})}(\lambda(x:\mathsf{X}).(f\>x,g\>x))$.

Note that Definition 3.9 is extension of standard notions of structures
defined in [29, Definition 9.8.1]: the added data and axioms guarantee that
the resulting category has binary products and a terminal object.

######  Problem 3.10.

Given a cartesian notion of structure $\mathcal{S}$, to construct a univalent
cartesian category $\mathsf{Str}(\mathcal{S})$.

$\blacktriangleright$ Construction 3.11 (for Problem 3.10). In [29, Section
9.8], it is shown how every standard notion of structure gives rise to a
univalent category. The terminal object is given by
$(\mathsf{unit},\mathsf{p}_{\mathsf{unit}})$, and the product of
$(\mathsf{X},\mathsf{p}_{\mathsf{X}})$ and
$(\mathsf{Y},\mathsf{p}_{\mathsf{Y}})$ is given by
$(\mathsf{X}\times\mathsf{Y},\mathsf{p}_{\mathsf{X}}\times\mathsf{p}_{\mathsf{Y}})$.
∎

######  $\blacktriangleright$ Proposition 3.12.

Let $\mathsf{C}$ be a category and let $\mathcal{S}$ be a cartesian notion of
structure. Then the type of $\mathsf{Str}(\mathcal{S})$-enrichments for
$\mathsf{C}$ is equivalent to a structure
$\mathsf{hom}_{(x,y)}:\mathsf{P}_{\mathcal{S}}\>(x\rightarrow y)$ for all
objects $x,y:\mathsf{C}$ such that for all $x,y,z:\mathsf{C}$ we have
$\mathsf{H}_{(\mathsf{hom}_{(y,z)}\times\mathsf{hom}_{(x,y)},\mathsf{hom}_{(x,z)})}(\lambda
f.\pi_{2}\>f\cdot\pi_{1}\>f)$.

######  Example 3.13.

We have a cartesian notion of structure $\mathsf{DCPO}$ of directed complete
partial orders structures (DCPOs) such that
$\mathsf{P}_{\mathsf{DCPO}}\>\mathsf{X}$ is the set of DCPOs on $\mathsf{X}$
and such that
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{Y}})}(f)$ expresses
that $f$ is a Scott continuous map. We also have a cartesian notion of
structure $\mathsf{DCPPO}$ of pointed directed complete partial orders
structures (DCPPOs) such that $\mathsf{P}_{\mathsf{DCPPO}}\>\mathsf{X}$ is the
set of DCPPOs on $\mathsf{X}$ and such that
$\mathsf{H}_{(\mathsf{p}_{\mathsf{X}},\mathsf{p}_{\mathsf{Y}})}(f)$ expresses
that $f$ is a Scott continuous map.

######  Remark 3.14.

In Example 3.13, we defined a cartesian notion of structure by _pointed_ DCPOs
and Scott continuous maps without requiring these maps to be strict. For
pointed DCPOs and strict Scott continuous maps, one can also define such a
structure. However, in applications, one is often interested in a different
monoidal structure for pointed DCPOs with strict maps, namely the one given by
the smash product. The formalization contains a further extension of
Definition 3.9, called a structure supporting smash products, and a proof that
every such structure gives rise to a symmetric monoidal closed category. For
such structures, the smash product is constructed a quotient of types, and one
can instantiate this notion using pointed sets and pointed partial orders.

##  4 Image Factorization

We continue our study of univalent enriched category by proving that every
essentially surjective and fully faithful (enriched) functor is an adjoint
equivalence. Classically, one would use the axiom of choice to prove this
fact: to define the inverse, one needs to pick preimages and those are only
guaranteed to be unique up to isomorphism. One can give a constructive proof
of this fact if one assumes that the domain of the functor in question is
univalent.

The way we approach this result, is via _orthogonal factorization systems_ in
bicategories. More specifically, we show that the essentially surjective and
the fully faithful enriched functors form an orthogonal factorization system
[15, Lemma 4.3.5]. From this fact, one directly obtains that every essentially
surjective and fully faithful functor is an adjoint equivalence. The proof is
similar to how in orthogonal factorization systems in categories the
intersection of the left and right class of maps are precisely the
isomorphisms.

We start by defining _orthogonal_ maps in bicategories.

######  Definition 4.1.

Let $\mathsf{B}$ be a bicategory and let $f:x_{1}\rightarrow x_{2}$ and
$g:y_{1}\rightarrow y_{2}$ be 1-cells. Then we say that $f$ is orthogonal to
$g$, written $f\mathrel{\bot}g$, if the following diagram of categories is a
weak pullback in the bicategory of categories.

${{\underline{\mathsf{B}}(x_{2},y_{1})}}$${{\underline{\mathsf{B}}(x_{1},y_{1})}}$${{\underline{\mathsf{B}}(x_{2},y_{2})}}$${{\underline{\mathsf{B}}(x_{1},y_{2})}}$$\scriptstyle{f^{\mathsf{pre}}}$$\scriptstyle{g^{\mathsf{post}}}$$\scriptstyle{g^{\mathsf{post}}}$$\scriptstyle{f^{\mathsf{pre}}}$

where the functors $f^{\mathsf{pre}}$ and $g^{\mathsf{post}}$ are given by
precomposition with $f$ and postcomposition with $g$ respectively.

Let us expand on Definition 4.1. Weak pullbacks of categories are given by
iso-comma categories. The objects in the iso-comma category
$\mathsf{F}/_{\cong}\mathsf{G}$ of functors
$\mathsf{F}:\mathsf{C}_{1}\rightarrow\mathsf{C}_{3}$ and
$\mathsf{G}:\mathsf{C}_{2}\rightarrow\mathsf{C}_{3}$ are given by triples
$(x,y,f)$ of objects $x:\mathsf{C}_{1}$ and $y:\mathsf{C}_{2}$ together with
an isomorphism $f:\mathsf{F}\>x\cong\mathsf{G}\>y$. Note that we have a
functor $\mathsf{O}_{(f,g)}:\underline{\mathsf{B}}(x_{2},y_{1})\rightarrow
f^{\mathsf{pre}}/_{\cong}g^{\mathsf{post}}$. The functor $\mathsf{O}_{(f,g)}$
maps 1-cells $h:x_{2}\rightarrow y_{1}$ to the triple $(h\cdot g,f\cdot
h,\alpha_{f,h,g})$ where $\alpha$ is the associator of $\mathsf{B}$.
Orthogonality can equivalently be phrased by saying that the functor
$\mathsf{O}_{(f,g)}$ is an adjoint equivalence. Essential surjectivity of
$\mathsf{O}_{(f,g)}$ says that every square has a diagonal filler as follows.

${{x_{1}}}$${{y_{1}}}$${{x_{2}}}$${{y_{2}}}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{h_{1}}$$\scriptstyle{h_{2}}$$\scriptstyle{l}$

More concretely, given the diagram above, there is a lift $l:x_{2}\rightarrow
y_{1}$ making the two triangles commute up to invertible 2-cell. Fully
faithfulness of $\mathsf{O}_{(f,g)}$ says that whenever we have two lifts
$l_{1},l_{2}:x_{2}\rightarrow y_{1}$ together with 2-cells
$\tau_{1}:l_{1}\cdot g\Rightarrow l_{2}\cdot g$ and $\tau_{2}:f\cdot
l_{1}\Rightarrow f\cdot l_{2}$, we have a unique 2-cell
$\zeta:l_{1}\Rightarrow l_{2}$ such that $\zeta\vartriangleright g=\tau_{1}$
and $f\vartriangleleft\zeta=\tau_{2}$.

######  Definition 4.2.

Let $\mathsf{B}$ be a bicategory. An orthogonal factorization system on
$\mathsf{B}$ consists of two classes of maps, which we denote by $\mathcal{L}$
and $\mathcal{R}$, such that

  * •

$\mathcal{L}$ and $\mathcal{R}$ are closed under invertible 2-cells;

  * •

for all 1-cells $f$ and $g$ such that $\mathcal{L}\>f$ and $\mathcal{R}\>g$,
we have $f\mathrel{\bot}g$;

  * •

for every 1-cell $f$, we have a factorization $f\cong l\cdot r$ such that
$\mathcal{L}\>l$ and $\mathcal{R}\>r$.

In this section, we are interested in a particular factorization system on
$\mathsf{EnrichCat}_{\mathsf{V}}$, which is given by the fully faithful and
the essentially surjective enriched functors.

######  Definition 4.3.

Let $\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ be an enriched
functor.

  * •

We say that $\mathcal{F}$ is fully faithful if for all objects
$x,y:\mathcal{E}_{1}$ the morphism $\mathcal{F}(x,y)$ is an isomorphism.

  * •

We say that $\mathcal{F}$ is essentially surjective if its underlying functor
is essentially surjective. That is to say, for all $y:\mathcal{E}_{2}$ we have
an inhabitant of
$\mathopen{}\left\|\sum(x:\mathcal{E}_{1}),\mathcal{F}\>x\cong
y\right\|\mathclose{}$.

  * •

We say that $\mathcal{F}$ is a weak equivalence if $\mathcal{F}$ is both fully
faithful and essentially surjective.

Every enriched functor can be factorized as an essentially surjective functor
followed by a fully faithful functor by taking the _full image_.

######  Example 4.4.

Let $\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ be an enriched
functor. We define a predicate $\mathsf{P}$ on the objects of
$\mathcal{E}_{2}$ such that
$\mathsf{P}\>y\coloneqq\mathopen{}\left\|\sum(x:\mathcal{E}_{1}),\mathcal{F}\>x\cong
y\right\|\mathclose{}.$ The full image $\mathsf{Im}(\mathcal{F})$ of
$\mathcal{F}$ is defined to be the full subcategory of $\mathcal{E}_{2}$ with
respect to $\mathsf{P}$.

######  $\blacktriangleright$ Proposition 4.5.

Suppose that we have univalent enriched categories
$\mathcal{E}_{1},\mathcal{E}_{2},\mathcal{E}_{3}$, and $\mathcal{E}_{4}$. If
we have enriched functors
$\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ and
$\mathcal{G}:\mathcal{E}_{3}\rightarrow\mathcal{E}_{4}$ such that
$\mathcal{F}$ is essentially surjective and $\mathcal{G}$ is fully faithful,
then $\mathcal{F}\mathrel{\bot}\mathcal{G}$.

######  Problem 4.6.

To construct an orthogonal factorization system on
$\mathsf{EnrichCat}_{\mathsf{V}}$.

$\blacktriangleright$ Construction 4.7 (for Problem 4.6). The classes
$\mathcal{L}$ and $\mathcal{R}$ are given by the essentially surjective and
the fully faithful enriched functors respectively. The desired factorization
is given by Example 4.4, and the proof of orthogonality is given in
Proposition 4.5. It remains to show that essentially surjective and fully
faithful enriched functors are closed under enriched natural isomorphisms, and
the details for that is given in the formalization. ∎

From this factorization system, we directly obtain that weak equivalence are
actually adjoint equivalences.

######  $\blacktriangleright$ Theorem 4.8.

Every fully faithful and essentially surjective enriched functor
$\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ is an adjoint
equivalence.

###### Proof.

Suppose that $\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ is fully
faithful and essentially surjective. Consider the following diagram

${{\mathcal{E}_{1}}}$${{\mathcal{E}_{1}}}$${{\mathcal{E}_{2}}}$${{\mathcal{E}_{2}}}$$\scriptstyle{\mathcal{F}}$$\scriptstyle{\mathcal{F}}$$\scriptstyle{\operatorname{id}{}}$$\scriptstyle{\operatorname{id}{}}$$\scriptstyle{l}$

Due to the orthogonality of fully faithful and essentially surjective
morphisms, this diagram has a lift $l$ such that both triangles commute up to
invertible 2-cell. From this, we get that $f$ is an equivalence, and since
equivalences can be refined to adjoint equivalences, $f$ is an adjoint
equivalence. ∎

######  Remark 4.9.

For the proof of 4.8, we require both the domain and codomain of $\mathcal{F}$
to be univalent. This restriction is a consequence of the bicategorical
machinery, because we phrase everything in the bicategory
$\mathsf{EnrichCat}_{\mathsf{V}}$ whose objects are univalent enriched
categories. In the case that only the domain of $\mathcal{F}$ is univalent,
one would still use the same construction as in Section 4.

##  5 The Rezk Completion

The next aspect in our study of univalent enriched categories, is the
_enriched Rezk completion_. There are two features to a suitable Rezk
completion for enriched categories. First of all, one needs to show that every
enriched category is weakly equivalent to a univalent one (Section 5). This
construction is similar to the Rezk completion of categories [2]: in both
cases, we construct the enriched Rezk completion as the image of the Yoneda
embedding. Note that for Section 5 we assume that $\mathsf{V}$ is a complete
symmetric monoidal closed category to guarantee that we have an enrichment for
the desired presheaf category. Second of all, one needs to prove a universal
property (5.5). This property says that every enriched functor from an
enriched category $\mathcal{E}$ to some univalent enriched category can be
extended to the Rezk completion of $\mathcal{E}$.

Our construction of the enriched Rezk completion makes use of the _Yoneda
lemma_ [12]. As such, we first define representable presheaves and the Yoneda
embedding, and we prove the Yoneda lemma.

######  Definition 5.1.

Let $\mathsf{V}$ be a complete symmetric monoidal closed category, and let
$\mathcal{E}$ be an $\mathsf{V}$-enriched category Given an object
$y:\mathcal{E}$, we define the representable functor
$\mathsf{r}_{0}(y):[\mathcal{E}^{\mathsf{op}},\mathsf{self}(\mathsf{V})]$ as
follows.

  * •

For objects $x:\mathcal{E}$, we define
$\mathsf{r}_{0}(y)\>x\coloneqq\mathcal{E}(x,y)$;

  * •

for morphisms $f:x_{1}\rightarrow x_{2}$, we define $\mathsf{r}_{0}(y)\>f$ to
be $f^{\mathsf{pre}}:\mathcal{E}(x_{2},y)\rightarrow\mathcal{E}(x_{1},y)$.

Given a morphism $f:y_{1}\rightarrow y_{2}$ in $\mathcal{E}$, we define the
representable natural transformation
$\mathsf{r}_{1}(f):\mathsf{r}_{0}(y_{1})\rightarrow\mathsf{r}_{0}(y_{2})$ to
be $f^{\mathsf{post}}:\mathcal{E}(x,y_{1})\rightarrow\mathcal{E}(x,y_{2})$ for
every $x:\mathcal{E}$.

Finally, the enriched Yoneda embedding
$\mathsf{y}_{\mathcal{E}}:\mathcal{E}\rightarrow[\mathcal{E}^{\mathsf{op}},\mathsf{self}(\mathsf{V})]$
is defined to be $\mathsf{r}_{0}(y)$ on objects $y:\mathcal{E}$ and
$\mathsf{r}_{1}(f)$ on morphisms $f:y_{1}\rightarrow y_{2}$.

Note that in Definition 5.1, one also needs to construct
$\mathsf{V}$-enrichments for $\mathsf{r}_{0}(y)$ and
$\mathsf{y}_{\mathcal{E}}$, and prove that $\mathsf{r}_{1}(f)$ is
$\mathsf{V}$-enriched. The details for that can be found in [12] and the
formalization.

######  $\blacktriangleright$ Proposition 5.2.

The enriched Yoneda embedding is fully faithful.

######  Problem 5.3.

Given a category $\mathcal{E}$ enriched over a univalent complete symmetric
monoidal category $\mathsf{V}$, to construct a univalent enriched category
$\mathcal{R}(\mathcal{E})$ and a weak equivalence
$\mathsf{P}:\mathcal{E}\rightarrow\mathcal{R}(\mathcal{E})$.

$\blacktriangleright$ Construction 5.4 (for Problem 5.3). We define
$\mathcal{R}(\mathcal{E})$ to be the image of the Yoneda embedding
$\mathsf{y}_{\mathcal{E}}$. The enriched functor
$\mathsf{P}:\mathcal{E}\rightarrow\mathcal{R}(\mathcal{E})$ is essentially
surjective by construction (Example 4.4). By the Yoneda lemma (Proposition
5.2), $\mathsf{P}$ is fully faithful as well. ∎

Note that Section 5 might increase the universe level. Let us assume that the
type of objects of $\mathcal{E}$ and $\mathsf{V}$ live in $\mathcal{U}$ and
$\mathcal{V}$ respectively. Since objects of $\mathcal{R}(\mathcal{E})$ are
enriched presheaves from $\mathcal{E}$ to $\mathsf{self}(\mathsf{V})$ that are
in the image of $\mathsf{y}_{\mathcal{E}}$, the type of objects of
$\mathcal{R}(\mathcal{E})$ lives in $\mathcal{U}\sqcup\mathcal{V}$. In many
examples, $\mathcal{V}$ is a larger universe that $\mathcal{U}$, because we
require the category $\mathsf{V}$ to have all products indexed by the objects
in $\mathcal{E}$.

Finally, we verify the universal property of the Rezk completion. This
property is formulated using the precomposition functor.

######  $\blacktriangleright$ Theorem 5.5.

Suppose that we have a enriched functor
$\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ and a univalent
enriched category $\mathcal{E}_{3}$. The the precomposition functor
$\mathcal{F}^{\mathsf{pre}}:[\mathcal{E}_{2},\mathcal{E}_{3}]\rightarrow[\mathcal{E}_{1},\mathcal{E}_{3}]$
is an adjoint equivalence of categories.

To verify 5.5, we use that $\mathcal{E}_{3}$ is univalent. This implies that
the categories $[\mathcal{E}_{2},\mathcal{E}_{3}]$ and
$[\mathcal{E}_{1},\mathcal{E}_{3}]$ are both univalent, and thus it suffices
to check that
$\mathcal{F}^{\mathsf{pre}}:[\mathcal{E}_{2},\mathcal{E}_{3}]\rightarrow[\mathcal{E}_{1},\mathcal{E}_{3}]$
is essentially surjective and fully faithful. The proofs of Lemmata 5.6 and
5.7 have some overlap with the ordinary categorical case [2, Theorem 8.4].
However, here we must also check that the obtained functors and natural
transformations actually are enriched.

######  $\blacktriangleright$ Lemma 5.6.

Suppose that we have a enriched functor
$\mathcal{F}:\mathcal{E}_{1}\rightarrow\mathcal{E}_{2}$ and a univalent
enriched category $\mathcal{E}_{3}$. The functor
$\mathcal{F}^{\mathsf{pre}}:[\mathcal{E}_{2},\mathcal{E}_{3}]\rightarrow[\mathcal{E}_{1},\mathcal{E}_{3}]$
is fully faithful.

###### Proof.

The proof that
$\mathcal{F}^{\mathsf{pre}}:[\mathcal{E}_{2},\mathcal{E}_{3}]\rightarrow[\mathcal{E}_{1},\mathcal{E}_{3}]$
is faithful, is in essence the same as for ordinary categories [2, Lemma 8.1],
so we only show that $\mathcal{F}^{\mathsf{pre}}$ is full. Let
$\mathcal{G}_{1},\mathcal{G}_{2}:[\mathcal{E}_{2},\mathcal{E}_{3}]$ be two
enriched functors, and suppose that we have an enriched transformation
$\tau:\mathcal{F}\mathbin{\cdot}\mathcal{G}_{1}\Rightarrow\mathcal{F}\mathbin{\cdot}\mathcal{G}_{2}$.
We show how to construct the desired enriched natural transformation
$\theta:\mathcal{G}_{1}\Rightarrow\mathcal{G}_{2}$.

For all objects $x:\mathcal{E}_{2}$ the following type is contractible.

$\sum(f:\mathcal{G}_{1}\>x\rightarrow\mathcal{G}_{2}\>x),\prod(w:\mathcal{E}_{1})(i:\mathcal{F}\>w\cong
x),\tau\>w\cdot\mathcal{G}_{2}\>i=\mathcal{G}_{1}\>i\cdot f$

The contractibility of this type follows from our assumption that
$\mathcal{F}$ is essentially surjective. From this, we obtain the data of the
the desired transformation $\theta$. The fact that $\theta$ is
$\mathsf{V}$-enriched is shown by using Equation 1 and the fact that
$\mathcal{F}$ is essentially surjective. ∎

######  $\blacktriangleright$ Lemma 5.7.

The functor
$\mathcal{F}^{\mathsf{pre}}:[\mathcal{E}_{2},\mathcal{E}_{3}]\rightarrow[\mathcal{E}_{1},\mathcal{E}_{3}]$
is essentially surjective.

###### Proof.

Suppose that we have an enriched functor
$\mathcal{G}:[\mathcal{E}_{1},\mathcal{E}_{3}]$. We only demonstrate how to
construct the desired enriched functor
$\mathcal{H}:[\mathcal{E}_{2},\mathcal{E}_{3}]$.

Suppose that we have an object $x:\mathcal{E}_{2}$. Then there is a unique
$y:\mathcal{E}_{3}$ and function
$\varphi:\prod(w:\mathcal{E}_{1})(i:\mathcal{F}\>x\cong y),\mathcal{G}\>w\cong
y$ such that for all objects $w_{1},w_{2}:\mathcal{E}_{1}$, isomorphisms
$i_{1}:\mathcal{F}\>w_{1}\cong x$ and $i_{2}:\mathcal{F}\>w_{2}\cong x$, and
morphisms $k:w_{1}\rightarrow w_{2}$ satisfying $\mathcal{F}\>k\cdot
i_{2}=i_{1}$, we have
$\mathcal{G}\>k\cdot\varphi\>w_{2}\>i_{2}=\varphi\>w_{1}\>i_{1}$. The
uniqueness follows from the fact that $\mathcal{F}$ is fully faithful, and the
desired element is constructed by using that $\mathcal{F}$ is essentially
surjective. One can show that the obtained action on objects gives rise to a
functor $H$ from the underlying category of $\mathcal{E}_{2}$ to that of
$\mathcal{E}_{3}$. We also have isomorphisms
$\varphi\>w\>i:\mathcal{G}\>w\cong H\>x$ for all $w:\mathcal{E}_{1}$ and
$i:\mathcal{F}\>x\cong y$.

Next we construct an enrichment for this functor. Suppose, that we have two
objects $x,y:\mathcal{E}_{2}$. Then there is a unique morphism
$f:\mathcal{E}_{2}(x,y)\rightarrow\mathcal{E}_{3}(H\>x,H\>y)$ in $\mathsf{V}$
such that for all objects $w_{1},w_{2}:\mathcal{E}_{2}$ and isomorphisms
$i_{1}:\mathcal{F}\>w_{1}\cong x$ and $i_{2}:\mathcal{F}\>w_{2}\cong x$, $f$
is equal to the following composition of morphisms

${{\mathcal{E}_{2}(x,y)}}$${{\mathcal{E}_{2}(\mathcal{F}\>w_{1},y)}}$${{\mathcal{E}_{2}(\mathcal{F}\>w_{1},\mathcal{F}\>w_{2})}}$${{\mathcal{E}_{1}(w_{1},w_{2})}}$${{\mathcal{E}_{3}(\mathcal{G}\>w_{1},\mathcal{G}\>w_{2})}}$${{\mathcal{E}_{3}(H\>x,\mathcal{G}\>w_{2})}}$${{\mathcal{E}_{3}(H\>x,H\>y)}}$$\scriptstyle{i_{1}^{\mathsf{pre}}}$$\scriptstyle{(i_{2}^{-1})^{\mathsf{pre}}}$$\scriptstyle{(\mathcal{F})^{-1}}$$\scriptstyle{\mathcal{G}}$$\scriptstyle{((\varphi\>w_{1}\>i_{1})^{-1})^{\mathsf{pre}}}$$\scriptstyle{\varphi\>w_{2}\>i_{2}^{\mathsf{post}}}$

This follows from the fact that $\mathcal{F}$ is a weak equivalence. As such,
we get the desired enriched functor
$\mathcal{H}:[\mathcal{E}_{2},\mathcal{E}_{3}]$. ∎

##  6 Enriched Monads

We end our study of univalent enriched categories by looking at enriched
monads. More specifically, we discuss Kleisli objects (Section 6) in the
bicategory of enriched categories. At first glance, it might not seem that
univalence plays an interesting role, but upon closer look, this question is
rather subtle.

Usually, the Kleisli category of a monad $\mathsf{T}$ on a category
$\mathsf{C}$ is defined to be the category whose objects are objects of
$\mathsf{C}$ and whose morphisms from $x$ to $y$ are morphisms
$x\rightarrow\mathsf{T}\>y$ in $\mathsf{C}$. We denote this category by
$\mathsf{K}(\mathsf{T})$. In general, this category is not univalent (for
example the constant monad on the unit set). This situation can be rectified
by defining the Kleisli category in a slightly different way [4], namely as
the image of the free algebra functor from $\mathsf{C}$ to the Eilenberg-Moore
category $\mathsf{EM}(\mathsf{T})$ of $\mathsf{T}$. The resulting univalent
category is denoted by $\mathsf{Kleisli}(\mathsf{T})$. To derive the usual
theorems about Kleisli categories, one can instantiate the formal theory of
monads [13, 27, 30], meaning that it suffices to prove the universal property
for Kleisli objects. Proving the desired universal property is a nice exercise
using the universal property of the Rezk completion (5.5).

The key notion of this section, enriched monads, can be defined concisely as
monads internal to $\mathsf{EnrichCat}_{\mathsf{V}}$. Recall that monads in
bicategories are defined as follows.

######  Definition 6.1.

Let $\mathsf{B}$ be a bicategory. A monad $m$ in $\mathsf{B}$ is given by

  * •

an object $\mathsf{ob}_{m}:\mathsf{B}$;

  * •

a 1-cell $\mathsf{mor}_{m}:\mathsf{ob}_{m}\rightarrow\mathsf{ob}_{m}$;

  * •

a 2-cell $\mathsf{\eta}_{m}:\operatorname{id}_{\mathsf{ob}_{m}}\Rightarrow m$;

  * •

a 2-cell $\mathsf{\mu}_{m}:m\mathbin{\cdot}m\Rightarrow m$.

such that the following diagrams commute.

${{\mathsf{mor}_{m}}}$${{\mathsf{mor}_{m}\mathbin{\cdot}\operatorname{id}{x}}}$${{\mathsf{mor}_{m}\mathbin{\cdot}\mathsf{mor}_{m}}}$${{\operatorname{id}\mathbin{\cdot}\mathsf{mor}_{m}}}$${{\mathsf{mor}_{m}}}$${{\mathsf{mor}_{m}}}$$\scriptstyle{\mathsf{\mu}_{m}}$$\scriptstyle{\mathsf{mor}_{m}\vartriangleleft\mathsf{\eta}_{m}}$$\scriptstyle{\rho^{-1}}$$\scriptstyle{\operatorname{id}}$$\scriptstyle{\lambda^{-1}}$$\scriptstyle{\mathsf{\eta}_{m}\vartriangleright\mathsf{mor}_{m}}$$\scriptstyle{\operatorname{id}}$
${{\mathsf{mor}_{m}\mathbin{\cdot}(\mathsf{mor}_{m}\mathbin{\cdot}\mathsf{mor}_{m})}}$${{\mathsf{mor}_{m}\mathbin{\cdot}\mathsf{mor}_{m}}}$${{(\mathsf{mor}_{m}\mathbin{\cdot}\mathsf{mor}_{m})\mathbin{\cdot}\mathsf{mor}_{m}}}$${{\mathsf{mor}_{m}\mathbin{\cdot}\mathsf{mor}_{m}}}$${{\mathsf{mor}_{m}}}$$\scriptstyle{\mathsf{\mu}_{m}}$$\scriptstyle{\mathsf{\mu}_{m}}$$\scriptstyle{\mathsf{\mu}_{m}\vartriangleright\mathsf{mor}_{m}}$$\scriptstyle{\alpha}$$\scriptstyle{\mathsf{mor}_{m}\vartriangleleft\mathsf{\mu}_{m}}$

For enriched categories, one can further unfold this definition and phrase it
in terms of enrichments. This results in the notion of _enrichments for
monads_.

######  Definition 6.2.

Suppose that we have a category $\mathsf{C}$, a monad $\mathsf{T}$ on
$\mathsf{C}$, and a $\mathsf{V}$-enrichment for $\mathsf{C}$. Then a
$\mathsf{V}$-enrichment for $\mathsf{T}$ consists of a $\mathsf{V}$-enrichment
for the endofunctor $\mathsf{T}$ such that the unit $\eta_{\mathsf{T}}$ and
multiplication $\mu_{\mathsf{T}}$ are $\mathsf{V}$-enriched natural
transformations.

When we say _enriched monad_ , we mean a monad together with an enrichment. In
the remainder of this section, we are concerned with _Kleisli objects_ in the
bicategory of enriched categories. To define Kleisli objects, we first define
their cocones. Note that for these definitions, we talk about arbitrary
bicategories $\mathsf{B}$ and monads internal to $\mathsf{B}$.

######  Definition 6.3.

Let $\mathsf{B}$ be a bicategory and let $m$ be a monad in $\mathsf{B}$. A
Kleisli cocone $k$ for $m$ in $\mathsf{B}$ consists of an object
$\mathsf{ob}_{k}:\mathsf{B}$, a 1-cell
$\mathsf{mor}_{k}:\mathsf{ob}_{m}\rightarrow\mathsf{ob}_{k}$, and a 2-cell
$\mathsf{cell}_{k}:m\mathbin{\cdot}\mathsf{mor}_{k}\Rightarrow\mathsf{mor}_{k}$
such that the following diagrams commute.

${{\operatorname{id}{\mathsf{ob}_{m}}\mathbin{\cdot}\mathsf{mor}_{k}}}$${{m\mathbin{\cdot}\mathsf{mor}_{k}}}$${{\mathsf{mor}_{k}}}$$\scriptstyle{\mathsf{\eta}_{m}\vartriangleright\mathsf{mor}_{k}}$$\scriptstyle{\mathsf{cell}_{k}}$$\scriptstyle{\lambda}$
${{(m\mathbin{\cdot}m)\mathbin{\cdot}\mathsf{mor}_{k}}}$${{m\mathbin{\cdot}(m\mathbin{\cdot}\mathsf{mor}_{k})}}$${{m\mathbin{\cdot}\mathsf{mor}_{k}}}$${{m\mathbin{\cdot}\mathsf{mor}_{k}}}$${{\mathsf{mor}_{k}}}$$\scriptstyle{\mathsf{\mu}_{m}\vartriangleright\mathsf{mor}_{k}}$$\scriptstyle{\alpha^{-1}}$$\scriptstyle{m\vartriangleleft\mathsf{cell}_{k}}$$\scriptstyle{\mathsf{cell}_{k}}$$\scriptstyle{\mathsf{cell}_{k}}$

######  Definition 6.4.

A Kleisli cocone $k$ is universal if the following conditions are satisfied.

  * •

For every Kleisli cocone $q$ there is a 1-cell
$\mathsf{Kl}_{\mathsf{mor}}(q):\mathsf{ob}_{k}\rightarrow\mathsf{ob}_{q}$ and
an invertible 2-cell
$\mathsf{Kl}_{\mathsf{com}}(q):\mathsf{mor}_{k}\mathbin{\cdot}\mathsf{Kl}_{\mathsf{mor}}(q)\Rightarrow\mathsf{mor}_{q}$
such that the following diagram commutes.

${{m\mathbin{\cdot}(\mathsf{mor}_{k}\mathbin{\cdot}\mathsf{Kl}_{\mathsf{mor}}(q))}}$${{m\mathbin{\cdot}\mathsf{mor}_{q}}}$${{(m\mathbin{\cdot}\mathsf{mor}_{k})\mathbin{\cdot}\mathsf{Kl}_{\mathsf{mor}}(q)}}$${{\mathsf{mor}_{k}\mathbin{\cdot}\mathsf{Kl}_{\mathsf{mor}}(q)}}$${{\mathsf{mor}_{q}}}$$\scriptstyle{m\vartriangleleft\mathsf{Kl}_{\mathsf{com}}(q)}$$\scriptstyle{\alpha}$$\scriptstyle{\mathsf{cell}_{k}\vartriangleright\mathsf{Kl}_{\mathsf{mor}}(q)}$$\scriptstyle{\mathsf{Kl}_{\mathsf{com}}(q)}$$\scriptstyle{\mathsf{cell}_{q}}$

  * •

Suppose that we have an object $x:\mathsf{B}$, two 1-cells
$g_{1},g_{2}:\mathsf{ob}_{k}\rightarrow x$, and a 2-cell
$\tau:\mathsf{mor}_{k}\mathbin{\cdot}g_{1}\Rightarrow\mathsf{mor}_{k}\mathbin{\cdot}g_{2}$
such that the following diagram commutes.

${{m\mathbin{\cdot}(\mathsf{mor}_{k}\mathbin{\cdot}g_{1})}}$${{(m\mathbin{\cdot}\mathsf{mor}_{k})\mathbin{\cdot}g_{1}}}$${{\mathsf{mor}_{k}\mathbin{\cdot}g_{1}}}$${{m\mathbin{\cdot}(\mathsf{mor}_{k}\mathbin{\cdot}g_{2})}}$${{(m\mathbin{\cdot}\mathsf{mor}_{k})\mathbin{\cdot}g_{2}}}$${{\mathsf{mor}_{k}\mathbin{\cdot}g_{2}}}$$\scriptstyle{\alpha}$$\scriptstyle{\mathsf{cell}_{k}\vartriangleright
g_{1}}$$\scriptstyle{\tau}$$\scriptstyle{m\vartriangleleft\tau}$$\scriptstyle{\alpha}$$\scriptstyle{\mathsf{cell}_{k}\vartriangleright
g_{2}}$

Then there is a unique 2-cell
$\mathsf{Kl}_{\mathsf{cell}}(\tau):g_{1}\Rightarrow g_{2}$ such that
$\mathsf{cell}_{k}\vartriangleleft\mathsf{Kl}_{\mathsf{cell}}(\tau)=\tau$.

We say that a bicategory has Kleisli objects if there is a universal Kleisli
cocone for every monad $m$.

As discussed before, there are multiple ways to define Kleisli categories. We
first define an enrichment for $\mathsf{K}(\mathsf{T})$.

######  Example 6.5.

Let $\mathsf{T}$ be an enriched monad on an enriched category $\mathcal{E}$.
We define a $\mathsf{V}$-enrichment $\mathsf{K}_{\mathsf{e}}(\mathsf{T})$ for
$\mathsf{K}(\mathsf{T})$ as follows.

  * •

We define $\mathsf{K}_{\mathsf{e}}(\mathsf{T})(x,y)$ to be
$\mathcal{E}(x,\mathsf{T}\>y)$.

  * •

We define $\mathsf{id}^{\mathsf{e}}(x)$ to be
$\overrightarrow{\eta_{\mathsf{T}}\>x}$.

  * •

We define $\mathsf{comp}(x,y,z)$ as the following composition of morphisms.

${{\mathcal{E}(y,\mathsf{T}\>z)\otimes\mathcal{E}(x,\mathsf{T}\>y)}}$${{\mathcal{E}(\mathsf{T}\>y,\mathsf{T}\>(\mathsf{T}\>z))\otimes\mathcal{E}(x,\mathsf{T}\>y)}}$${{\mathcal{E}(x,\mathsf{T}\>(\mathsf{T}\>z))}}$${{\mathcal{E}(x,\mathsf{T}\>z)}}$$\scriptstyle{\mathsf{comp}}$$\scriptstyle{\mathsf{T}\otimes\operatorname{id}{}}$$\scriptstyle{(\mu_{\mathsf{T}}\>z)^{\mathsf{post}}}$

The operations $\overrightarrow{f}$ and $\overleftarrow{f}$ in
$\mathsf{K}_{\mathsf{e}}(\mathsf{T})$ are inherited from $\mathcal{E}$.

Next we define an enrichment for $\mathsf{Kleisli}(\mathsf{T})$. Since
$\mathsf{Kleisli}(\mathsf{T})$ is defined as a full subcategory of the
Eilenberg-Moore category $\mathsf{EM}(\mathsf{T})$, we define an enrichment
for $\mathsf{EM}(\mathsf{T})$ first.

######  Example 6.6.

Suppose that $\mathsf{V}$ has equalizers, and let $\mathsf{T}$ be an enriched
monad on an enriched category $\mathcal{E}$. Note that we can define the
Eilenberg-Moore category of $\mathsf{T}$ as a full subcategory of
$\mathsf{Dialg}(\mathsf{T},\operatorname{id})$. By Examples 3.4 and 3.2 we
obtain the desired $\mathsf{V}$-enrichment
$\mathsf{EM}_{\mathsf{e}}(\mathsf{T})$ on $\mathsf{EM}(\mathsf{T})$.

Using Example 6.6 one can show that $\mathsf{EnrichCat}_{\mathsf{V}}$ has
Eilenberg-Moore objects. In general, we have an enriched functor
$\mathsf{FreeAlg}_{\mathsf{T}}:\mathcal{E}\rightarrow\mathsf{EM}_{\mathsf{e}}(\mathsf{T})$.
This functor sends every object $x$ to the free algebra $\mathsf{T}\>x$. Now
we define an enrichment for $\mathsf{Kleisli}(\mathsf{T})$.

######  Example 6.7.

Suppose that $\mathsf{V}$ is a monoidal category with equalizers, and let
$\mathsf{T}$ be an enriched monad on an enriched category $\mathcal{E}$. Note
that $\mathsf{Kleisli}(\mathsf{T})$ is constructed as a full subcategory of
the Eilenberg-Moore category. Since the Eilenberg-Moore category can be
constructed as a category category of dialgebras, we obtain the
$\mathsf{V}$-enrichment $\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})$ for
$\mathsf{Kleisli}(\mathsf{T})$ from Examples 3.2 and 3.4.

The category defined in Example 6.7 is univalent if we assume $\mathcal{E}$ to
be univalent. This is because the Eilenberg-Moore category of a monad on a
univalent category is always univalent and because univalence is preserved
under full subcategories. In addition, note that in Example 6.7 we assume that
$\mathsf{V}$ has equalizers, whereas in Example 6.5, we do not.

We finish this section by showing that
$\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})$ satisfies the required universal
property. The main idea behind the proof is that we have a weak equivalence
$\mathsf{incl}_{\mathsf{T}}:\mathsf{K}_{\mathsf{e}}(\mathsf{T})\rightarrow\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})$,
and this weak equivalence allows use to instantiate 5.5.

######  Problem 6.8.

Given a monoidal category $\mathsf{V}$ with equalizers, to construct Kleisli
objects in the bicategory $\mathsf{EnrichCat}_{\mathsf{V}}$.

$\blacktriangleright$ Construction 6.9 (for Problem 6.8). Given an enriched
monad $\mathsf{T}$ on $\mathcal{E}$, the Kleisli object of $\mathsf{T}$ in
$\mathsf{EnrichCat}_{\mathsf{V}}$ is given by
$\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})$. The main work lies in verifying
the universal property. This check happens in three steps.

First, we define a weak equivalence
$\mathsf{incl}_{\mathsf{T}}:\mathsf{K}_{\mathsf{e}}(\mathsf{T})\rightarrow\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})$.
This enriched functor sends every object $x$ to the free algebra on $x$. The
action on morphisms is given by the following composition

${{\mathcal{E}(x,\mathsf{T}\>y)}}$${{\mathcal{E}(\mathsf{T}\>x,\mathsf{T}\>(\mathsf{T}\>y))}}$${{\mathcal{E}(\mathsf{T}\>x,\mathsf{T}\>y)}}$$\scriptstyle{\mathsf{T}}$$\scriptstyle{(\mu_{y})^{\mathsf{post}}}$

Second, we check that $\mathsf{K}_{\mathsf{e}}(\mathsf{T})$ gives rise to
Kleisli objects in the bicategory of (not necessarily univalent) enriched
categories. For this, one can use the same proof as used, for example, by
Street [27, Theorem 15].

Third, we conclude that the universal property also holds for
$\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})$, and we only show how to construct
1-cells arising from the mapping property. Suppose, that we have some Kleisli
cocone $q$ in $\mathsf{EnrichCat}_{\mathsf{V}}$. We get an enriched functor
$\mathcal{F}:\mathsf{K}_{\mathsf{e}}(\mathsf{T})\rightarrow\mathsf{ob}_{q}$.
From 5.5, we get the desired 1-cell
$\tilde{\mathcal{F}}:\mathsf{Kleisli}_{\mathsf{e}}(\mathsf{T})\rightarrow\mathsf{ob}_{q}$.
∎

Note the similarities between Section 6 and the construction of Kleisli
objects for univalent categories [30, Construction 6.10].

##  7 Conclusion

In this paper, we studied univalent enriched categories, and we discussed
several aspects of their study. First, we proved a structure identity
principle for univalent enriched categories, which we formulated using
univalent bicategories. The proof used displayed bicategories. Second, we
showed that all weak equivalences between univalent enriched categories are
adjoint equivalences. Here we made us of orthogonal factorization systems.
Third, we discussed the Rezk completion of enriched categories, which we
constructed using the Yoneda lemma. We also used the Rezk completion to
construct Kleisli objects in the bicategory of univalent enriched categories.

There are several ways to extend the results in this paper. A wide variety of
notions in category theory can be defined internally to a bicategory. However,
for enriched categories, these internal notions are not always the correct
ones. For example, the notion of a fully faithful 1-cell can be defined
internally to a bicategory using a representable definition, but the obtained
notion does not correspond to the one given in Definition 4.3. To obtain the
desired notions, one could use the theory of equipments [37], and one
interesting extension of this work would be to develop the equipment of
enriched categories. This requires developing the theory of enriched
profunctors and extending the work by Van der Weide, Rasekh, Ahrens, and North
[31] to incorporate Verity double bicategories [32]. Another interesting
extension would be formalizing applications of enriched categories, such as
models of the enriched effect calculus [7] or enriched profunctor optics [6].

## References

  * [1] Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide.  Bicategories in univalent foundations.  Mathematical Structures in Computer Science, page 1–38, 2022.  doi:10.1017/S0960129522000032.
  * [2] Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman.  Univalent categories and the Rezk completion.  Mathematical Structures in Computer Science, 25:1010–1039, 2015\.  arXiv:1303.0584, doi:10.1017/S0960129514000486.
  * [3] Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert.  Displayed monoidal categories for the semantics of linear logic.  In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 260–273. ACM, 2024.  doi:10.1145/3636501.3636956.
  * [4] Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis.  The univalence principle.  CoRR, abs/2102.06275, 2021.  URL: https://arxiv.org/abs/2102.06275, arXiv:2102.06275.
  * [5] Alexander Campbell.  Skew-enriched categories.  Appl. Categ. Structures, 26(3):597–615, 2018.  doi:10.1007/s10485-017-9504-0.
  * [6] Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregiàn, Bartosz Milewski, Emily Pillmore, and Mario Román.  Profunctor optics, a categorical update.  CoRR, abs/2001.07488, 2020.  URL: https://arxiv.org/abs/2001.07488, arXiv:2001.07488.
  * [7] Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson.  The enriched effect calculus: syntax and semantics.  J. Log. Comput., 24(3):615–654, 2014.  doi:10.1093/logcom/exs025.
  * [8] David Gepner and Rune Haugseng.  Enriched $\infty$-categories via non-symmetric $\infty$-operads.  Adv. Math., 279:575–716, 2015.  doi:10.1016/j.aim.2015.02.007.
  * [9] Paul G. Goerss and John F. Jardine.  Simplicial homotopy theory.  Modern Birkhäuser Classics. Birkhäuser Verlag, Basel, 2009.  Reprint of the 1999 edition [MR1711612].  doi:10.1007/978-3-0346-0189-4.
  * [10] Jason Z. S. Hu and Jacques Carette.  Formalizing category theory in Agda.  In Catalin Hritcu and Andrei Popescu, editors, CPP ’21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 327–342. ACM, 2021.  doi:10.1145/3437992.3439922.
  * [11] Krzysztof Kapulkin and Peter LeFanu Lumsdaine.  The Simplicial Model of Univalent Foundations (after Voevodsky).  Journal of the European Mathematical Society, 23(6):2071–2126, 2021\.  doi:10.4171/JEMS/1050.
  * [12] Max Kelly.  Basic concepts of enriched category theory, volume 64.  CUP Archive, 1982.
  * [13] Stephen Lack and Ross Street.  The formal theory of monads. II.  volume 175, pages 243–265. 2002.  Special volume celebrating the 70th birthday of Professor Max Kelly.  doi:10.1016/S0022-4049(02)00137-8.
  * [14] Tom Leinster.  A survey of definitions of $n$-category.  Theory Appl. Categ., 10:1–70, 2002.
  * [15] Fosco Loregian and Emily Riehl.  Categorical notions of fibration.  Expo. Math., 38(4):496–514, 2020.  doi:10.1016/j.exmath.2019.02.004.
  * [16] Saunders Mac Lane.  Categories for the working mathematician, volume 5.  Springer Science & Business Media, 2013.
  * [17] Per Martin-Löf.  Intuitionistic type theory, volume 1 of Studies in proof theory.  Bibliopolis, 1984.
  * [18] The mathlib Community.  The Lean mathematical library.  In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 367–381. ACM, 2020.  doi:10.1145/3372885.3373824.
  * [19] Dylan McDermott and Alan Mycroft.  Galois connecting call-by-value and call-by-name.  In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 32:1–32:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.32, doi:10.4230/LIPICS.FSCD.2022.32.
  * [20] Dylan McDermott and Tarmo Uustalu.  What makes a strong monad?  In Jeremy Gibbons and Max S. New, editors, Proceedings Ninth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022, volume 360 of EPTCS, pages 113–133, 2022.  doi:10.4204/EPTCS.360.6.
  * [21] Eugenio Moggi.  Computational lambda-calculus and monads.  In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989, pages 14–23. IEEE Computer Society, 1989.  doi:10.1109/LICS.1989.39155.
  * [22] Ulf Norell.  Dependently typed programming in Agda.  In Proceedings of the 4th international workshop on Types in language design and implementation, pages 1–2, 2009.
  * [23] Gordon Plotkin and John Power.  Notions of computation determine monads.  In International Conference on Foundations of Software Science and Computation Structures, pages 342–356. Springer, 2002.
  * [24] Gordon Plotkin and John Power.  Algebraic operations and generic effects.  Applied categorical structures, 11(1):69–94, 2003.
  * [25] John Power.  Models for the computational lambda-calculus.  In Ted Hurley, Mícheál Mac an Airchinnigh, Michel P. Schellekens, and Anthony Karel Seda, editors, First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2000, Cork, Ireland, July 20-21, 2000, volume 40 of Electronic Notes in Theoretical Computer Science, pages 288–301. Elsevier, 2000.  doi:10.1016/S1571-0661(05)80056-8.
  * [26] Egbert Rijke.  Introduction to homotopy type theory.  arXiv preprint arXiv:2212.11082, 2022.
  * [27] Ross Street.  The formal theory of monads.  J. Pure Appl. Algebra, 2(2):149–168, 1972.  doi:10.1016/0022-4049(72)90019-9.
  * [28] The Coq Development Team.  The Coq Proof Assistant, September 2022.  doi:10.5281/zenodo.7313584.
  * [29] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [30] Niels van der Weide.  The formal theory of monads, univalently.  In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 6:1–6:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.6, doi:10.4230/LIPICS.FSCD.2023.6.
  * [31] Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North.  Univalent double categories.  In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 246–259. ACM, 2024.  doi:10.1145/3636501.3636955.
  * [32] Dominic Verity.  Enriched categories, internal categories and change of base.  Repr. Theory Appl. Categ., (20):1–266, 2011.
  * [33] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al.  Unimath — a computer-checked library of univalent mathematics.  available at http://unimath.org.  URL: https://github.com/UniMath/UniMath, doi:10.5281/zenodo.8427604.
  * [34] Mitchell Wand.  Fixed-point constructions in order-enriched categories.  Theor. Comput. Sci., 8:13–30, 1979.  doi:10.1016/0304-3975(79)90053-7.
  * [35] Charles A. Weibel.  An introduction to homological algebra, volume 38 of Cambridge Studies in Advanced Mathematics.  Cambridge University Press, Cambridge, 1994.  doi:10.1017/CBO9781139644136.
  * [36] John Wiegley.  category-theory: Category Theory in Coq, 2023.  URL: https://github.com/jwiegley/category-theory.
  * [37] R. J. Wood.  Abstract pro arrows I.  Cahiers de topologie et géométrie différentielle, 23(3):279–290, 1982.