We study the formal theory of monads, as developed by Street, in univalent foundations.
This allows us to formally reason about various kinds of monads on the right level of abstraction.
In particular, we define the bicategory of monads internal to a bicategory, and prove its univalence.
We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects.
Finally, we relate monads and adjunctions in arbitrary bicategories.
Our work is formalized in Coq using the library.

§ INTRODUCTION

Monads are ubiquitous in both mathematics and computer science, and many different kinds of monads have been considered in various settings.
In functional programming, monads are used to capture computational effects [22].
Strong monads have been used to provide semantics of programming languages such as Moggi's computational $\lambda$-calculus [33, 34] and models of call-by-push-value [29].
Monads are also used in algebra to represent algebraic theories, and in fact, the class of algebraic theories is equivalent to a class of monads [20].
This result has been adapted to the enriched case as well in order to relate various notions of computations with enriched monads [37, 38, 40].
Comonads, the dual notion of monads, have also found applications: symmetric monoidal comonads are used in the semantics of linear logic [32].

A general setting in which all these different variations of monads can be studied, has been developed by Street [45].
This setting, known as the formal theory of monads, uses the fact that the notion of monad can be defined internal to an arbitrary bicategory [12], including 2-categories (which were used by Street).
Each of the aforementioned kinds of monads is actually an instance of this more general notion.
For example, monads in the bicategory of symmetric monoidal categories are symmetric monoidal monads, and strong monads are monads in the bicategory of so-called left actegories [14].
Comonads in a bicategory $\B$ are the same as monads in $\cobicat{\B}$, which is $\B$ with the 2-cells reversed.
Even several kinds of distributive laws, including mixed distributive laws  [13, 42] and iterated distributive laws [15], are instances of this notion of monad.
An overview of the different kinds of monads internal to various bicategories can be found in Table <ref>.
As such, the formal theory of monads provides a good setting to study monads with the right level of abstraction.

Bicategory                                     Notion of monad

Symmetric monoidal categories     Symmetric monoidal monad

Actegories [14]                                   Strong monad

Enriched categories [24]                     Enriched monad

Bicategory of monads                  Distributive law

Various notions of monads

In this paper, we work in univalent foundations [48].
Univalent foundations is an extension of intensional type theory with the univalence axiom.
Roughly speaking, this axiom says that equivalent types are equal.
More precisely, we have a map $\idtoequiv$ that sends identities $X = Y$ to equivalences from $X$ to $Y$, and the univalence axiom states that $\idtoequiv$ is an equivalence itself.
This axiom has numerous effects on the mathematics in this foundation.
One consequence is function extensionality and another is that identity types must necessarily be proof relevant: since there could be multiple equivalence between two types, we could have different proofs of their equality.

In addition, the notion of category studied in this setting is that of univalent categories [3].
A univalent category is a category in which isomorphic objects are equal.
More precisely, for all objects $x$ and $y$ in a category $\C$, we have a map $\idtoiso{x}{y} : x = y \rightarrow x \cong y$, and $\C$ is called univalent if $\idtoiso{x}{y}$ is an equivalence for all $x, y : \C$.
From the univalence axiom, one can deduce that the category of sets is univalent.
The reason why this notion is interesting, is because in the set-theoretical semantics [23], univalent categories correspond to categories in set theory.
Furthermore, every property expressible in type theory about univalent categories is closed under equivalence.
For a more detailed exposition of univalent category theory, we refer the reader to the literature [3].

However, there are some challenges when working with univalent categories.
For instance, the usual definition of the Kleisli category [30] does not give rise to a univalent category.
Given a monad $m$ on $\C$, we define $\kleisli{m}$ as the category whose objects are objects $x : \C$ and whose morphisms from $x$ to $y$ are morphisms $x \onecell m(y)$ in $\C$.
However, even if $\C$ is univalent, the category $\kleisli{m}$ is not guaranteed to be univalent as well.
The technical reason is that isomorphisms in $\kleisli{m}$ are not the same as isomorphisms in $\C$.
Therefore, $\kleisli{m}$ does not actually define a Kleisli category in univalent foundations.
A solution to this problem has already been given: we need to use its Rezk completion [8].
However, the necessary theorems about the Kleisli category (e.g., every monad gives rise to an adjunction via the Kleisli category) have not been proven in that work.

In the present paper, we study and formalize the formal theory of monads by Street [45] in univalent foundations.
More specifically, we formalize the key notions, which are the bicategory of monads and Eilenberg-Moore objects, in univalent foundations, and we illustrate them with numerous examples.
We also prove the two main theorems that relate monads to adjunctions: every adjunction gives rise to a monad and in a bicategory with Eilenberg-Moore objects, every monad gives rise to an adjunction.
In addition, we instantiate the formal theory of monads to deduce the main theorems about Kleisli categories.

The abstract setting provided by the formal theory of monads is beneficial for formalization, which is our main motivation for this work.
The main theorems are only proven once in this setting, and afterwards they are instantiated to the relevant cases of interest without the need of reproving anything.

The results in this paper are formalized using the Coq proof assistant [46] over the library [51].
Definitions, theorems, constructions, and examples in this paper are accompanied with a link that points to the relevant definition in the formalization.
For example, Bicategories.Core.Bicatbicat refers to the definition of a bicategory.

Related work

The formal theory of monads was originally developed by Street [45], and later extended by Lack and Street [27].
There are two differences between our work and Street's work.
First of all, Street used strict 2-categories while we use bicategories.
As has already been noticed by Lack [25], this difference is rather minor.
The resulting definitions are similar: the only difference is that associators and unitors have to be put on the right places.
In addition, one can use the coherence theorem [31, 39] to conclude that every bicategory is biequivalent to a strict 2-category.
More fundamental is the second difference: we work in univalent foundations and univalent (bi)categories whereas Street works in set-theoretic foundations.
This affects the development in several ways.
While both bicategories and strict 2-categories have been defined and studied in a univalent setting [2], a coherence theorem is not available.
In addition, since we work in an intensional setting, working with a strict 2-category is not significantly more convenient than working with a bicategory.
The reason for that, is that equality proofs of associativity and unitality are present in terms to guarantee that the whole expression is well-typed.
Another difference is that in our framework, the usual definition of the Kleisli category does not give rise to a univalent category, and we need to work with its Rezk completion instead.
An overview of the main notions in bicategory theory can be found in various sources [12, 21, 26, 28].

Several formalizations have results about bicategory theory.
The coherence theorem [28] is formalized in both Isabelle [35, 44] and Lean [1], but neither of those are based on univalent foundations.
Some notions in bicategory theory have been formalized in Agda [36], namely in 1Lab [47] and the Agda-categories library [19].
However, neither of these cover the formal theory of monads.
We use [51] and its formalization of bicategories [2, 49].
Formalizations on category theory are more plentiful, and an overview can be found in [19].
Within the framework of univalent foundations, there is the HoTT library [11, 18], Agda UniMath [43], and Cubical Agda [50].
Ahrens, Matthes, and Mörtberg formalized monads of categories in [51].
They also defined a notion of signature, that allows for binding, and they showed that every signature gives rise to a monad [5, 6].

We start this paper by recalling some preliminary notions in <ref>.
Next we construct in <ref> the bicategory of monads internal to bicategories and we prove its univalence.
We illustrate the material of <ref> with various examples in <ref>.
In <ref> we discuss Eilenberg-Moore objects.
We follow that up in <ref> by using Kleisli categories to construct Eilenberg-Moore objects in the opposite bicategory.
In <ref> we prove some theorems in this setting.
We prove in <ref> that every adjunction gives rise to a monad and that every monad gives rise to an adjunction under mild assumptions.
In <ref> we define the notion of monadic adjunctions in arbitrary bicategory and we characterize those using monadic adjunctions in categories.
We conclude in <ref>.

§ PRELIMINARIES

In this section, we briefly recall some of the basic notions needed in this paper.
First of all, we use the notions of propositions and sets.
Types $A$ for which we have $x = y$ for all $x, y : A$, are called propositions, and types $A$ for which every $x = y$ is a proposition, are called sets.
In addition, we assume that our foundation supports the propositional truncation: the truncation $\trunc{A}$ is $A$ with all its elements identified.
More concretely, we have a map $A \rightarrow \trunc{A}$ and for all $x, y : \trunc{A}$, we have $x = y$.
Next we discuss some notions from bicategory theory [2, 12, 28], and we start with bicategories.

A bicategory $\B$ consists of a type $\B$ of objects, for every $x, y : \B$ a type $x \onecell y$ of 1-cells, and for every $f, g : x \onecell y$, a set $f \twocell g$.
On this data, we have the following operations:

* For every $x : \B$, a 1-cell $\id{x} : x \onecell x$

* For all 1-cells $f : x \onecell y$ and $g : y \onecell z$, a 1-cell $\comp{f}{g} : x \onecell z$

* For every 1-cell $f : x \onecell y$, a 2-cell $\id{f} : f \twocell f$

* For all 2-cells $\theta : f \twocell g$ and $\tau : g \twocell h$, a 2-cell $\theta \vcomp \tau : f \twocell h$

* For every 1-cell $f : x \onecell y$, invertible 2-cells $\lunitorfull{f} : \comp{\id{x}}{f} \twocell f$ and $\runitorfull{f} : \comp{f}{\id{y}} \twocell f$

* For all 1-cells $f : w \onecell x$, $g : x \onecell y$, and $h : y \onecell z$, an invertible 2-cell $\lassociatorfull{f}{g}{h} : \comp{
(\comp{f}{g})}{h} \twocell \comp{f}{(\comp{g}{h})}$

If the relevant 1-cells are clear from the context, we write $\lunitor{f}$, $\runitor{f}$, and $\lassociator{f}{g}{h}$ instead of $\lunitorfull{f}$, $\runitorfull{f}$, and $\lassociatorfull{f}{g}{h}$ respectively.
We can also whisker 2-cells with 1-cells in two ways.
Given 1-cells and 2-cells as depicted in the diagram on the left below, we have a 2-cell $f \whiskerl \tau : \comp{f}{g_1} \twocell \comp{f}{g_2}$, and from 1-cells and 2-cells as depicted in the diagram on the right below, we get a 2-cell $\tau \whiskerr g : \comp{f_1}{g} \twocell \comp{f_2}{g}$.

\[
\begin{tikzcd}
x & y & z
\arrow["f"', from=1-1, to=1-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "{g_1}", shift left=3, from=1-2, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{g_2}"', shift right=3, from=1-2, to=1-3]
\arrow["\tau", shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=1]
\end{tikzcd}
\quad \quad
\begin{tikzcd}
x & y & z
\arrow["g", from=1-2, to=1-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{f_1}", shift left=3, from=1-1, to=1-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{f_2}"', shift right=3, from=1-1, to=1-2]
\arrow["\tau", shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=1]
\end{tikzcd}
\]

The laws that need to be satisfied, can be found in the literature <cit.>.

Note that we use diagrammatic order for composition instead of compositional order.
We use the notation $\homC{\B}{x}{y}$ for the category whose objects are 1-cells $f : x \onecell y$ and whose morphisms from $f : x \onecell y$ to $g : x \onecell y$ are 2-cells $\tau : f \twocell g$.
Given a 1-cell $f : x \rightarrow y$ and an object $w : \B$, we have a functor $\postcomp{f}{w} : \homC{\B}{w}{x} \onecell \homC{\B}{w}{y}$, which sends a 1-cell $g : w \onecell x$ to $\comp{g}{f}$ and a 2-cell $\tau : g_1 \twocell g_2$ to $\tau \whiskerr f$.

The core example of a bicategory in this paper is $\UnivCat$.
Its objects are univalent categories, the 1-cells are functors, and the 2-cells are natural transformations.
We also have a bicategory $\Cat$ whose objects are (not necessarily univalent) categories, 1-cells are functors, and 2-cells are natural transformations.

In this paper, we also make use of univalent bicategories.
To define this property, we use that between every two objects $x, y : \B$, we have a type $\adjequiv{x}{y}$ of adjoint equivalences between them.
In addition, for all 1-cells $f, g : x \onecell y$, there is a type $\invcell{f}{g}$ of invertible 2-cells between them.
For the precise definition of these notions, we refer the reader to the literature <cit.>.

Let $\B$ be a bicategory

* (Bicategories.Core.Univalenceis_univalent_2_1) Using path induction, we define a function $\idtoisoloc{f}{g} : f = g \rightarrow \invcell{f}{g}$ for all 1-cells $f, g : x \onecell y$. A bicategory is locally univalent if $\idtoisoloc{f}{g}$ is an equivalence for all $f$ and $g$.

* (Bicategories.Core.Univalenceis_univalent_2_0) Using path induction, we define a function $\idtoisoglob{x}{y} : x = y \rightarrow \adjequiv{x}{y}$ for all objects $x$ and $y$. We say that $\B$ is globally univalent if $\idtoisoglob{x}{y}$ is an equivalence for all $x$ and $y$.

* (Bicategories.Core.Univalenceis_univalent_2) A bicategory is univalent if it is both locally and globally univalent.

The bicategory $\UnivCat$ of univalent categories is both locally and globally univalent.
However, $\Cat$, whose objects objects are not required to be univalent, is neither.

If we have a bicategory $\B$, then we define the bicategory $\opbicat{\B}$ by 'reversing the 1-cells' in $\B$.
More precisely, objects are the same as objects in $\B$, 1-cells from $x$ to $y$ in $\opbicat{\B}$ are 1-cells $y \onecell x$ in $\B$, while 2-cells from $f : y \onecell x$ to $g : y \onecell x$ are 2-cells $f \twocell g$ in $\B$.
In addition, from a bicategory $\B$, we obtain $\cobicat{\B}$ by 'reversing the 2-cells'.
Objects and 1-cells in $\cobicat{\B}$ are the same as objects and 1-cells in $\B$ respectively, but a 2-cell from $f$ to $g$ in $\cobicat{\B}$ is a 2-cell $g \twocell f$ in $\B$.
Next we define pseudofunctors.

Let $\B_1$ and $\B_2$ be bicategories.
A pseudofunctor $F : \B_1 \onecell \B_2$ consists of

* A function $F : \B_1 \rightarrow \B_2$;

* For every $x, y : \B_1$ a function that maps $f : x \onecell y$ to $F \> f : F \> x \onecell F \> y$;

* For all 1-cell $f, g : x \onecell y$ a function that maps $\theta : f \twocell g$ to $F \> \theta : F \> f \twocell F \> g$;

* For every $x : \B_1$, an invertible 2-cell $\identitor{F}{x} : \id{F \> x} \twocell F(\id{x})$;

* For all $f : x \onecell y$ and $g : y \onecell z$, an invertible 2-cell $\compositor{F}{f}{g} : \comp{F(f)}{F(g)} \twocell F(\comp{f}{g})$.

The coherencies that need to be satisfied, can be found in the literature <cit.>.

In applications, we are interested in a wide variety of bicategories beside $\UnivCat$, and among those are $\Terminal$ and $\SymMonCat$.
These examples have something in common: their objects are categories equipped with some extra structure, the 1-cells are structure preserving functors, while the 2-cells are structure preserving natural transformations.
We capture this pattern using displayed bicategories.
This notion is an adaptation of displayed categories to the bicategorical setting [4].

To get an idea of what displayed bicategories are, let us first briefly discuss displayed categories.
A displayed category $\D$ over $\C$ represents structure and properties to be added to the objects and morphisms of $\C$.
For every object $x : \C$, we have a type of displayed objects $\D_x$ and for every morphism $f : x \onecell y$ and displayed objects $\disp{x} : \D_x$ and $\disp{y} : \D_y$, we have a set $\dmor{\disp{x}}{\disp{y}}{f}$ of displayed morphisms.
For example, for $\C$ we take the category of sets, and an example of a displayed category would be group structures.
The displayed objects over a set $X$ are group structures over $X$, while the displayed morphisms over $f : X \rightarrow Y$ between two group structures are proofs that $f$ preserves the unit and multiplication.
Every displayed category $\D$ gives rise to a total category $\total{\D}$ and a functor $\proj{\D} : \total{\D} \onecell \C$.
In the example we mentioned before, $\total{\D}$ would be the category of groups and $\proj{\D}$ maps a group to its underlying set.

In the bicategorical setting, we use a similar approach, but a displayed bicategory should not only have displayed objects and 1-cells, but also displayed 2-cells.
More precisely, we define displayed bicategories as follows.

A displayed bicategory $\D$ over a bicategory $\B$ consists of

* For every $x : \B$ a type $\dob{D}{x}$ of displayed objects;

* For all 1-cells $f : x \onecell y$ and displayed objects $\disp{x} : \dob{D}{x}$ and $\disp{y} : \dob{D}{y}$, a type $\dmor{\disp{x}}{\disp{y}}{f}$ of displayed morphisms;

* For all 2-cells $\theta : f \twocell g$ and displayed morphisms $\disp{f} : \dmor{\disp{x}}{\disp{y}}{f}$ and $\disp{g} : \dmor{\disp{x}}{\disp{y}}{g}$ a set $\dtwo{\disp{f}}{\disp{g}}{\theta}$ of displayed 2-cells.

In addition, there are displayed versions of every operation of bicategories.
For example, for every $x : \B$ and $\disp{x} : \dob{D}{x}$, we have the displayed identity $\disp{\id{x}} : \dmor{\disp{x}}{\disp{x}}{\id{x}}$, and from two displayed morphisms $\disp{f} : \dmor{\disp{x}}{\disp{y}}{f}$ and $\disp{g} : \dmor{\disp{y}}{\disp{z}}{g}$ we get a displayed morphism $\comp{\disp{f}}{\disp{g}} : \dmor{\disp{x}}{\disp{z}}{\comp{f}{g}}$.
A list of the operations and laws can be found in the literature <cit.>.

Just like for displayed categories, every displayed bicategory $\D$ gives rise to  bicategory $\total{\D}$ and a pseudofunctor $\total{\D} \onecell \B$.

Given a displayed bicategory $\D$ over $\B$, to construct a bicategory $\total{\D}$ and a pseudofunctor $\proj{\D} : \total{\D} \onecell \B$.

The bicategory $\total{\D}$ is defined as follows:

* Its objects are pairs $x : \B$ together with $\disp{x} : \dob{\D}{x}$

* Its 1-cells from $(x, \disp{x})$ to $(y, \disp{y})$ are pairs $f : x \onecell y$ together with $\disp{f} : \dmor{\disp{x}}{\disp{y}}{f}$

* Its 2-cells from $(f, \disp{f})$ to $(g, \disp{g})$ are pairs $\tau : f \twocell g$ together with $\disp{\tau} : \dtwo{\disp{f}}{\disp{g}}{\tau}$

The pseudofunctor $\proj{\D}$ sends objects $(x, \disp{x})$ to $x$, 1-cells $(f, \disp{f})$ to $f$, and 2-cells $(\theta, \disp{\theta})$ to $\theta$.

Univalent displayed bicategories are defined similarly to univalent bicategories, and the precise definition can be found elsewhere [2].
If we have a displayed bicategory $\D$ over $\B$ and if both $\B$ and $\D$ are univalent, then $\total{\D}$ is univalent as well.
This gives modular way to construct univalent bicategories.

In numerous different examples, we look at displayed bicategories whose displayed 2-cells are actually trivial, in a certain sense.
More precisely, we look at two properties.
One of them expresses that between all displayed 1-cells $\disp{f} : \dmor{\disp{x}}{\disp{y}}{f}$ and $\disp{g} : \dmor{\disp{x}}{\disp{y}}{g}$, there is at most one displayed 2-cell.
That property is called locally propositional: it expresses that the type $\dtwo{\disp{f}}{\disp{g}}{\tau}$ is a proposition.
The other property is locally groupoidal, and it says that every displayed 2-cell over an invertible 2-cell is again invertible.

Let $\D$ be a displayed bicategory over $\B$.

* (Bicategories.DisplayedBicats.DispBicatdisp_2cells_isaprop)We say that $\D$ is locally propositional if for all $\disp{\tau}, \disp{\tau'} : \dtwo{\disp{f}}{\disp{g}}{\tau}$ we have $\disp{\tau} = \disp{\tau'}$.

* (Bicategories.DisplayedBicats.DispBicatdisp_locally_groupoid) We say that $\D$ is locally groupoidal if every $\disp{\tau} : \dtwo{\disp{f}}{\disp{g}}{\tau}$ is invertible where $\tau$ is an invertible 2-cell.

Suppose, we have a bicategory $\B$ and

* For each $x : \B$ a type $\D_x$;

* For every 1-cell $f : x \onecell y$ and elements $\disp{x} : \D_x$ and $\disp{y} : \D_y$ a type $\D_{\disp{x}, \disp{y}, f}$;

* For every $x : \B$ and $\disp{x} : \D_x$ an inhabitant of $\D_{\disp{x}, \disp{x}, \id{x}}$;

* For all $\disp{f} : \D_{\disp{x}, \disp{y}, f}$ and $\disp{g} : \D_{\disp{y}, \disp{z}, g}$ an inhabitant of $\D_{\disp{x}, \disp{z}, \comp{f}{g}}$.

Then we get a displayed bicategory over $\B$ whose 2-cells are inhabitants of the unit type.

Note that every displayed bicategory constructed using <ref> is both locally propositional and locally groupoidal.
Now let us look at some examples of displayed bicategories.
These were already considered in previous work [9, 52].

Using <ref>, we define a displayed bicategory $\dTerminal$ over $\UnivCat$.

* Objects over $\C$ are terminal objects $T_\C$ in $\C$;

* Displayed 1-cells over $F : \C_1 \onecell \C_2$ are proofs that $F$ preserves terminal objects.

We define $\Terminal$ to be $\total{\dTerminal}$.

We define a displayed bicategory $\dMonCat$ over $\UnivCat$ as follows:

* Objects over $\C$ are monoidal structures over $\C$;

* 1-cells over $F : \C_1 \onecell \C_2$ are structures that $F$ is a lax monoidal functor;

* 2-cells over $\theta : F \twocell G$ are proofs that $\theta$ is a monoidal transformation.

We denote its total bicategory by $\MonCat$.

Note that similarly, one can define a displayed bicategory $\dSymMonCat$ over $\UnivCat$ whose total bicategory $\SymMonCat$ is the bicategory of symmetric monoidal categories.
In the remainder of this paper, we use several operations on displayed bicategories.

We have the following operations on displayed bicategories:

* (Bicategories.DisplayedBicats.Examples.Proddisp_dirprod_bicat) Given displayed bicategories $\D_1$ and $\D_2$ over $\B$, we construct a displayed bicategory $\D_1 \times \D_2$ over $\B$ whose objects, 1-cells and 2-cells are pairs of objects, 1-cells, and 2-cells in $\D_1$ and $\D_2$ respectively.

* (Bicategories.DisplayedBicats.Examples.Sigmasigma_bicat) Suppose that we have a displayed bicategory $\D_1$ over $\B$ and a displayed bicategory $\D_2$ over $\total{\D_1}$.
We construct a displayed bicategory $\sigmaD{\D_2}$ over $\B$ by setting the objects over $x$ to be pairs of $(\disp{x}, \disp{\disp{x}})$ of objects $\disp{x} : \dob{D_1}{x}$ and $\disp{\disp{x}} : \dob{\D_2}{(x, \disp{x})}$.

* (Bicategories.DisplayedBicats.Examples.FullSubdisp_fullsubbicat) Let $\B$ be a bicategory and let $P$ be a predicate on the objects of $\B$.
We define a displayed bicategory $\dfullsub{P}$ over $\B$ by setting the displayed objects over $x$ to be proofs of $P(x)$ and the 1-cells and 2-cells are inhabitants of the unit type.

The last notion we discuss, is the notion of a section of a displayed bicategory.
Intuitively, a section assigns to every $x$ a displayed object $\disp{x} : \D_x$ in a pseudofunctorial way.
As such every section $s$ of $\D$ induces a pseudofunctor $\Section{s} : \B \onecell \total{D}$ such that every $x : \B$ is definitionally equal to $\proj{\D}(\Section{s}(x))$.

A section $s$ of $\D$ consists of

* For every object $x : \B$ a displayed object $\sob{s}{x} : \dob{D}{x}$;

* For every 1-cell $f : x \onecell y$ a displayed 1-cell $\smor{s}{f} : \dmor{\sob{s}{x}}{\sob{s}{y}}{f}$;

* For every 2-cell $\theta : f \twocell g$ a displayed 2-cell $\stwo{s}{\theta} : \dtwo{\smor{s}{f}}{\smor{s}{g}}{\theta}$;

* For every $x : \B$ an invertible 2-cell $\sid{s}{x} : \dtwo{\disp{\id{\sob{s}{x}}}}{\smor{s}{\id{x}}}{\id{\id{x}}}$;

* For every $f : x \onecell y$ and $g : y \onecell z$ an invertible 2-cell $\scomp{s}{f}{g} : \dtwo{\comp{\smor{s}{f}}{\smor{s}{g}}}{\smor{s}{\comp{f}{g}}}{\id{\comp{f}{g}}}$.

We also require several coherencies reminiscent of the laws of pseudofunctors, and for a precise description of those, we refer the reader to the formalization.

Given a displayed bicategory $\D$ on $\B$ and a section $s$ on $\D$, to construct a pseudofunctor $\Section{s} : \B \onecell \total{D}$.

We define the pseudofunctor $\Section{s}$ as follows: it sends objects $x$ to the pair $(x, \sob{s}{x})$, 1-cells $f$ to $(f, \sob{s}{f})$, and 2-cells $\tau : f \twocell g$ to $(\tau, \sob{s}{\tau})$.

§ THE BICATEGORY OF MONADS

Two concepts play a key role in the formal theory of monads: the bicategory of monads $\mnd{\B}$ internal to $\B$ and Eilenberg-Moore objects.
In this section, we study the first concept, and we use displayed bicategories to construct the bicategory $\mnd{\B}$ given a bicategory $\B$.
We also show that $\mnd{\B}$ must be univalent if $\B$ is.

The main idea behind the construction is to split up monads in several independent parts.
We first define $\dEndo{\B}$ whose displayed objects over $x$ are 1-cells $e : x \onecell x$.
After that, we define $\dUnit{\B}$ and $\dMult{\B}$ whose displayed objects are the unit and multiplication of the monad respectively.
We finally take a full subcategory for the monad laws.

Let $\B$ be a bicategory.
Define a displayed bicategory $\dEndo{\B}$ over $\B$ as follows:

* The displayed objects over $x$ are 1-cells $e_x : x \onecell x$;

* The displayed 1-cells over $f : x \onecell y$ from $e_x : x \onecell x$ to $e_y : y \onecell y$ are 2-cells $\theta_f$

\[
\begin{tikzcd}
x & x \\
y & y
\arrow[""{name=0, anchor=center, inner sep=0}, "{e_y}"', from=2-1, to=2-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{e_x}", from=1-1, to=1-2]
\arrow["f", from=1-2, to=2-2]
\arrow["f"', from=1-1, to=2-1]
\arrow["{\tau_f}"', shorten <=4pt, shorten >=4pt, Rightarrow, from=0, to=1]
\end{tikzcd}
\]

* The displayed 2-cells over $\tau : f \twocell g$ from $\theta_f : \comp{f}{e_y} \twocell \comp{e_x}{f}$ to $\theta_g : \comp{g}{e_y} \twocell \comp{e_x}{g}$ are proofs that the following diagram commutes

\[
\begin{tikzcd}
{\comp{f}{e_y}} & {\comp{e_x}{f}} \\
{\comp{g}{e_y}} & {\comp{e_x}{g}}
\arrow["{\theta_f}", from=1-1, to=1-2, Rightarrow]
\arrow["{\theta_g}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\tau \whiskerr e_y}"', from=1-1, to=2-1, Rightarrow]
\arrow["{e_x \whiskerl \tau}", from=1-2, to=2-2, Rightarrow]
\end{tikzcd}
\]

We define $\Endo{B}$ by $\total{\dEndo{\B}}$.

Next we define two displayed bicategories over $\Endo{\B}$.
For both, we use <ref>.

Given a bicategory $\B$, we define the displayed bicategory $\dUnit{\B}$ over $\Endo{\B}$ as follows

* The displayed objects over $(x, e_x)$ are 2-cells $\eta_x : \id{x} \twocell e_x$;

* The displayed 1-cells over $(f, \theta_f)$ where $f : x \onecell y$ and $\theta_f : \comp{f}{e_y} \twocell \comp{e_x}{f}$ from $\eta_x : \id{x} \twocell e_x$ to $\eta_y : \id{y} \twocell e_y$ are proofs that the following diagram commutes

\[
\begin{tikzcd}
f && {\comp{\id{x}}{f}} \\
{\comp{f}{\id{y}}} & {\comp{f}{e_y}} & {\comp{e_x}{f}}
\arrow["{\rinvunitor{f}}"', from=1-1, to=2-1, Rightarrow]
\arrow["{f \whiskerl \eta_y}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\theta_f}"', from=2-2, to=2-3, Rightarrow]
\arrow["{\linvunitor{f}}", from=1-1, to=1-3, Rightarrow]
\arrow["{\eta_x \whiskerr f}", from=1-3, to=2-3, Rightarrow]
\end{tikzcd}
\]

Given a bicategory $\B$, we define the displayed bicategory $\dMult{\B}$ over $\Endo{\B}$ as follows

* The displayed objects over $(x, e_x)$ are 2-cells $\mu_x : \comp{e_x}{e_x} \twocell e_x$;

* The displayed 1-cells over $(f, \theta_f)$ where $f : x \onecell y$ and $\theta_f : \comp{f}{e_y} \twocell \comp{e_x}{f}$ from $\mu_x : \comp{e_x}{e_x} \twocell e_x$ to $\mu_y : \comp{e_y}{e_y} \twocell e_y$ are proofs that the following diagram commutes

\[
\begin{tikzcd}
{\comp{f}{(\comp{e_y}{e_y})}} && {\comp{f}{e_y}} && {\comp{e_x}{f}} \\
{\comp{(\comp{f}{e_y})}{e_y}} & {\comp{(\comp{e_x}{f})}{e_y}} & {\comp{e_x}{(\comp{f}{e_y})}} & {\comp{e_x}{(\comp{e_x}{f})}} & {\comp{(\comp{e_x}{e_x})}{f}}
\arrow["{\lassociator{f}{e_y}{e_y}}"', from=1-1, to=2-1, Rightarrow]
\arrow["{\theta_f \whiskerr e_y}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\rassociator{e_x}{f}{e_y}}"', from=2-2, to=2-3, Rightarrow]
\arrow["{e_x \whiskerl \theta_f}"', from=2-3, to=2-4, Rightarrow]
\arrow["{\lassociator{e_x}{e_x}{f}}"', from=2-4, to=2-5, Rightarrow]
\arrow["{\mu_x \whiskerr f}"', from=2-5, to=1-5, Rightarrow]
\arrow["{\theta_f}", from=1-3, to=1-5, Rightarrow]
\arrow["{f \whiskerl \mu_y}", from=1-1, to=1-3, Rightarrow]
\end{tikzcd}
\]

Next we define $\dMndData{\B}$ to be $\sigmaD{\dUnit{\B} \times \dMult{\B}}$ and we denote its total bicategory by $\MndData{\B}$.
To obtain $\mnd{\B}$, we take a full subbicategory.

For a bicategory $\B$, we define the predicate $\isMnd$ over $\MndData{\B}$: given $(x, (e_x, (\eta_x, \mu_x)))$, the following diagrams commute

\[
\begin{tikzcd}[sep=large]
{e_x} & {\comp{e_x}{\id{x}}} & {\comp{e_x}{e_x}} & {\comp{\id{x}}{e_x}} & {e_x} \\
&& {e_x}
\arrow["{\mu_x}", from=1-3, to=2-3, Rightarrow]
\arrow["{e_x \whiskerl \eta_x}", from=1-2, to=1-3, Rightarrow]
\arrow["{\rinvunitor{e_x}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\id{x}}"', from=1-1, to=2-3, Rightarrow]
\arrow["{\linvunitor{e_x}}"', from=1-5, to=1-4, Rightarrow]
\arrow["{\eta_x \whiskerr e_x}"', from=1-4, to=1-3, Rightarrow]
\arrow["{\id{e_x}}", from=1-5, to=2-3, Rightarrow]
\end{tikzcd}
\]

\[
\begin{tikzcd}[row sep = huge]
{\comp{e_x}{(\comp{e_x}{e_x})}} && {\comp{e_x}{e_x}} \\
{\comp{(\comp{e_x}{e_x})}{e_x}} & {\comp{e_x}{e_x}} & {e_x}
\arrow["{\mu_x}", from=1-3, to=2-3, Rightarrow]
\arrow["{\mu_x}"', from=2-2, to=2-3, Rightarrow]
\arrow["{\mu_x \whiskerr e_x}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\lassociator{e_x}{e_x}{e_x}}"', from=1-1, to=2-1, Rightarrow]
\arrow["{e_x \whiskerl \mu_x}", from=1-1, to=1-3, Rightarrow]
\end{tikzcd}
\]

We define $\dmnd{\B}$ to be $\sigmaD{\dfullsub{\isMnd}}$, and we denote its total bicategory by $\mnd{\B}$.

Before we continue, let us discuss the objects, 1-cells, and 2-cells of $\mnd{\B}$, and fix the relevant notation for the remainder of this paper.
This also explains what the displayed objects, 1-cells, and 2-cells in $\dmnd{\B}$ are.
The data of a monad $m$ in $\B$ consists of

* an object $\monadob{m} : \B$;

* a 1-cell $\monadendofull{m} : \monadob{m} \onecell \monadob{m}$;

* a 2-cell $\monadunit{m} : \id{\monadob{m}} \twocell \monadendo{m}$;

* a 2-cell $\monadmult{m} : \comp{\monadendo{m}}{\monadendo{m}} \twocell \monadendo{m}$.

If no confusion arises, we write $\monadendo{m}$ instead of $\monadendofull{m}$.

The data of a monad morphism $f : m_1 \onecell m_2$ between monads $m_1$ and $m_2$ consists of a 1-cell $\monadmorobfull{f} : \monadob{m_1} \onecell \monadob{m_2}$ and a 2-cell $\monadmorendo{f} : \comp{\monadmorob{f}}{\monadendo{m_2}} \twocell \comp{\monadendo{m_1}}{\monadmorob{f}}$.
Lastly, the data of monad 2-cell $\gamma : f_1 \twocell f_2$ between monad morphisms is a 2-cell $\monadcellobfull{\gamma} : \monadmorob{f_1} \twocell \monadmorob{f_2}$.
We write $\monadmorob{f}$ instead of $\monadmorobfull{f}$ and $\monadcellob{\gamma}$ instead of $\monadcellobfull{\gamma}$ if no confusion arises.

Next we look at the univalence of $\mnd{\B}$, and to prove it, we use displayed univalence <cit.>.
This way, it suffices to prove the displayed univalence of $\dEndo{\B}$, $\dUnit{\B}$, and $\dMult{\B}$.
We also need $\B$ to be univalent.

If $\B$ is univalent, then so is $\mnd{\B}$.

We also characterize invertible 2-cells and adjoint equivalences in $\mnd{\B}$.

A 2-cell $\gamma$ between monad morphisms is invertible, if the underlying 2-cell $\monadcellobfull{\gamma} : \monadmorob{f_1} \twocell \monadmorob{f_2}$ is invertible.

Let $\B$ be a univalent bicategory.
A 1-cell $f : m_1 \onecell m_2$ in $\mnd{B}$ is an adjoint equivalence if $\monadmorobfull{f}$ is an adjoint equivalence and $\monadmorendo{f}$ is an invertible 2-cell.

Note that in <ref>, we assume that $\B$ is univalent.
Because of univalence, it suffices to prove this proposition assuming that $\monadmorob{f}$ is the identity 1-cell, which simplifies the involved coherencies.
The same idea can be used to show that pointwise pseudonatural adjoint equivalences are adjoint equivalences in the bicategory of pseudofunctors.

§ EXAMPLES OF MONADS

Next we look at examples of monads, and we start by characterizing monads internal to several bicategories.
Let us start by observing that monads in the bicategory $\UnivCat$ of categories correspond to monads as how they usually are defined in category theory.
However, since this notion of monads is defined in every bicategory, we can also look at other bicategories, such as $\SymMonCat$,and $\Terminal$.

In a wide variety of applications, one is interested in monads in a bicategory of categories with some extra structure.
For example, symmetric monoidal monads are monads internal to the bicategory of symmetric monoidal categories.
Strong monads are monads in the bicategory of left actegories.
The bicategories in these two examples can be constructed as a total bicategory of some displayed bicategory over $\UnivCat$.
To characterize monads in total bicategories, we define displayed monads.

Let $\B$ be a bicategory and let $\D$ be a displayed bicategory over $\B$ and suppose that $\D$ is locally propositional and locally groupoidal.
A displayed monad $\disp{m}$ over a monad $m$ in $\B$ consists of

* a displayed object $\disp{\monadob{m}} : \dob{\D}{\monadob{m}}$;

* a displayed 1-cell $\disp{\monadendo{m}} : \dmor{\disp{\monadob{m}}}{\disp{\monadob{m}}}{\monadendo{m}}$;

* a displayed 1-cell $\disp{\monadunit{m}} : \dtwo{\disp{\id{\monadob{m}}}}{\disp{\monadendo{m}}}{\monadunit{m}}$;

* a displayed 1-cell $\disp{\monadmult{m}} : \dtwo{\comp{\disp{\monadendo{m}}}{\disp{\monadendo{m}}}}{\disp{\monadendo{m}}}{\monadmult{m}}$.

Note that we do not require any coherencies in <ref>, because the involved displayed bicategory needs to be locally propositional.

Given a monad $m$ and a displayed monad $\disp{m}$ over $m$, to construct a monad $\total{m}$ in $\total{D}$.

We construct $\total{m}$ as follows

* We define the object $\monadob{\total{m}}$ to be $(\monadob{m}, \disp{\monadob{m}})$;

* We define the 1-cell $\monadendo{\total{m}}$ to be $(\monadendo{m}, \disp{\monadendo{m}})$;

* We define the unit $\monadunit{\total{m}}$ to be $(\monadunit{m}, \disp{\monadunit{m}})$;

* We define multiplication $\monadmult{\total{m}}$ to be $(\monadmult{m}, \disp{\monadmult{m}})$.

Every displayed monad in $\dTerminal$ over $m$ consists of a terminal object in $\monadob{m}$ and a proof that $\monadendo{m}$ preserves terminal objects.

Displayed monads have also been used by Ahrens, Matthes, and Wullaert to determine monads in the bicategory of left actegories.
Analogously, we can characterize monads in $\SymMonCat$.
Next we look at monads in $\opbicat{\B}$ and $\cobicat{\B}$.

We characterize monads in $\opbicat{\B}$ and $\cobicat{\B}$.

* (Bicategories.Monads.ExamplesMonadsInOp1Bicat) Monads in $\opbicat{\B}$ are the same as monads in $\B$.
However, 1-cells in $\mnd{\opbicat{\B}}$ are different from 1-cells in $\mnd{\B}$.
If we have a 1-cell $f : m_1 \onecell m_2$ in $\mnd{\opbicat{\B}}$, then the cell $\monadmorendo{f}$ gives rise to a 2-cell $\comp{\monadendo{m_2}}{\monadmorob{f}} \twocell \comp{\monadmorob{f}}{\monadendo{m_1}}$.
Hence, 1-cells in $\opbicat{\mnd{\opbicat{\B}}}$ are the same as oplax monad morphisms in $\B$.

* (Bicategories.Monads.ExamplesMonadsInOp2Bicat) Suppose, we have $m : \mnd{\cobicat{\B}}$.
Then $\monadob{m} : \B$ and we also have a 1-cell $\monadendo{m} : \monadob{m} \onecell \monadob{m}$ in $\B$.
However, since the direction of the 2-cells are reversed in $\cobicat{\B}$, the 2-cells $\monadunit{m}$ and $\monadmult{m}$ give rise to a 2-cell $\monadendo{m} \twocell \id{\monadob{m}}$ and $\monadendo{m} \twocell \comp{\monadendo{m}}{\monadendo{m}}$ respectively.
As such, monads in $\cobicat{\B}$ are the same as comonads in $\B$.

Objects in $m : \mnd{\mnd{\B}}$ are distributive laws between monads.
To see why, observe that the object $\monadob{m}$ is a monad in $\B$.
In addition, we can construct another monad $m'$ in $\B$ as follows:

* The object $\monadob{m'}$ is $\monadob{\monadob{m}}$;

* The endomorphism is $\monadmorob{\monadendo{m}}$, which is a 1-cell from $\monadob{\monadob{m}}$ to $\monadob{\monadob{m}}$;

* The unit and multiplication are the underlying 2-cells of $\monadunit{m}$ and $\monadmult{m}$ respectively.

The 2-cell $\monadmorendo{\monadendo{m}}$ is the 2-cell of the distributive law, and the laws are the proofs that $\monadunit{m}$ and $\monadmult{m}$ are 2-cells in $\mnd{\B}$.

Analogously, we can show that objects in $\mnd{\cobicat{\mnd{\cobicat{\B}}}}$ are mixed distributive laws in $\B$ [13, 42].
We can also look at iterated distributive laws, which are monads in $\mndn{\B}{n}$ [15].

Next we look at two ways to general constructions of monads.
First of all, we look at the identity monad: on every object $x : \B$, we construct the identity monad $\idmonad{x}$.

Given a bicategory $\B$, to construct a section on $\dmnd{\B}$.

To construct the desired section, we define the identity monad $\idmonad{x}$ for every $x$.

* The object is $x$;

* The 1-cell is $\id{x} : x \onecell x$;

* The unit is $\id{\id{x}} : \id{x} \twocell \id{x}$;

* The multiplication is $\lunitor{\id{x}} : \comp{\id{x}}{\id{x}} \twocell \id{x}$.

In the remainder, we only use the pseudofunctor arising from <ref> and <ref>, and this pseudofunctor is denoted as $\idmonadpsfunctor : \B \onecell \mnd{\B}$.
Second, we notice that every monad $m : \mnd{\B}$ gives rise to a monad of categories.
This example is used in <ref>.

Given a monad $m$ in a bicategory $\B$ and an object $x$, to construct a monad $\hommonad{x}{m}$ on $\homC{\B}{x}{\monadob{m}}$.

The monad $\hommonad{x}{m}$ is defined as follows:

* The endofunctor is $\postcomp{\monadendo{m}}{x} : \homC{\B}{x}{\monadob{m}} \onecell \homC{\B}{x}{\monadob{m}}$.

* For every $f : x \onecell \monadob{m}$, the unit is defined to be

\[
\begin{tikzcd}[column sep = large]
f & {\comp{f}{\id{\monadob{m}}}} & {\comp{f}{\monadendo{m}}}
\arrow["{\rinvunitor{f}}", from=1-1, to=1-2, Rightarrow]
\arrow["{f \whiskerl \monadunit{m}}", from=1-2, to=1-3, Rightarrow]
\end{tikzcd}
\]

* For every $f : x \onecell \monadob{m}$, the multiplication is defined to be

\[
\begin{tikzcd}[column sep = large]
{\comp{(\comp{f}{\monadendo{m}})}{\monadendo{m}}} & {\comp{f}{(\comp{\monadendo{m}}{\monadendo{m}})}} & {\comp{f}{\monadendo{m}}}
\arrow["{\rassociator{f}{\monadendo{m}}{\monadendo{m}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{f \whiskerl \monadmult{m}}", from=1-2, to=1-3, Rightarrow]
\end{tikzcd}
\qedhere
\]

Next we show that pseudofunctors preserve monads.

Given bicategories $\B_1$ and $\B_2$, a pseudofunctor $F : \B_1 \onecell \B_2$, and a monad $m : \mnd{\B_1}$, to construct a monad $F(m) : \mnd{\B_2}$.

The object of $F(m)$ is $F(\monadob{m})$ while the 1-cell is $F(\monadendo{m}) : F(\monadob{m}) \onecell F(\monadob{m})$.
The unit and multiplication are constructed using to the following pasting diagrams respectively

\[
\begin{tikzcd}[column sep=7em, row sep=huge]
{F(\monadob{m})} & {F(\monadob{m})}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\id{F(\monadob{m})}}", bend left=60, from=1-1, to=1-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{F(\monadendo{m})}"', bend right=60, from=1-1, to=1-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{F(\id{\monadob{m}})}"{description}, from=1-1, to=1-2]
\arrow["{\identitor{F}{\monadob{m}}}", shorten <=1pt, shorten >=5pt, Rightarrow, from=0, to=2]
\arrow["{F(\monadunit{m})}", shorten <=5pt, shorten >=1pt, Rightarrow, from=2, to=1]
\end{tikzcd}
\quad \quad
\begin{tikzcd}[column sep=7em, row sep=huge]
{F(\monadob{m})} & {F(\monadob{m})}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\comp{F(\monadendo{m})}{F(\monadendo{m})}}", bend left=60, from=1-1, to=1-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{F(\monadendo{m})}"', bend right=60, from=1-1, to=1-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{F(\comp{\monadendo{m}}{\monadendo{m}})}"{description}, from=1-1, to=1-2]
\arrow["{\compositor{F}{\monadendo{m}}{\monadendo{m}}}", shorten <=1pt, shorten >=5pt, Rightarrow, from=0, to=2]
\arrow["{F(\monadmult{m})}", shorten <=5pt, shorten >=1pt, Rightarrow, from=2, to=1]
\end{tikzcd}
\]

For a proof of the monad laws, we refer the reader to the formalization.

In fact, if we have a pseudofunctor $F : \B_1 \onecell \B_2$, then we obtain a pseudofunctor $\mnd{F} : \mnd{\B_1} \onecell \mnd{\B_2}$.
Next we show that monads can be composed if we have a distributive law between them.

Suppose that we have a distributive law $\tau$ between monads $m_1$ and $m_2$ (<ref>).
Then we define a monad $\comp{m_1}{m_2}$ as follows:

* The object is $\monadob{m_1}$ (which is definitionally equal to $\monadob{m_2}$);

* The 1-cell is $\comp{\monadendo{m_1}}{\monadendo{m_2}}$;

* The unit is constructed as the following composition of 2-cells

\[
\begin{tikzcd}[sep=huge]
{\id{\monadob{m_1}}} & {\comp{\id{\monadob{m_1}}}{\id{\monadob{m_1}}}} & {\comp{\monadendo{m_1}}{\id{\monadob{m_1}}}} & {\comp{\monadendo{m_1}}{\monadendo{m_2}}}
\arrow["{\linvunitor{\monadob{m_1}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\monadunit{m_1} \whiskerr \id{\monadob{m_1}}}", from=1-2, to=1-3, Rightarrow]
\arrow["{\monadendo{m_1} \whiskerl \monadunit{m_2}}", from=1-3, to=1-4, Rightarrow]
\end{tikzcd}
\]

* The multiplication is the following composition of 2-cells

\[
\begin{tikzcd}[sep=huge]
{\comp{(\comp{\monadendo{m_1}}{\monadendo{m_2}})}{(\comp{\monadendo{m_1}}{\monadendo{m_2}})}} & {\comp{\monadendo{m_1}}{(\comp{\monadendo{m_2}}{(\comp{\monadendo{m_1}}{\monadendo{m_2}})})}} & {\comp{\monadendo{m_1}}{(\comp{(\comp{\monadendo{m_2}}{\monadendo{m_1}})}{\monadendo{m_2}})}} \\
{\comp{\monadendo{m_1}}{(\comp{(\comp{\monadendo{m_1}}{\monadendo{m_2}})}{\monadendo{m_2}})}} & {\comp{\monadendo{m_1}}{(\comp{\monadendo{m_1}}{(\comp{\monadendo{m_2}}{\monadendo{m_2}})})}} & {\comp{(\comp{\monadendo{m_1}}{\monadendo{m_1}})}{(\comp{\monadendo{m_2}}{\monadendo{m_2}})}} \\
{\comp{\monadendo{m_1}}{(\comp{\monadendo{m_2}}{\monadendo{m_2}})}} & & {\comp{\monadendo{m_1}}{\monadendo{m_2}}}
\arrow["{\rassociator{}{}{}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\monadendo{m_1} \whiskerl \lassociator{}{}{}}", from=1-2, to=1-3, Rightarrow]
\arrow["{\monadendo{m_1} \whiskerl (\tau \whiskerr \monadendo{m_2})}"{description}, from=1-3, to=2-1, Rightarrow]
\arrow["{\monadendo{m_1} \whiskerl \rassociator{}{}{}}"{description}, from=2-1, to=2-2, Rightarrow]
\arrow["{\lassociator{}{}{}}"{description}, from=2-2, to=2-3, Rightarrow]
\arrow["{\monadmult{m_1} \whiskerr (\comp{\monadendo{m_2}}{\monadendo{m_2}})}"{description}, from=2-3, to=3-1, Rightarrow]
\arrow["{\monadendo{m_1} \whiskerl \monadmult{m_2}}"', from=3-1, to=3-3, Rightarrow]
\end{tikzcd}
\]

§ EILENBERG-MOORE OBJECTS

The second important concept in the formal theory of monads is the notion of Eilenberg-Moore objects.
An important property of monads in category theory is that every monad gives rise to an adjunction.
One can do this in two ways: either via Eilenberg-Moore categories or via Kleisli categories.
In this section, we study Eilenberg-Moore objects, which formulate Eilenberg-Moore categories in bicategorical terms.

Note that the terminology in this section is slightly differently compared to what was used by Street [45].
Whereas Street would say that a bicategory admits the construction of algebras, we would say that a bicategory has Eilenberg-Moore objects.
In addition, our notions are defined slightly differently, but still equivalent to the original definition by Street.
The difference comes from the fact that we use Eilenberg-Moore cones.

Let $\B$ be a bicategory and let $m$ be a monad in $\B$.
An Eilenberg-Moore cone for $m$ consists of an object $e$ together with a 1-cell $\idmonad{e} \onecell m$.

More concretely, an Eilenberg-Moore cone $e$ for a monad $m$ consists of

* An object $\emobfull{e}$;

* A 1-cell $\emmor{e} : \emobfull{e} \onecell \monadob{m}$;

* A 2-cell $\emcell{e} : \comp{\emmor{e}}{\monadendo{m}} \twocell \comp{\id{x}}{\emmor{e}}$

such that the following diagrams commutes

\[
\begin{tikzcd}
\emmor{e} & {\comp{\emmor{e}}{\id{\monadob{m}}}} &[2em] {\comp{\emmor{e}}{\monadendo{m}}} \\
&& {\comp{\id{x}}{\emmor{e}}}
\arrow["\emcell{e}", from=1-3, to=2-3, Rightarrow]
\arrow["{\emmor{e} \whiskerl \monadunit{m}}", from=1-2, to=1-3, Rightarrow]
\arrow["{\rinvunitor{\emmor{e}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\linvunitor{\emmor{e}}}"', from=1-1, to=2-3, Rightarrow]
\end{tikzcd}
\]

\[
\begin{tikzcd}[column sep = huge]
{\comp{\emmor{e}}{(\comp{\monadendo{m}}{\monadendo{m}})}} &&& {\comp{\emmor{e}}{\monadendo{m}}} \\
{\comp{(\comp{\emmor{e}}{\monadendo{m}})}{\monadendo{m}}} & {\comp{(\comp{\id{x}}{\emmor{e}})}{\monadendo{m}}} & {\comp{\emmor{e}}{\monadendo{m}}} & {\comp{\id{x}}{\emmor{e}}}
\arrow["{\lassociator{\emmor{e}}{\monadendo{m}}{\monadendo{m}}}"', from=1-1, to=2-1, Rightarrow]
\arrow["{\emcell{e} \whiskerr \monadendo{m}}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\lunitor{\emmor{e}} \whiskerr \monadendo{m}}"', from=2-2, to=2-3, Rightarrow]
\arrow["{\emcell{e}}"', from=2-3, to=2-4, Rightarrow]
\arrow["{\emmor{e} \whiskerl \monadmult{m}}", from=1-1, to=1-4, Rightarrow]
\arrow["{\emcell{e}}", from=1-4, to=2-4, Rightarrow]
\end{tikzcd}
\]

If no confusion arises, we write $\emob{e}$ instead of $\emobfull{e}$.

Next we look at the universal property of Eilenberg-Moore objects.
Since Eilenberg-Moore objects are examples of limits in a bicategories [41], there are multiple methods to express their universal property.
A first possibility, which is used by Street, is to use biadjunctions [45], and a second option is to write out explicit mapping properties.
Alternatively, one could express the universal property as an adjoint equivalence on the hom-categories.
We use the last option.
To write out the desired definition precisely, we first define a functor with domain $\homC{\B}{x}{\emob{e}}$ where $e$ is an Eilenberg-Moore cone and $x$ is any object.

Given an Eilenberg-Moore cone $e$ for $m$ and an object $x$, to construct a functor $\emfunctor{x}{\emob{e}} : \homC{\B}{x}{\emob{e}} \onecell \homC{\mnd{\B}}{\idmonad{x}}{m}$.

Suppose that we have a 1-cell $f : x \onecell e$. We construct the monad morphism $\emfunctor{x}{e}(f)$ as follows:

* The underlying morphism is $\comp{f}{\emmor{e}}$.

* For the 2-cell $\comp{(\comp{f}{\emmor{e}})}{\monadendo{m}} \twocell \comp{\id{x}}{(\comp{f}{\emmor{e}})}$, we take

\[
\begin{tikzcd}
{\comp{(\comp{f}{\emmor{e}})}{\monadendo{m}}} & {\comp{f}{\comp{\emmor{e}}{\monadendo{m}}}} & {\comp{f}{\comp{\id{\emob{e}}}{\emmor{e}}}} & {\comp{f}{\emmor{e}}} & {\comp{\id{x}}{(\comp{f}{\emmor{e}})}.}
\arrow["{\rassociator{f}{\emmor{e}}{\monadendo{m}}}", from=1-1, to=1-2]
\arrow["{f \whiskerl \emcell{e}}", from=1-2, to=1-3]
\arrow["{f \whiskerl \lunitor{\emmor{e}}}", from=1-3, to=1-4]
\arrow["{\linvunitor{\comp{f}{\emmor{e}}}}", from=1-4, to=1-5]
\end{tikzcd}
\]

Given a 2-cell $\tau : f \twocell g$, the underlying cell of $\emfunctor{x}{e}(\tau) : \emfunctor{x}{e}(f) \twocell \emfunctor{x}{e}(g)$ is $\tau \whiskerr \emmor{e}$.

Let $\B$ be a bicategory and let $m$ be a monad in $\B$.
An Eilenberg-Moore cone $e$ for $m$ is called universal if for every object $x$ the functor $\emfunctor{x}{e}$ is an adjoint equivalence of categories.
We say that a bicategory has Eilenberg-Moore objects if for every monad $m$ there is a universal Eilenberg-Moore cone.

Let $\B$ be a locally univalent bicategory and let $e$ be an Eilenberg-Moore cone for a monad $m$ in $\B$.
The type that $e$ is universal, is a proposition.

Another way to formulate the universality of an Eilenberg-Moore cone, is by using Eilenberg-Moore categories.
If we have a monad $m$ on a category $\C$, we write $\emlim{}{m}$ for the Eilenberg-Moore category of $m$.

Given an Eilenberg-Moore cone $e$ for a monad $m$ and an object $x : \B$, to construct a functor $\emfunctoralt{x}{e} : \homC{\B}{x}{\emob{e}} \onecell \emlim{}{\hommonad{x}{m}}$.

First, we say how $\emfunctoralt{x}{e}$ acts on objects.
Suppose that we have $f : x \onecell \emob{e}$.
To define an object of $\emlim{}{\hommonad{x}{m}}$, we first need to give a 1-cell $h : x \onecell \monadob{x}$.
We define $h$ as
\begin{tikzcd}
x & {\emob{e}} & {\monadob{m}}
\arrow["f", from=1-1, to=1-2]
\arrow["{\emmor{e}}", from=1-2, to=1-3]
\end{tikzcd}
We also need to define a 2-cell $\tau : \comp{h}{\monadendo{m}} \Rightarrow h$ for which we take

\[
\begin{tikzcd}[column sep = large]
{\comp{(\comp{f}{\emmor{e}})}{\monadendo{m}}} & {\comp{f}{(\comp{\emmor{e}}{\monadendo{m}})}} & {\comp{f}{(\comp{\id{x}}{\emmor{e}})}} & {\comp{f}{\emmor{e}}}
\arrow["{\lassociator{f}{\emmor{e}}{\monadendo{m}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{f \whiskerl \emcell{e}}", from=1-2, to=1-3, Rightarrow]
\arrow["{f \whiskerl \lunitor{\emmor{e}}}", from=1-3, to=1-4, Rightarrow]
\end{tikzcd}
\]

Next we define the action on morphisms.
Suppose that we have $f, g : x \onecell \emob{e}$ and a 2-cell $\theta : f \twocell g$.
We need to construct a 2-cell $\comp{f}{\emmor{e}} \twocell \comp{g}{\emmor{e}}$, for which we take $\theta \whiskerr \emmor{e}$.

Let $e$ be an Eilenberg-Moore cone.
Then $e$ is universal if and only if for every $x$ the functor $\emfunctoralt{x}{e}$ is an adjoint equivalence.

We only give a brief sketch of the proof.
The main idea is that one can construct an adjoint equivalence from $\emlim{}{\hommonad{x}{m}}$ to $\homC{\mnd{\B}}{\idmonad{x}}{m}$.
With this equivalence available, the theorem follows from the 2-out-of-3 property.

Alternatively, universality can be formulated using mapping properties.
These properties are deduced from the fact that every adjoint equivalence is split essentially surjective and fully faithful.
More precisely, an Eilenberg-Moore cone $e$ is universal if and only if

* for every Eilenberg-Moore cone $q$ there is a 1-cell $\emumpmor{q} : \emob{q} \onecell \emob{e}$ and an invertible 2-cell $\emumpcom{q} : \comp{\idmonad{\emumpmor{q}}}{\emmor{e}} \Rightarrow \emmor{q}$ in $\mnd{\B}$;

* for all 1-cells $g_1, g_2 : \emob{q} \onecell \emob{e}$ and 2-cells $\tau : \comp{\idmonad{g_1}}{\emmor{e}} \Rightarrow \comp{\idmonad{g_2}}{\emmor{e}}$ in $\mnd{\B$},
there is a unique 2-cell $\emumpcell{\tau}$ such that $\idmonad{\emumpcell{\tau}} \whiskerr \emmor{e} = \tau$.
\end{itemize}
Let us consider some examples of Eilenberg-Moore objects.

\begin{exa}[\coqident{Bicategories.Limits.Examples.LimitsStructuredCategories}{has_em_bicat_of_univ_cats}]
\label{ex:em-cats}
The bicategory $\UnivCat$ has Eilenberg-Moore objects.
As suggested by the name, the Eilenberg-Moore object on a monad $m$ is indeed given by the Eilenberg-Moore category $\emlim{}{m}$.
Note that if $\C$ is a univalent and $m$ is a monad on $\C$, then $\emlim{}{m}$ is univalent as well.
\end{exa}

\begin{exa}[\coqident{Bicategories.Limits.Examples.LimitsStructuredCategories}{has_em_univ_cat_with_terminal_obj}]
\label{ex:em-terminal}
The bicategory $\Terminal$ has Eilenberg-Moore objects as well.
If we have a monad $m : \mnd{\Terminal}$, then $\monadob{m}$ has a terminal object and $\monadendo{m}$ preserves terminal objects.
Under these conditions, it follows that the Eilenberg-Moore category of $m$ has a terminal object.
From this, we can conclude that $\Terminal$ indeed has Eilenberg-Moore objects.
\end{exa}

One can also show that $\cobicat{\SymMonCat}$ has Eilenberg-Moore objects.
These are given by Eilenberg-Moore categories of comonads.

\section{Duality and Kleisli Objects}
\label{sec:duality}
The goal of this section is to construct Eilenberg-Moore objects in $\opbicat{\UnivCat}$.
To do so, we start by characterizing such objects via \emph{Kleisli objects}.

\begin{defi}[\coqident{Bicategories.Colimits.KleisliObjects}{kleisli_cocone}]
Let $\B$ be a bicategory and let $m$ be a monad in $\B$.
A \textbf{Kleisli cocone} $k$ for $m$ in $\B$ consists of an object $\klob{k} : \B$, a 1-cell $\klmor{k} : \monadob{m} \onecell \klob{k}$, and a 2-cell $\klcell{k} : \comp{\monadendo{m}}{\klmor{k}} \twocell \klmor{k}$ such that the following diagrams commute
\[
\begin{tikzcd}[column sep = huge]
{\comp{\id{\monadob{m}}}{\klmor{k}}} & {\comp{\monadendo{m}}{\klmor{k}}} \\
& {\klmor{k}}
\arrow["{\monadunit{m} \whiskerr \klmor{k}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\klcell{k}}", from=1-2, to=2-2, Rightarrow]
\arrow["{\lunitor{\klmor{k}}}"', from=1-1, to=2-2, Rightarrow]
\end{tikzcd}
\]
\[
\begin{tikzcd}[column sep = large]
{\comp{(\comp{\monadendo{m}}{\monadendo{m}})}{\klmor{k}}} & {\comp{\monadendo{m}}{(\comp{\monadendo{m}}{\klmor{k}})}} & {\comp{\monadendo{m}}{\klmor{k}}} \\
{\comp{\monadendo{m}}{\klmor{k}}} && {\klmor{k}}
\arrow["{\monadmult{m} \whiskerr \klmor{k}}"', from=1-1, to=2-1, Rightarrow]
\arrow["{\rassociator{\monadendo{m}}{\monadendo{m}}{\klmor{k}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\monadendo{m} \whiskerl \klcell{k}}", from=1-2, to=1-3, Rightarrow]
\arrow["{\klcell{k}}", from=1-3, to=2-3, Rightarrow]
\arrow["{\klcell{k}}"', from=2-1, to=2-3, Rightarrow]
\end{tikzcd}
\]
\end{defi}

\begin{defi}[\coqident{Bicategories.Colimits.KleisliObjects}{has_kleisli_ump}]
A Kleisli cocone $k$ is said to be \textbf{universal} if
\begin{itemize}
\item For every Kleisli cocone $q$ there there is a 1-cell $\klumpmor{q} : \klob{k} \onecell \klob{q}$ and an invertible 2-cell $\klumpcom{q} : \comp{\klmor{k}}{\klumpmor{q}} \twocell \klmor{q}$ such that that the following diagram commutes
\[
\begin{tikzcd}[column sep = huge]
{\comp{\monadendo{m}}{(\comp{\klmor{k}}{\klumpmor{q}})}} && {\comp{\monadendo{m}}{\klmor{q}}} \\
{\comp{(\comp{\monadendo{m}}{\klmor{k}})}{\klumpmor{q}}} & {\comp{\klmor{k}}{\klumpmor{q}}} & {\klmor{q}}
\arrow["{\monadendo{m} \whiskerl \klumpcom{q}}", from=1-1, to=1-3, Rightarrow]
\arrow["{\lassociator{\monadendo{m}}{\klmor{k}}{\klumpmor{q}}}"', from=1-1, to=2-1, Rightarrow]
\arrow["{\klcell{k} \whiskerr \klumpmor{q}}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\klumpcom{q}}"', from=2-2, to=2-3, Rightarrow]
\arrow["{\klcell{q}}", from=1-3, to=2-3, Rightarrow]
\end{tikzcd}
\]
\item Suppose that we have an object $x : \B$, two 1-cells $g_1, g_2 : \klob{k} \onecell x$, and a 2-cell $\tau : \comp{\klcell{k}}{g_1} \twocell \comp{\klcell{k}}{g_2}$ such that the following diagram commutes
\[
\begin{tikzcd}[column sep = huge]
{\comp{\monadendo{m}}{(\comp{\klmor{k}}{g_1})}} & {\comp{(\comp{\monadendo{m}}{\klmor{k}})}{g_1}} & {\comp{\klmor{k}}{g_1}} \\
{\comp{\monadendo{m}}{(\comp{\klmor{k}}{g_2})}} & {\comp{(\comp{\monadendo{m}}{\klmor{k}})}{g_2}} & {\comp{\klmor{k}}{g_2}}
\arrow["{\lassociator{\monadendo{m}}{\klmor{k}}{g_1}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\klcell{k} \whiskerr g_1}", from=1-2, to=1-3, Rightarrow]
\arrow["\tau", from=1-3, to=2-3, Rightarrow]
\arrow["{\monadendo{m} \whiskerl \tau}"', from=1-1, to=2-1, Rightarrow]
\arrow["{\lassociator{\monadendo{m}}{\klmor{k}}{g_2}}"', from=2-1, to=2-2, Rightarrow]
\arrow["{\klcell{k} \whiskerr g_2}"', from=2-2, to=2-3, Rightarrow]
\end{tikzcd}
\]
Then there is a unique 2-cell $\klumpcell{\tau} : g_1 \twocell g_2$ such that $\klcell{k} \whiskerl \klumpcell{\tau} = \tau$.
\end{itemize}
A \textbf{Kleisli object} is a universal Kleisli cocone.
We say that a bicategory has Kleisli objects if there is a Kleisli object for every monad $m$.
\end{defi}

\begin{prop}[\coqident{Bicategories.Limits.Examples.OpMorBicatLimits}{op1_has_em}]
If $\B$ has Kleisli objects, then $\opbicat{\B}$ has Eilenberg-Moore objects.
\end{prop}

As such, to find Eilenberg-Moore objects in $\opbicat{\UnivCat}$, we need to find Kleisli objects in $\UnivCat$.
However, before we look those, we look at Kleisli objects in $\Cat$.
These are constructed via the usual definition of \emph{Kleisli categories}.

\begin{problem}
\label{prob:kleisli-cats}
To construct Kleisli objects in $\Cat$.
\end{problem}

\begin{construction}[\coqident{Bicategories.Colimits.Examples.BicatOfCatsColimits}{bicat_of_cats_has_kleisli}]{prob:kleisli-cats}
Recall that given a monad $m$ on a category $\C$, the Kleisli category $\kleisli{m}$ is usually defined to be the category whose objects are $x : \C$ and whose morphisms from $x : \C$ to $y : \C$ are morphisms  $x \onecell m(y)$.
Note that we have a functor $F : \C \onecell \kleisli{m}$: it sends objects $x$ to $x$ and morphisms $f : x \onecell y$ to
x & y & {\monadendo{m}(y).}
\arrow["f", from=1-1, to=1-2]
\arrow["{\monadunit{m}(y)}", from=1-2, to=1-3]
\end{tikzcd}$
We also have a natural transformation $\comp{\monadendo{m}}{F} \twocell F$, which is the identity on ever object $x$.
As such, we have a Kleisli cocone.
This cocone is universal, and for a proof we refer the reader to the formalization.
\end{construction}

Note that even if $\C$ is required to be univalent, the Kleisli category $\kleisli{m}$ is \textbf{not} necessarily univalent.
As such, to obtain Kleisli objects in $\UnivCat$, we need to use an alternative definition for the Kleisli category [8].
First, we define a functor $\freealg{m} : \C \onecell \eilenbergmoore{m}$ which sends objects $x : \C$ to the algebra $\monadmult{m}(x) : \monadendo{m}(\monadendo{m}(x)) \onecell \monadendo{m}(x)$ and morphisms $f : x \onecell y$ to $\monadendo{m}(f) : \monadendo{m}(x) \onecell \monadendo{m}(y)$.
Note that this 1-cell can actually be defined in arbitrary bicategories (see \cref{sec:adj}).
By taking the full image of this functor, we obtain the category $\univkleisli{m}$.
\begin{itemize}
\item Objects of $\univkleisli{m}$ are pairs $y : \C$ together with a proof of
\trunc{\sigmatype{x}{\C}{m(x) \cong y}}.
\item Morphisms from $y_1 : \univkleisli{m}$ to $y_2 : \univkleisli{m}$ are morphisms $y_1 \onecell y_2$ in $\C$.
\end{itemize}
If $\C$ is univalent, then $\emlim{\UnivCat}{m}$ is univalent, and thus $\univkleisli{m}$ is so as well.

\begin{problem}
\label{prob:kleisi-functor}
To construct a fully faithful essentially surjective functor $\kleislifunctor{m} : \kleisli{m} \onecell \univkleisli{m}$.
\end{problem}

\begin{construction}[\coqident{CategoryTheory.categories.KleisliCategory}{functor_to_kleisli_cat}]{prob:kleisi-functor}
\label{constr:kleisi-functor}
The functor $\kleislifunctor{m}$ sends every object $x : \kleisli{m}$ to $\freealg{m}(x)$, which is indeed in the image of $\freealg{m}$.
Morphisms $f : x \onecell \monadendo{m}(y)$ are sent to
{\monadendo{m}(x)} & {\monadendo{m}(\monadendo{m}(y))} & {\monadendo{m}(y).}
\arrow["{\monadendo{m}(f)}", from=1-1, to=1-2]
\arrow["{\monadmult{m}(y)}", from=1-2, to=1-3]
\end{tikzcd}$
A proof that this functor is both essentially surjective and fully faithful can be found in the formalization.
\end{construction}
% Note that we have a fully faithful essentially surjective functor $\kleislifunctor{m} : \kleisli{m} \onecell \univkleisli{m}$.

In univalent foundations, not every functor that is both fully faithful and essentially surjective is automatically an adjoint equivalence as well.
This statement only holds if the domain is univalent.
However, we can still use the functor $\kleislifunctor{m}$ to deduce the universal property of $\univkleisli{m}$.
For that, we use Theorem 8.4 in [3].

\begin{prop}[\coqident{CategoryTheory.PrecompEquivalence}{precomp_adjoint_equivalence}]
\label{prop:precomp-equiv}
Let $F : \C_1 \onecell \C_2$ be a fully faithful and essentially surjective functor, and suppose that $\C_3$ is a univalent category.
Then the functor $\precomp{F}{\C_3} : \C_3^{\C_2} \onecell \C_3^{\C_1}$, given by precomposition with $F$, is an adjoint equivalence.
\end{prop}
% For that, we use Theorem 8.4 in [3], which says that the functor $\precomp{F}{\C_3} : \C_3^{\C_2} \onecell \C_3^{\C_1}$, given by precomposition with $F$, is an adjoint equivalence if $F$ is fully faithful and essentially surjective and $\C_3$ is univalent.

\begin{problem}
\label{prob:univ-kleisli-cats}
To construct Kleisli objects in $\UnivCat$.
\end{problem}

\begin{construction}[\coqident{Bicategories.Colimits.Examples.BicatOfUnivCatsColimits}{bicat_of_univ_cats_has_kleisli}]{prob:univ-kleisli-cats}
\label{constr:univ-kleisli-cats}
We only show how to construct the required 1-cells.
Suppose that we have a Kleisli cocone $q$ in $\UnivCat$.
Note that $q$ also is a Kleisli cocone in $\Cat$, and as such, we get a functor $\klumpmor{q} : \kleisli{m} \onecell \klob{q}$.
By \cref{prop:precomp-equiv}, we now get the desired functor $\univkleisli{m} \onecell \klob{q}$.
\end{construction}

\section{Monads and Adjunctions}
\label{sec:adj}
The cornerstone of the theory of monads is the relation between monads and adjunctions.
More specifically, every adjunction gives rise to a monad and vice versa.
This was generalized by Street to 2-categories that have Eilenberg-Moore objects [45].
In this section, we prove these theorems, and to do so, we start by recalling adjunctions in bicategories.

\begin{defi}[\coqident{Bicategories.Morphisms.Adjunctions}{adjunction}]
\label{def:adjunction}
An \textbf{adjunction} $\adjunction{l}{r}{\eta}{\varepsilon}$ in a bicategory $\B$ consists of
\begin{itemize}
\item objects $x$ and $y$;
\item 1-cells $l : x \onecell y$ and $r : y \onecell x$;
\item 2-cells $\eta : \id{x} \twocell \comp{l}{r}$ and $\varepsilon : \comp{r}{l} \twocell \id{y}$
\end{itemize}
such that the following 2-cells are identities
\[
\begin{tikzcd}
l & {\comp{\id{x}}{l}} & {\comp{(\comp{l}{r})}{l}} & {\comp{l}{(\comp{r}{l})}} & {\comp{l}{\id{y}}} & l
\arrow["{\linvunitor{l}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\eta \whiskerr l}", from=1-2, to=1-3, Rightarrow]
\arrow["{\rassociator{l}{r}{l}}", from=1-3, to=1-4, Rightarrow]
\arrow["{l \whiskerl \varepsilon}", from=1-4, to=1-5, Rightarrow]
\arrow["{\runitor{l}}", from=1-5, to=1-6, Rightarrow]
\end{tikzcd}
\]
\[
\begin{tikzcd}
r & {\comp{r}{\id{x}}} & {\comp{r}{(\comp{l}{r})}} & {\comp{(\comp{r}{l})}{r}} & {\comp{\id{y}}{r}} & r
\arrow["{\rinvunitor{r}}", from=1-1, to=1-2, Rightarrow]
\arrow["{r \whiskerl \eta}", from=1-2, to=1-3, Rightarrow]
\arrow["{\lassociator{r}{l}{r}}", from=1-3, to=1-4, Rightarrow]
\arrow["{\varepsilon \whiskerr r}", from=1-4, to=1-5, Rightarrow]
\arrow["{\lunitor{r}}", from=1-5, to=1-6, Rightarrow]
\end{tikzcd}
\]
\end{defi}

Our notation for adjunctions is taken from [16].
The two coherencies in \cref{def:adjunction} are called the \emph{triangle equalities}.
As expected, adjunctions internal to $\UnivCat$ correspond to adjunctions of categories [30].
This is because the unitors and associators in $\UnivCat$ are pointwise the identity, so the triangle equalities in \cref{def:adjunction} reduce to the usual ones.

\begin{exa}
\label{exa:adj-dual}
We characterize adjunctions in $\opbicat{B}$ and $\cobicat{B}$ as follows.
\begin{itemize}
\item (\coqident{Bicategories.Morphisms.Examples.MorphismsInOp1Bicat}{op1_left_adjoint_to_right_adjoint}) Every adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ in $\B$ gives rise to an adjunction $\adjunction{r}{l}{\eta}{\varepsilon}$ in $\opbicat{\B}$ and vice versa.
\item (\coqident{Bicategories.Morphisms.Examples.MorphismsInOp2Bicat}{op2_left_adjoint_to_right_adjoint})  Every adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ in $\B$ gives rise to an adjunction $\adjunction{r}{l}{\varepsilon}{\eta}$ in $\cobicat{\B}$ and vice versa.
\end{itemize}
\end{exa}

\cref{exa:adj-dual} can be strengthened by using the terminology of \emph{left adjoints} and \emph{right adjoints}.
Given a 1-cell $f : x \onecell y$, the type $\leftadj{\B}{f}$ says that we have $r$,$\eta$, and $\varepsilon$ such that we have an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$.
The type $\rightadj{\B}{f}$ is defined analogously.
Now we can reformulate \cref{exa:adj-dual} as follows: we have equivalences $\typeequiv{\leftadj{\opbicat{\B}}{f}}{\rightadj{\B}{f}}$ and $\typeequiv{\leftadj{\cobicat{\B}}{f}}{\rightadj{\B}{f}}$ of types.

Next we look at \emph{displayed adjunctions}, which we use to obtain adjunctions in total bicategories [2].
This notion is used to characterize adjunctions in bicategories such as $\Terminal$ and $\SymMonCat$.

\begin{defi}[\coqident{Bicategories.DisplayedBicats.DispAdjunctions}{disp_adjunction}]
\label{def:disp-adj}
Let $\B$ be a bicategory and let $\D$ be a displayed bicategory over $\B$.
A \textbf{displayed adjunction} over an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ where $l : x \onecell y$ consists of
\begin{itemize}
\item Objects $\disp{x} : \dob{D}{x}$ and $\disp{y} : \dob{D}{y}$;
\item Displayed morphisms $\disp{l} : \dmor{\disp{x}}{\disp{y}}{l}$ and $\disp{r} : \dmor{\disp{y}}{\disp{x}}{r}$;
\item Displayed 2-cells $\disp{\eta} : \dtwo{\disp{\id{x}}}{\comp{\disp{l}}{\disp{r}}}{\eta}$ and $\disp{\varepsilon} : \dtwo{\comp{\disp{r}}{\disp{l}}}{\id{x}}{\varepsilon}$.
\end{itemize}
We also require some coherencies and those can be found in the formalization.
We denote this data by $\dispadjunction{l}{r}{\eta}{\varepsilon}$.
\end{defi}

\begin{problem}
\label{prob:total-adj}
Given a displayed adjunction $\dispadjunction{l}{r}{\eta}{\varepsilon}$ in a displayed bicategory $\D$ over $\adjunction{l}{r}{\eta}{\varepsilon}$, to construct an adjunction $\total{\dispadjunction{l}{r}{\eta}{\varepsilon}}$ in $\total{D}$.
\end{problem}

\begin{construction}[\coqident{Bicategories.DisplayedBicats.DispAdjunctions}{left_adjoint_data_total_weq}]{prob:total-adj}
\label{constr:total-adj}
The left adjoint of $\total{\dispadjunction{l}{r}{\eta}{\varepsilon}}$ is $(l, \disp{l})$, the right adjoint is $(r, \disp{r})$, the unit is $(\eta, \disp{\eta})$, and the counit is $(\varepsilon, \disp{\varepsilon})$.
\end{construction}
% Every displayed adjunction $\dispadjunction{l}{r}{\eta}{\varepsilon}$ in a displayed bicategory $\D$ over $\adjunction{l}{r}{\eta}{\varepsilon}$ gives rise to an adjunction $\total{\dispadjunction{l}{r}{\eta}{\varepsilon}}$ in $\total{D}$.

\begin{exa}[\coqident{Bicategories.Morphisms.Examples.MorphismsInStructuredCat}{disp_adj_weq_preserves_terminal}]
\label{exa:adj-terminal}
Adjunctions in $\Terminal$ are given by an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ in $\UnivCat$ such that $l$ preserves terminal objects.
Note that $r$ automatically preserves terminal objects, because $r$ is a right adjoint.
\end{exa}

Analogously, we characterize adjunctions in $\SymMonCat$.
Now we have developed enough to state and prove the core theorems of the formal theory of monads [45].
These theorems relate adjunctions and monads, and we first prove that every adjunction gives rise to a monad.

\begin{problem}
\label{prob:adj-to-mnd}
Given an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$, to construct a monad $\adjtomnd{\adjunction{l}{r}{\eta}{\varepsilon}}$.
\end{problem}

\begin{construction}[\coqident{Bicategories.Monads.Examples.AdjunctionToMonad}{mnd_from_adjunction}]{prob:adj-to-mnd}
\label{constr:adj-to-mnd}
Let an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ be given where $l : x \rightarrow y$.
We define the monad $\adjtomnd{\adjunction{l}{r}{\eta}{\varepsilon}}$ as follows.
\begin{itemize}
\item Its object is $x$;
\item The endomorphism is $\comp{l}{r} : x \onecell y$;
\item The unit is $\eta : \id{x} \onecell \comp{l}{r}$;
\item For the multiplication, we use the following composition of 2-cells
\[
\begin{tikzcd}[sep=3em]
{\comp{(\comp{l}{r})}{(\comp{l}{r})}} & {\comp{l}{(\comp{r}{(\comp{l}{r})})}} & {\comp{l}{(\comp{(\comp{r}{l})}{r})}} & {\comp{l}{(\comp{\id{y}}{r})}} & {\comp{l}{r}}
\arrow["{\lassociator{l}{r}{\comp{l}{r}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{l \whiskerl \rassociator{r}{l}{r}}", from=1-2, to=1-3, Rightarrow]
\arrow["{l \whiskerl (\varepsilon \whiskerr r)}", from=1-3, to=1-4, Rightarrow]
\arrow["{l \whiskerl \lunitor{r}}", from=1-4, to=1-5, Rightarrow]
\end{tikzcd}
\]
\end{itemize}
The proofs of the necessary equalities can be found in the formalization.
\end{construction}

Since by \cref{exa:adj-dual,exa:mnd-dual} adjunctions and monads in $\cobicat{\B}$ correspond to adjunctions and comonads in $\B$ respectively,
we get that every adjunction in $\B$ induces a comonad by \cref{constr:adj-to-mnd}.
Next we look at the converse: obtaining adjunctions from monads.
For this, we need to work in a bicategory with Eilenberg-Moore objects.
We show that every monad $m$ gives rise to an adjunction and that the monad coming from this adjunction is equivalent to $m$.

\begin{problem}
\label{prob:mnd-to-adj}
Given a bicategory $\B$ with Eilenberg-Moore objects and a monad $m$ in $\B$, to construct an adjunction $\mndtoadj{m}$ and an adjoint equivalence $\mndtoadjequiv{m}$ between $\adjtomnd{\mndtoadj{m}}$ and $m$.
\end{problem}

\begin{construction}[\coqident{Bicategories.Monads.MonadToAdjunction}{mnd_to_adjunction}]{prob:mnd-to-adj}
\label{constr:mnd-to-adj}
The right adjoint is the 1-cell $\emmor{e} : \monadob{m} \onecell \emlim{\B}{m}$.
For the left adjoint, we need to define a 1-cell $\freealg{m} : \emlim{\B}{m} \onecell \monadob{m}$, and we use the universal property of Eilenberg-Moore objects for that.
We construct a cone $q$ as follows:
\begin{itemize}
\item The object is $\monadob{m}$;
\item The morphism is $\monadendo{m}$;
\item The 2-cell is
\begin{tikzcd}
{\comp{\monadendo{m}}{\monadendo{m}}} & {\monadendo{m}} & {\comp{\id{\monadob{m}}}{\monadendo{m}}.}
\arrow["{\monadmult{m}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\linvunitor{\monadendo{m}}}", from=1-2, to=1-3, Rightarrow]
\end{tikzcd}
\end{itemize}
We define $\freealg{m}$ as $\emumpmor{q}$.
The unit of the desired adjunction is defined as follows:
\[
\begin{tikzcd}[column sep = huge]
{\id{\monadob{m}}} & {\monadendo{m}} & {\comp{\freealg{m}}{\emmor{e}}}
\arrow["{\monadunit{m}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\emumpcom{q}}", from=1-2, to=1-3, Rightarrow]
\end{tikzcd}
\]
For the counit we use the universal property of Eilenberg-Moore objects.
The details can be found in the formalization.

To construct $\mndtoadjequiv{m}$, we use \cref{prop:mnd-adjequiv}.
Hence, it suffices to construct a monad morphism $G : \adjtomnd{\mndtoadj{m}} \onecell m$ whose underlying 1-cell and 2-cell are an adjoint equivalence and invertible respectively.
We define $G$ as follows:
\begin{itemize}
\item The underlying 1-cell is $\id{\monadob{m}} : \monadob{m} \onecell \monadob{m}$.
\item For the underlying 2-cell, we take
\[
\begin{tikzcd}
{\comp{\id{\monadob{m}}}{\monadendo{m}}} &[1em] {\monadendo{m}} & [2em]{\comp{\freealg{m}}{\emmor{e}}} &[2em] {\comp{(\comp{\freealg{m}}{\emmor{e}})}{\id{\monadob{m}}}}
\arrow["{\lunitor{\monadendo{m}}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\emumpcom{q}}", from=1-2, to=1-3, Rightarrow]
\arrow["{\rinvunitor{\comp{\freealg{m}}{\emmor{e}}}}", from=1-3, to=1-4, Rightarrow]
\end{tikzcd}
\qedhere
\]
\end{itemize}
\end{construction}
Note that we can instantiate \cref{constr:mnd-to-adj} to several concrete instances.
\begin{itemize}
\item Since $\UnivCat$ has Eilenberg-Moore objects by \cref{ex:em-cats}, we get the usual construction of adjunctions from monads via Eilenberg-Moore categories.
\item Since $\opbicat{\UnivCat}$ has Eilenberg-Moore objects by \cref{constr:univ-kleisli-cats}, every monad gives rise to an adjunction via Kleisli categories.
\end{itemize}
One can also show that $\cobicat{\SymMonCat}$ has Eilenberg-Moore objects, and thus every comonad of symmetric monoidal categories gives rise to an adjunction.
This is used to construct models of linear logic [32].

\section{Monadic Adjunctions}
\label{sec:monadic}
By \cref{constr:mnd-to-adj} we have an equivalence $\adjtomnd{\mndtoadj{m}} \simeq m$ for every monad $m$.
However, such a statement does not hold for adjunctions.
\emph{Monadic adjunctions} are the adjunctions for which we do have such an equivalence.

\begin{problem}
\label{prob:comparison}
Given an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ where $l : x \onecell y$ in a bicategory $\B$ with Eilenberg-Moore objects,
to construct a 1-cell $\comparison{\adjunction{l}{r}{\eta}{\varepsilon}} : y \onecell \emlim{\B}{\adjtomnd{\adjunction{l}{r}{\eta}{\varepsilon}}}$.
\end{problem}

\begin{construction}[\coqident{Bicategories.Morphisms.Monadic}{comparison_mor}]{prob:comparison}
\label{constr:comparison}
We use the universal property of Eilenberg-Moore objects, and we construct a cone $q$ as follows
\begin{itemize}
\item The object is $y$;
\item The 1-cell is $r : y \onecell x$;
\item The 2-cell is
\begin{tikzcd}
{\comp{r}{(\comp{l}{r})}} & {\comp{(\comp{r}{l})}{r}} & {\comp{\id{y}}{r}}
\arrow["{\lassociator{r}{l}{r}}", from=1-1, to=1-2, Rightarrow]
\arrow["{\varepsilon \whiskerr r}", from=1-2, to=1-3, Rightarrow]
\end{tikzcd}.
\end{itemize}
Note that the object and 1-cell of $\adjtomnd{\adjunction{l}{r}{\eta}{\varepsilon}}$ are $x$ and $\comp{l}{r}$ respectively.
Now we define $\comparison{\adjunction{l}{r}{\eta}{\varepsilon}}$ to be $\emumpmor{q}$.
\end{construction}

\begin{defi}[\coqident{Bicategories.Morphisms.Monadic}{is_monadic}]
An adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ in a bicategory $\B$ with Eilenberg-Moore objects is called \textbf{monadic} if the 1-cell $\comparison{\adjunction{l}{r}{\eta}{\varepsilon}}$ is an adjoint equivalence.
\end{defi}

Next we look at a representable version of this definition.
More specifically, we define monadic 1-cells using monadic functors in $\UnivCat$.
To do so, we first show that every adjunction gives rise to an adjunction on the hom-categories.

\begin{problem}
\label{prob:hom-adj}
Given $\adjunction{l}{r}{\eta}{\varepsilon}$ where $l : x \onecell y$ and an object $w$, to construct an adjunction $\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}$ between $\homC{\B}{w}{x}$ and $\homC{\B}{w}{y}$.
\end{problem}

\begin{construction}[\coqident{Bicategories.Morphisms.Properties.AdjunctionsRepresentable}{left_adjoint_to_adjunction_cat}]{prob:hom-adj}
\label{constr:hom-adj}
The left adjoint is $\postcomp{l}{w}$, while the right adjoint is $\postcomp{r}{w}$.
For the unit, we need to construct natural 2-cells $f \twocell \comp{(\comp{f}{l})}{r}$, and for which we take
\[
\begin{tikzcd}
f & {\comp{f}{\id{y}}} & {\comp{f}{(\comp{l}{r})}} & {\comp{(\comp{f}{l})}{r}}
\arrow["{\rinvunitor{f}}", from=1-1, to=1-2, Rightarrow]
\arrow["{f \whiskerl \eta}", from=1-2, to=1-3, Rightarrow]
\arrow["{\lassociator{f}{l}{r}}", from=1-3, to=1-4, Rightarrow]
\end{tikzcd}
\]
For the counit, we construct natural 2-cells $\comp{(\comp{f}{r})}{l}$, which are defined as follows
\[
\begin{tikzcd}
{\comp{(\comp{f}{r})}{l}} & {\comp{f}{(\comp{r}{l})}} & {\comp{f}{\id{y}}} & f
\arrow["{\rassociator{f}{r}{l}}", from=1-1, to=1-2, Rightarrow]
\arrow["{f \whiskerl \varepsilon}", from=1-2, to=1-3, Rightarrow]
\arrow["{\runitor{f}}", from=1-3, to=1-4, Rightarrow]
\end{tikzcd} \qedhere
\]
\end{construction}
% If we have an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ with $l : x \onecell y$ and an object $w$, then we also get an adjunction $\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}$ between $\homC{\B}{w}{x}$ and $\homC{\B}{w}{y}$.

\begin{defi}[\coqident{Bicategories.Morphisms.Monadic}{is_monadic_repr}]
\label{def:repr-monadic}
An adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ in a locally univalent bicategory is called \textbf{representably monadic} if
for every $w \in \B$ the adjunction $\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}$ is a monadic 1-cell in $\UnivCat$.
\end{defi}

Note that we require the bicategory in \cref{def:repr-monadic} to be locally univalent, so that each hom-category lies in $\UnivCat$.
Now we show that these two notions of monadicity are equivalent.
We first prove the following lemma.

\begin{lem}[\coqident{Bicategories.Morphisms.Properties.AdjunctionsRepresentable}{left_adjoint_equivalence_weq_left_adjoint_equivalence_repr}]
\label{prop:repr-adjequiv}
A 1-cell $f : x \onecell y$ is an adjoint equivalence if and only if for all $w$ the functor $\postcomp{f}{w}$ is an adjoint equivalence of categories.
\end{lem}

\begin{proof}
Suppose, we have a a adjoint equivalence $f : \adjequiv{x}{y}$ and let $w : \B$.
By \cref{constr:hom-adj}, we obtain an adjunction $\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}$ between $\homC{\B}{w}{x}$ and $\homC{\B}{w}{y}$ whose right adjoint is $\postcomp{f}{w}$.
Since the unit and counit of $f$ are invertible, the unit and counit of $\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}$ are invertible as well, and thus we get the desired adjoint equivalence.

Next suppose that for every $w$ the functor $\postcomp{f}{w}$ is an adjoint equivalence.
For every $w$, we denote its right adjoint by $R_w : \homC{\B}{w}{y} \onecell \homC{\B}{w}{x}$, its unit by $\eta_w : \comp{R_w}{\postcomp{f}{w}} \twocell \idimpl{\homC{\B}{w}{y}}$, and its counit by $\varepsilon_w : \idimpl{\homC{\B}{w}{x}} \twocell \comp{\postcomp{f}{w}}{R_w}$.
Now we show that $f$ is an adjoint equivalence
\begin{itemize}
\item The right adjoint is $R_y(\id{y}) : \homC{\B}{y}{x}$.
\item The unit is $\eta_w(\id{y}) : \comp{R_y(\id{y})}{f} \twocell \id{y}$.
\item For the counit, we use the following composition
\[
\begin{tikzcd}[row sep=large]
{\comp{f}{R_y(\id{y})}} &[3em] {\comp{R_x((\comp{f}{R_y(\id{y})})}{f})} &[2em] {R_x(\comp{f}{(\comp{R_y(\id{y})}{f})})} \\
{R_x(\comp{f}{\id{y}})} & {R_x(f)} & {R_x(\comp{\id{x}}{f})} & {\id{x}}
\arrow["{\eta_x(\comp{f}{R_y(\id{y})})}", from=1-1, to=1-2, Rightarrow]
\arrow["{R(\rassociator{f}{R_y(\id{y})}{f})}", from=1-2, to=1-3, Rightarrow]
\arrow["{R(f \whiskerl \eta_y(\id{y}))}"{description}, from=1-3, to=2-1, Rightarrow]
\arrow["{R(\runitor{f})}"', from=2-1, to=2-2, Rightarrow]
\arrow["{R(\linvunitor{f})}"', from=2-2, to=2-3, Rightarrow]
\arrow["{\eta_x^{-1}(\id{x})}"', from=2-3, to=2-4, Rightarrow]
\end{tikzcd}
\]
\end{itemize}
Since both the unit and counit are invertible, $f$ is indeed an adjoint equivalence.
\end{proof}

\begin{thrm}[\coqident{Bicategories.Morphisms.Monadic}{is_monadic_repr_weq_is_monadic}]
\label{prop:repr-monadic}
An adjunction is monadic if and only if it is representably monadic.
\end{thrm}

\begin{proof}
Suppose that we have an adjunction $\adjunction{l}{r}{\eta}{\varepsilon}$ and that we have $w : \B$.
First, we note that we have a monad on $\homC{\B}{w}{y}$, namely $m \defeq \hommonad{w}{\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}}$.
We denote the comparison cell $\comparison{\homadj{w}{\adjunction{l}{r}{\eta}{\varepsilon}}}$ by $F$.

We also have a functor $\postcomp{\comparison{\adjunction{l}{r}{\eta}{\varepsilon}}}{w} : \homC{\B}{w}{y} \onecell \homC{\B}{w}{\emlim{\B}{m'}}$, which we denote by $G$.
We write $m'$ for the monad $\hommonad{w}{m}$, and recall that by \cref{prop:em-ump} we have an adjoint equivalence from $\homC{\B}{w}{\emlim{\B}{m'}}$ to $\emlim{}{\hommonad{w}{m}}$.
Denote this equivalence by $H$.
There also is a functor $K : \emlim{}{m'} \onecell \emlim{}{m}$ and a natural isomorphism $\tau : \invcell{\comp{F}{(\comp{H}{K})}}{G}$: their precise definition can be found in the formalization.

As such, we have the following diagram for every $w : \B$:
\[
\begin{tikzcd}[column sep = huge]
{\homC{\B}{w}{y}} & {\emlim{}{m}} \\
{\homC{\B}{w}{\emlim{\B}{m'}}} & {\emlim{}{m'}}
\arrow[""{name=0, anchor=center, inner sep=0}, "G", from=1-1, to=1-2]
\arrow["F"', from=1-1, to=2-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "H"', from=2-1, to=2-2]
\arrow["K"', from=2-2, to=1-2]
\arrow["\tau"', shorten <=5pt, shorten >=5pt, Rightarrow, from=1, to=0]
\end{tikzcd}
\]
Since both $H$ and $K$ are adjoint equivalences, we deduce that $F$ is an adjoint equivalence if and only if $G$ is.
As such, if $\adjunction{l}{r}{\eta}{\varepsilon}$ is representably monadic, then $F$ is an adjoint equivalence and thus $G$ is an adjoint equivalence.
From \cref{prop:repr-adjequiv} we get that $\adjunction{l}{r}{\eta}{\varepsilon}$ is monadic.
For the converse, we use the same argument: if $\adjunction{l}{r}{\eta}{\varepsilon}$ is monadic, then $G$ is an adjoint equivalence.
Hence, $F$ is an adjoint equivalence as well, so $\adjunction{l}{r}{\eta}{\varepsilon}$ is representably monadic.
\end{proof}

\section{Conclusion}
\label{sec:concl}
We studied Street's formal theory of monads in this paper.
We saw that it provides a good setting to study monads in univalent foundations, because it allows us to prove the core theorems in arbitrary bicategories instead of only for categories.
For that reason, it helps us with concrete problems, such as constructing an adjunction from a monad using the univalent version of the Kleisli category.
This is because one only needs to prove a universal property instead of reproducing the whole construction of the adjunction.

There are numerous ways to continue this line of research.
One result that is missing, is Theorem 12 from Street's paper about comonads [45].
In addition, the work in this setting provides a framework in which one can study numerous applications, such as models of linear logic [32], Moggi-style semantics [34], and call-by-push-value [29], and formalizing these applications would be a worthwhile extension.
Finally, one could study extensions of the formal theory to a wider class of monads, such as graded monads [17].

\nocite{ahrens2022semantics-lics,univalence-principle-lics}

\begin{thebibliography}{10}

[1]
{The Lean mathematical library}.
\newblock In Jasmin Blanchette and Catalin Hritcu, editors, {\em 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.
\newblock \href {https://doi.org/10.1145/3372885.3373824}

[2]
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van~der
\newblock Bicategories in univalent foundations.
\newblock {\em Mathematical Structures in Computer Science}, page 1–38, 2022.
\newblock \href {https://doi.org/10.1017/S0960129522000032}

[3]
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman.
\newblock {Univalent categories and the Rezk completion}.
\newblock {\em Mathematical Structures in Computer Science}, 25:1010--1039,
\newblock \href {http://arxiv.org/abs/1303.0584} {\path{arXiv:1303.0584}},
\href {https://doi.org/10.1017/S0960129514000486}

[4]
Benedikt Ahrens and Peter~LeFanu Lumsdaine.
\newblock {Displayed Categories}.
\newblock {\em Logical Methods in Computer Science}, 15(1), 2019.
\newblock \href {https://doi.org/10.23638/LMCS-15(1:20)2019}

[5]
Benedikt Ahrens, Ralph Matthes, and Anders M{\"{o}}rtberg.
\newblock {From Signatures to Monads in UniMath}.
\newblock {\em J. Autom. Reason.}, 63(2):285--318, 2019.
\newblock \href {https://doi.org/10.1007/s10817-018-9474-4}

[6]
Benedikt Ahrens, Ralph Matthes, and Anders M{\"{o}}rtberg.
\newblock Implementing a category-theoretic framework for typed abstract
\newblock In Andrei Popescu and Steve Zdancewic, editors, {\em {CPP} '22: 11th
{ACM} {SIGPLAN} International Conference on Certified Programs and Proofs,
Philadelphia, PA, USA, January 17 - 18, 2022}, pages 307--323. {ACM}, 2022.
\newblock \href {https://doi.org/10.1145/3497775.3503678}

[7]
Benedikt Ahrens, Paige~Randall North, Michael Shulman, and Dimitris Tsementzis.
\newblock A higher structure identity principle.
\newblock In {\em Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in
Computer Science}, LICS '20, page 53–66, New York, NY, USA, 2020.
Association for Computing Machinery.
\newblock \href {https://doi.org/10.1145/3373718.3394755}

[8]
Benedikt Ahrens, Paige~Randall North, Michael Shulman, and Dimitris Tsementzis.
\newblock {The Univalence Principle}.
\newblock 2021.
\newblock Extended version of [7].
\newblock \href {http://arxiv.org/abs/2102.06275v2}
{\path{arXiv:2102.06275v2}}, \href {https://doi.org/10.1145/3373718.3394755}

[9]
Benedikt Ahrens, Paige~Randall North, and Niels van~der Weide.
\newblock Semantics for two-dimensional type theory.
\newblock 2022.
\newblock Extended version of [10].
\newblock \href {http://arxiv.org/abs/2201.10662v3}

[10]
Benedikt Ahrens, Paige~Randall North, and Niels van~der Weide.
\newblock Semantics for two-dimensional type theory.
\newblock In {\em Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in
Computer Science}, LICS '22, New York, NY, USA, 2022. Association for
Computing Machinery.
\newblock \href {https://doi.org/10.1145/3531130.3533334}

[11]
Andrej Bauer, Jason Gross, Peter~LeFanu Lumsdaine, Michael Shulman, Matthieu
Sozeau, and Bas Spitters.
\newblock {The HoTT library: a formalization of homotopy type theory in Coq}.
\newblock In Yves Bertot and Viktor Vafeiadis, editors, {\em Proceedings of the
6th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs, {CPP} 2017,
Paris, France, January 16-17, 2017}, pages 164--172. {ACM}, 2017.
\newblock \href {https://doi.org/10.1145/3018610.3018615}

[12]
Jean B{\'e}nabou.
\newblock Introduction to bicategories.
\newblock In {\em Reports of the Midwest Category Seminar}, pages 1--77,
Berlin, Heidelberg, 1967. Springer Berlin Heidelberg.
\newblock \href {https://doi.org/10.1007/BFb0074299}

[13]
Gabriella B{\"o}hm, Stephen Lack, and Ross Street.
\newblock On the 2-categories of weak distributive laws.
\newblock {\em Communications in Algebra}, 39(12):4567--4583, 2011.

[14]
Matteo Capucci and Bruno Gavranovi{\'c}.
\newblock {Actegories for the Working Amthematician}.
\newblock {\em arXiv preprint arXiv:2203.16351}, 2022.

[15]
Eugenia Cheng.
\newblock Iterated distributive laws.
\newblock In {\em Mathematical Proceedings of the Cambridge Philosophical
Society}, volume 150, pages 459--487. Cambridge University Press, 2011.

[16]
Ivan Di~Liberti and Fosco Loregian.
\newblock On the unicity of formal category theories.
\newblock {\em arXiv preprint arXiv:1901.01594}, 2019.

[17]
Soichiro Fujii, Shin{-}ya Katsumata, and Paul{-}Andr{\'{e}} Melli{\`{e}}s.
\newblock {Towards a Formal Theory of Graded Monads}.
\newblock In Bart Jacobs and Christof L{\"{o}}ding, editors, {\em Foundations
of Software Science and Computation Structures - 19th International
Conference, {FOSSACS} 2016, Held as Part of the European Joint Conferences on
Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
April 2-8, 2016, Proceedings}, volume 9634 of {\em Lecture Notes in Computer
Science}, pages 513--530. Springer, 2016.
\newblock \href {https://doi.org/10.1007/978-3-662-49630-5\_30}

[18]
Jason Gross, Adam Chlipala, and David~I. Spivak.
\newblock {Experience Implementing a Performant Category-Theory Library in
\newblock In Gerwin Klein and Ruben Gamboa, editors, {\em Interactive Theorem
Proving - 5th International Conference, {ITP} 2014, Held as Part of the
Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 14-17, 2014.
Proceedings}, volume 8558 of {\em Lecture Notes in Computer Science}, pages
275--291. Springer, 2014.
\newblock \href {https://doi.org/10.1007/978-3-319-08970-6\_18}

[19]
Jason Z.~S. Hu and Jacques Carette.
\newblock {Formalizing category theory in Agda}.
\newblock In Catalin Hritcu and Andrei Popescu, editors, {\em {CPP} '21: 10th
{ACM} {SIGPLAN} International Conference on Certified Programs and Proofs,
Virtual Event, Denmark, January 17-19, 2021}, pages 327--342. {ACM}, 2021.
\newblock \href {https://doi.org/10.1145/3437992.3439922}

[20]
Martin Hyland and John Power.
\newblock {The category theoretic understanding of universal algebra: Lawvere
theories and monads}.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 172:437--458,

[21]
Niles Johnson and Donald Yau.
\newblock {\em 2-dimensional categories}.
\newblock Oxford University Press, USA, 2021.

[22]
Simon L.~Peyton Jones and Philip Wadler.
\newblock {Imperative Functional Programming}.
\newblock In Mary S.~Van Deusen and Bernard Lang, editors, {\em Conference
Record of the Twentieth Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, Charleston, South Carolina, USA, January 1993},
pages 71--84. {ACM} Press, 1993.
\newblock \href {https://doi.org/10.1145/158511.158524}

[23]
Krzysztof Kapulkin and Peter~LeFanu Lumsdaine.
\newblock {The Simplicial Model of Univalent Foundations (after Voevodsky)}.
\newblock {\em Journal of the European Mathematical Society}, 23(6):2071--2126,
\newblock \href {https://doi.org/10.4171/JEMS/1050}

[24]
Max Kelly.
\newblock {\em Basic concepts of enriched category theory}, volume~64.
\newblock CUP Archive, 1982.

[25]
Stephen Lack.
\newblock Composing props.
\newblock {\em Theory and Applications of Categories}, 13(9):147--163, 2004.

[26]
Stephen Lack.
\newblock A 2-categories companion.
\newblock In {\em Towards higher categories}, pages 105--191. Springer, 2010.

[27]
Stephen Lack and Ross Street.
\newblock The formal theory of monads {II}.
\newblock {\em Journal of pure and applied algebra}, 175(1-3):243--265, 2002.

[28]
Tom Leinster.
\newblock {Basic Bicategories}, 1998.
\newblock \href {http://arxiv.org/abs/math/9810017}

[29]
Paul~Blain Levy.
\newblock {\em Call-by-push-value: A Functional/imperative Synthesis},
\newblock Springer Science \& Business Media, 2012.

[30]
Saunders Mac~Lane.
\newblock {\em Categories for the working mathematician}, volume~5.
\newblock Springer Science \& Business Media, 2013.

[31]
Saunders MacLane and Robert Par{\'e}.
\newblock Coherence for bicategories and indexed categories.
\newblock {\em Journal of Pure and Applied Algebra}, 37:59--80, 1985.

[32]
Paul-Andr{\'e} Mellies.
\newblock Categorical semantics of linear logic.
\newblock {\em Panoramas et syntheses}, 27:15--215, 2009.

[33]
Eugenio Moggi.
\newblock Computational lambda-calculus and monads.
\newblock In {\em 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.
\newblock \href {https://doi.org/10.1109/LICS.1989.39155}

[34]
Eugenio Moggi.
\newblock Notions of computation and monads.
\newblock {\em Information and computation}, 93(1):55--92, 1991.

[35]
Tobias Nipkow, Lawrence~C Paulson, and Markus Wenzel.
\newblock {\em {Isabelle/HOL: a proof assistant for higher-order logic}},
volume 2283.
\newblock Springer Science \& Business Media, 2002.

[36]
Ulf Norell.
\newblock {Dependently typed programming in Agda}.
\newblock In {\em Proceedings of the 4th international workshop on Types in
language design and implementation}, pages 1--2, 2009.

[37]
Gordon Plotkin and John Power.
\newblock Notions of computation determine monads.
\newblock In {\em International Conference on Foundations of Software Science
and Computation Structures}, pages 342--356. Springer, 2002.

[38]
Gordon Plotkin and John Power.
\newblock Algebraic operations and generic effects.
\newblock {\em Applied categorical structures}, 11(1):69--94, 2003.

[39]
John Power.
\newblock Coherence for bicategories with finite bilimits {I}.
\newblock In {\em Categories in computer science and logic}, volume 92 of
\emph{Contemporary Mathematics}, pages 341--347, 1989.

[40]
John Power.
\newblock Enriched {L}awvere theories.
\newblock {\em Theory and Applications of Categories}, 6(7):83--93, 1999.

[41]
John Power and Edmund Robinson.
\newblock {A Characterization of PIE Limits}.
\newblock {\em Mathematical Proceedings of the Cambridge Philosophical
Society}, 110:33--47, 1991.

[42]
John Power and Hiroshi Watanabe.
\newblock Combining a monad and a comonad.
\newblock {\em Theoretical Computer Science}, 280(1-2):137--162, 2002.

[43]
Egbert Rijke, Elisabeth Bonnevier, Jonathan Prieto-Cubides, et~al.
\newblock Univalent mathematics in {Agda}.
\newblock \url{https://unimath.github.io/agda-unimath/}.
\newblock URL: \url{https://github.com/UniMath/agda-unimath/}.

[44]
Eugene~W. Stark.
\newblock Bicategories.
\newblock {\em Arch. Formal Proofs}, 2020, 2020.
\newblock URL: \url{https://www.isa-afp.org/entries/Bicategory.html}.

[45]
Ross Street.
\newblock The formal theory of monads.
\newblock {\em Journal of Pure and Applied Algebra}, 2(2):149--168, 1972.

[46]
The Coq~Development Team.
\newblock {The Coq Proof Assistant}, January 2022.
\newblock \href {https://doi.org/10.5281/zenodo.5846982}

[47]
{The 1Lab Developers}.
\newblock {1Lab}.
\newblock \url{https://github.com/plt-amy/1lab/}.
\newblock URL: \url{https://github.com/plt-amy/1lab/}.

[48]
The {Univalent Foundations Program}.
\newblock {\em {Homotopy Type Theory: Univalent Foundations of Mathematics}}.
\newblock \url{https://homotopytypetheory.org/book}, Institute for Advanced
Study, 2013.

[49]
Niccolò Veltri and Niels van~der Weide.
\newblock {Constructing Higher Inductive Types as Groupoid Quotients}.
\newblock {\em {Logical Methods in Computer Science}}, {Volume 17, Issue 2},
April 2021.
\newblock URL: \url{https://lmcs.episciences.org/7391}.

[50]
Andrea Vezzosi, Anders M{\"{o}}rtberg, and Andreas Abel.
\newblock {Cubical Agda: a dependently typed programming language with
univalence and higher inductive types}.
\newblock {\em Proc. {ACM} Program. Lang.}, 3({ICFP}):87:1--87:29, 2019.
\newblock \href {https://doi.org/10.1145/3341691} {\path{doi:10.1145/3341691}}.

[51]
Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et~al.
\newblock {UniMath --- a computer-checked library of univalent mathematics}.
\newblock {Available} at \url{https://github.com/UniMath/UniMath}.

[52]
Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens.
\newblock Univalent monoidal categories.
\newblock {\em arXiv preprint arXiv:2212.03146}, 2022.

\end{thebibliography}

\end{document}