double.tex

% -*- root: thesis.tex -*-

\chapter{DOUBLE CATEGORIES}\label{Ch:Double}

Recall in~\cref{Def:FFColax}, a colax morphism of functorial factorizations is a pair $(F,\phi)$, where $\phi$ is a natural transformation
\begin{equation}\label{Eq:FFColaxSquare}
\begin{tikzcd}
	C^2 \rar[][domA]{E_1} \dar[swap]{\hat{F}} & C \dar{F} \\
	D^2 \rar[][codA,swap]{E_2} & D
	\twocellA{\phi}
\end{tikzcd}
\end{equation}
In~\cite{riehl:nwfs-model} it is proven that if $F\dashv G$ is an adjunction, then specifying a natural transformation $\phi$ making $F$ a colax morphism uniquely determines a natural transformation $\theta$ making $G$ a lax morphism. The transformation $\theta$ is called the \emph{mate} of $\phi$, and is found by composing $\phi$ with the unit and counit of $\hat{F}$ and $F$ respectively.

This mates correspondence (see~\cref{Ex:DoubleLAdj}) defines a bijection between natural transformations of the form~\eqref{Eq:FFColaxSquare} and natural transformations of the form
\[
\begin{tikzcd}
	C^2 \rar[][domA]{E_1} & C \\
	D^2 \uar{\hat{G}} \rar[][codA,swap]{E_2} & D. \uar[swap]{G}
	\twocellA{\theta}
\end{tikzcd}
\]
The collection of square 2-cells, where the vertical 1-cells are required to be the left adjoint of an adjunction, and the horizontal 1-cells are allowed to be arbitrary functors, can be organized into a structure called a \emph{double category}. Similarly, there is a double category where the vertical 1-cells are required to be right adjoints (with some subtlety regarding the direction vertical 1-cells and 2-cells point), and the naturality of the mates correspondence can be expressed by saying these two double categories are isomorphic.

Double categories are a fundamental structure for this thesis, primarily due to the importance of the mates correspondence to the algebraic analogue of Quillen functors: lax and colax morphisms of awfs.

In~\cref{Sec:DblCatReview}, we begin by giving an overview of double categories. Then in \cref{Sec:ArrowObjects} we give a generalization of~\cref{Def:ArrowObject}, defining arrow objects in a double category by means of a universal property. This is needed to be able to define functorial factorizations and (co)lax morphisms of functorial factorizations in general double categories, which we do in~\cref{Ch:FuncFact}.

We will ultimately want to define an algebraic weak factorization system to be a sort of bialgebraic object in a (two-fold) double category. To prepare the way for this definition, in~\cref{Sec:DblCatMonads} we give (one possible version of) the definition of monads in a double category.

\section{Review of Double Categories}\label{Sec:DblCatReview}

We first give the most concise definition of a double category, which we will then break down into more concrete terms.

\begin{definition}\label{Def:DoubleCat}
	A (strict) \emph{double category} is an internal category object in the (large) category of categories.
\end{definition}

So a double category $\dblcat{D}$ consists of a category $\dblcat{D}_0$ and a category $\dblcat{D}_1$, along with functors $s,t\colon \dblcat{D}_1\to \dblcat{D}_0$, $i\colon \dblcat{D}_0\to \dblcat{D}_1$, and $\otimes\colon \dblcat{D}_1\times_{\dblcat{D}_0}\dblcat{D}_1\to \dblcat{D}_1$ satisfying the usual axioms of a category. We will call the objects of $\dblcat{D}_0$ the 0-cells (or just objects) of $\dblcat{D}$, and the morphisms of $\dblcat{D}_0$ the vertical 1-cells. Thus $\dblcat{D}_0$ forms the so-called \emph{vertical category} of $\dblcat{D}$. We will call the objects of $\dblcat{D}_1$ the horizontal 1-cells of $\dblcat{D}$, and the morphisms of $\dblcat{D}_1$ are the 2-cells. 

A morphism $\phi\colon X\to Y$ in $\dblcat{D}_1$, where $s(X)=C$, $t(X)=C'$, $s(Y)=D$, $t(Y)=D'$, $s(\phi)=f$, and $t(\phi)=g$ will be drawn as
\begin{equation}\label{Eq:Double2Cell}
\begin{tikzcd}
	C \rar[tick][domA]{X} \dar[swap]{f} 
		& C' \dar{g} \\
	D \rar[tick][codA,swap]{Y} 
		& D'
	 \twocellA{\phi}
\end{tikzcd}
\end{equation}
where the tick-mark on the horizontal 1-cells serves as a further reminder that the horizontal 1-cells are of a different nature than the vertical 1-cells. The composition in $\dblcat{D}_0$ provides a vertical composition of vertical 1-cells and 2-cells, while the composition functor $\otimes\colon \dblcat{D}_1\times_{\dblcat{D}_0}\dblcat{D}_1\to \dblcat{D}_1$ provides a horizontal composition of horizontal 1-cells and 2-cells.

For any object $C$ in $\dblcat{D}_0$, $i(C)$ is the \emph{unit} horizontal 1-cell
\[
\begin{tikzcd}
	C \rar[tick]{I_C} & C
\end{tikzcd}
\]
and acts as an identity with respect to the horizontal composition.

A 2-cell $\theta$ for which $s\theta=t\theta=\id$ will be called \emph{globular}. We will sometimes draw globular 2-cells as
\[
\begin{tikzcd}[bend angle=30]
	C \rar[bend left,tick][domA]{X}
		\rar[bend right,tick][codA,swap]{Y}
	& C',
	\twocellA{\theta}
\end{tikzcd}
\]
to save space and help readability of diagrams.

\begin{example}\label{Ex:SqD}
	For any 2-category $\twocat{D}$, there is an associated double category $\Sq(\twocat{D})$ of \emph{squares} in $\twocat{D}$, in which the vertical and horizontal 1-cells are both just 1-cells in $\twocat{D}$, and 2-cells
	\[
	\begin{tikzcd}
		C \rar[tick][domA]{j} \dar[swap]{f} 
			& C' \dar{g} \\
		D \rar[tick][codA,swap]{k} 
			& D'
		\twocellA{\phi}
	\end{tikzcd}
	\]
	are simply 2-cells $\phi\colon gj\Rightarrow kf$ in $\twocat{D}$.
\end{example}

\begin{example}\label{Ex:DoubleLAdj}
	Given any 2-category $\twocat{D}$, there is a double category $\LAdj(\twocat{D})$. The horizontal 1-cells are just 1-cells in $\twocat{D}$, while the vertical 1-cells are fully specified adjunctions $f\dashv g$ (meaning the unit and counit have been chosen) pointing in the direction of the left adjoint. 2-cells
	\[
	\begin{tikzcd}
		C \rar[tick][domA]{j} \dar[swap]{(f\dashv g)} 
			& C' \dar{(f'\dashv g')} \\
		D \rar[tick][codA,swap]{k} 
			& D'
		\twocellA{\phi}
	\end{tikzcd}
	\]
	are natural transformations involving the left adjoints, $\phi\colon f'j\Rightarrow kf$.

	Similarly there is a double category $\RAdj(\twocat{D})$ where the vertical 1-cells still point in the direction of the left adjoint, but the 2-cells are natural transformations involving the right adjoints, $\phi\colon jg\Rightarrow g'k$.

	The \emph{mates correspondence} (see e.g.~\cite{cgr:mates}) gives an isomorphism $\LAdj(\twocat{D})\cong\RAdj(\twocat{D})$, which sends a 2-cell $\phi$ in $\LAdj(\twocat{D})$ to the 2-cell
	\[
	\begin{tikzcd}[column sep=2ex]
		{} & |[alias=domA]| C \rar[][domB]{j} \dar{f}
			&[3ex] C' \dar[swap]{f'} \rar[equal][domC]{}
			& C' \\
		D \rar[equal][codA]{} \urar{g}
			& D \rar[][codB,swap]{k}
			& |[alias=codC]| D' \urar[swap]{g'} &
		\twocellA[pos=.7]{\epsilon}
		\twocellB{\phi}
		\twocellC[pos=.3]{\eta}
	\end{tikzcd}
	\]
	given by composing with the unit/counit of the adjunctions.
\end{example}

\begin{example}\label{Ex:Span}
	Given any category $\cat{M}$, there is a pseudo double category $\Span(\cat{M})$ of \emph{spans} in $\cat{M}$. The vertical category of $\Span(\cat{M})$ is just $\cat{M}$, while horizontal 1-cells
	\[
	\begin{tikzcd}
		C \rar[tick][]{X} & D
	\end{tikzcd}
	\]
	are given by spans
	\[
	\begin{tikzcd}
		C & X \lar[swap]{j} \rar{k} & D
	\end{tikzcd}
	\]
	in $\cat{M}$, and 2-cells
	\[
	\begin{tikzcd}
		C \rar[tick][domA]{X} \dar[swap]{f} & D \dar{g} \\
		C' \rar[tick][swap,codA]{Y} & D'
		\twocellA{\theta}
	\end{tikzcd}
	\]
	are given by commutative diagrams
	\[
	\begin{tikzcd}
		C \dar[swap]{f} & X \lar[swap]{j} \rar{k} \dar{\theta} & D \dar{g} \\
		C' & Y \lar{j'} \rar[swap]{k'} & D.'
	\end{tikzcd}
	\]
	The horizontal composition of spans is given by pullback. It is because this horizontal composition is only determined up to isomorphsim that this example is not a strict double category.
\end{example}

\begin{definition}
	For any double category $\dblcat{D}$, there is an associated 2-category $\Hor(\dblcat{D})$, called the \emph{horizontal 2-category} of $\dblcat{D}$. The objects and 1-cells of $\Hor(\dblcat{D})$ are the objects and horizontal 1-cells of $\dblcat{D}$, while 2-cells $\phi\colon X\Rightarrow Y$ in $\Hor(\dblcat{D})$ are the globular 2-cells in $\dblcat{D}$, i.e. those of the form
	\[
	\begin{tikzcd}
		C \rar[tick][domA]{X} \dar[equal] 
			& D \dar[equal] \\
		C \rar[tick][codA,swap]{Y} 
			& D
		\twocellA{\phi}
	\end{tikzcd}
	\]
	Notice that $\Hor(\Sq(\mathcal{D}))$ is isomorphic to $\mathcal{D}$.
\end{definition}

\begin{definition}
	Given a double category $\dblcat{D}$, define double categories $\vop{\dblcat{D}}$ and $\hop{\dblcat{D}}$, obtained by reversing the direction of the vertical and horizontal 1-cells respectively, and changing the orientation of the 2-cells as appropriate. For example, a 2-cell~\eqref{Eq:Double2Cell} in $\vop{\dblcat{D}}$ is a 2-cell
	\[
	\begin{tikzcd}
		D \rar[tick][domA]{Y} \dar[swap]{f} 
		& D' \dar{g} \\
	C \rar[tick][codA,swap]{X} 
		& C'
	 \twocellA{\phi}
	\end{tikzcd}
	\]
	in $\dblcat{D}$.

	In terms of \cref{Def:DoubleCat}, $\vop{\dblcat{D}}$ is the double category obtained by replacing the categories $\dblcat{D}_0$ and $\dblcat{D}_1$ with their opposites, while $\vop{\dblcat{D}}$ is the obtained by swapping the horizontal source and target functors $s$ and $t$.
\end{definition}

\section{Arrow Objects in a Double Category}\label{Sec:ArrowObjects}

In the following we will need an extension of the universal property~\eqref{Eq:ArrowObject} to double categories. Fortunately, this is quite straightforward.

Let $\dblcat{D}$ be a double category. Given an object $C$ of $\dblcat{D}$, the \emph{arrow object} $C^2$, if it exists, is an object together with a diagram
\[
\begin{tikzcd}[bend angle=30]
	C^2 \rar[bend left,tick][domA]{\dom}
		\rar[bend right,tick][codA,swap]{\cod}
	& C,
	\twocellA{\kappa}
\end{tikzcd}
\]
such that any 2-cell
\[
\begin{tikzcd}[bend angle=30]
	A \rar[bend left,tick][domA]{d_1}
		\rar[bend right,tick][codA,swap]{d_0}
	& C
	\twocellA{\alpha}
\end{tikzcd}
\]
uniquely factors through $\kappa$, as
\[
\begin{tikzcd}[bend angle=30]
	A \rar[tick][]{\hat{\alpha}} 
		& C^2 \rar[bend left,tick][domA]{\dom}
			\rar[bend right,tick][codA,swap]{\cod}
		& C.
		\twocellA{\kappa}
\end{tikzcd}
\]

Given a vertical 1-cell $F\colon C\to D$ in $\dblcat{D}$, the \emph{lift to arrow objects} $\hat{F}\colon C^2\to D^2$, if it exists, is a vertical 1-cell $\hat{F}\colon C^2\to D^2$ together with 2-cells
\[
\begin{tikzcd}
	C^2 \rar[tick][domA]{\dom} \dar[swap]{\hat{F}} & C \dar{F} \\
	D^2 \rar[tick][codA,swap]{\dom} & D
	\twocellA{\gamma_1}
\end{tikzcd}
\qquad
\begin{tikzcd}
	C^2 \rar[tick][domA]{\cod} \dar[swap]{\hat{F}} & C \dar{F} \\
	D^2 \rar[tick][codA,swap]{\cod} & D
	\twocellA{\gamma_0}
\end{tikzcd}
\]
satisfying
\[
\begin{tikzcd}[bend angle=50]
	C^2 \rar[tick][domA]{\dom} 
		\dar[swap]{\hat{F}} 
	& C \dar{F} \\
	D^2 \rar[tick][codA,domB]{\dom}	
		\rar[bend right][codB,swap]{\cod}
	& D
	\twocellA{\gamma_1}
	\twocellB{\kappa}
\end{tikzcd}
=
\begin{tikzcd}[bend angle=50]
	C^2 \rar[bend left,tick][domA]{\dom} 
		\rar[tick][codA,domB,swap]{\cod} 
		\dar[swap]{\hat{F}} 
	& C \dar{F} \\
	D^2 \rar[tick][codB,swap]{\cod} & D,
	\twocellA{\kappa}
	\twocellB{\gamma_0}
\end{tikzcd}
\]
such that for any 2-cells
\[
\begin{tikzcd}[bend angle=30]
	A \rar[bend left,tick][domA]{d_1}
		\rar[bend right,tick][codA,swap]{d_0}
	& C
	\twocellA{\alpha}
\end{tikzcd}
\quad
\begin{tikzcd}[bend angle=30]
	B \rar[bend left,tick][domA]{d'_1}
		\rar[bend right,tick][codA,swap]{d'_0}
	& D
	\twocellA{\alpha'}
\end{tikzcd}
\]
and
\[
\begin{tikzcd}
	A \rar[tick][domA]{d_1} \dar[swap]{G} & C \dar{F} \\
	B \rar[tick][codA,swap]{d'_1} & D
	\twocellA{\lambda_1}
\end{tikzcd}
\qquad
\begin{tikzcd}
	A \rar[tick][domA]{d_0} \dar[swap]{G} & C \dar{F} \\
	B \rar[tick][codA,swap]{d'_0} & D
	\twocellA{\lambda_0}
\end{tikzcd}
\]
satisfying
\[
\begin{tikzcd}[bend angle=50]
	A \rar[tick][domA]{d_1} 
		\dar[swap]{G} 
	& C \dar{F} \\
	B \rar[tick][codA,domB]{d'_1}	
		\rar[bend right,tick][codB,swap]{d'_0}
	& D
	\twocellA{\lambda_1}
	\twocellB{\alpha'}
\end{tikzcd}
=
\begin{tikzcd}[bend angle=50]
	A \rar[bend left,tick][domA]{d_1} 
		\rar[tick][codA,domB,swap]{d_0} 
		\dar[swap]{G} 
	& C \dar{F} \\
	B \rar[tick][codB,swap]{d'_0} & D
	\twocellA{\alpha}
	\twocellB{\lambda_0}
\end{tikzcd}
\]
there is a unique 2-cell
\[
\begin{tikzcd}
	A \rar[tick][domA]{\hat{\alpha}} \dar[swap]{G} & C^2 \dar{\hat{F}} \\
	B \rar[tick][codA,swap]{\hat{\alpha}'} & D^2
	\twocellA{\theta}
\end{tikzcd}
\]
such that the horizontal composition of $\theta$ with $\gamma_0$ and $\gamma_1$ is respectively equal to $\lambda_0$ and $\lambda_1$.

\begin{remark}
	Note that in most examples, the 2-cells $\gamma_0$ and $\gamma_1$ will be isomorphisms (or even identities). This just says that given any $g\colon X\to Y$ in $C^2$, the lift $\hat{F}(g)$ will be some $\hat{F}(g)\colon FX\to FY$. We are not aware of any examples where the $\gamma_i$ are not isomorphisms, though when we generalize this universal property to the multivariable setting, they will necessarily not be isomorphisms (rather they will be projections out of a pullback).
\end{remark}

\begin{definition}
	A double category $\dblcat{D}$ \emph{has arrow objects} if for every object $C$ of $\dblcat{D}$ there is an object $C^2$ and 2-cell $\kappa$, and for every vertical 1-cell $F$ there is a vertical 1-cell $\hat{F}$ and 2-cells $\gamma_0$ and $\gamma_1$, satisfying the universal properties given above.
\end{definition}

The intuition that this is a generalization of \cref{Lem:ArrowObject} is supported by the following two propositions, the (easy) proofs of which are left to the reader.

\begin{proposition}
	If the double category $\dblcat{D}$ has arrow objects, then so does $\Hor(\dblcat{D})$.
\end{proposition}

\begin{proposition}
	If the 2-category $\twocat{D}$ has arrow objects, then so does $\Sq(\twocat{D})$.
\end{proposition}
\begin{proof}
	A simple check. The 2-cells $\gamma_0$ and $\gamma_1$ will always be identities.
\end{proof}

% \begin{remark}
% 	Notice that if we take $F$ and $\hat{F}$ to both be the identity, then the second part of this universal property is exactly the second part of Lemma \ref{Lem:ArrowObject}, applied to the horizontal 2-category of $\dblcat{D}$. It is in this sense that this universal property generalizes that for arrow objects in a 2-category.
% \end{remark}

\section{Monads}\label{Sec:DblCatMonads}

We will define a \emph{monad} in a double category $\dblcat{D}$ to be a tuple $(C,T,\eta,\mu)$, in which $C$ is an object, $T\colon C\to C$ is a horizontal 1-cell, and $\eta$ and $\mu$ are 2-cells
\[
\begin{tikzcd}
	C \rar[tick][domA]{\id_C} \dar[equal]
		& C \dar[equal] \\
	C \rar[tick][codA,swap]{T}
		& C
	\twocellA{\eta}
\end{tikzcd}
\qquad
\begin{tikzcd}
	C \rar[tick][]{T} \dar[equal]
		& |[alias=domA]| C \rar[tick][]{T}
		& C \dar[equal] \\
	C \ar[tick]{rr}[codA,swap]{T}
		&& C
	\twocellA{\mu}
\end{tikzcd}
\]
satisfying the usual unit and associativity conditions. In other words, a monad in $\dblcat{D}$ is simply a monad in the 2-category $\Hor(\dblcat{D})$. The non-identity vertical 1-cells come into play in the morphisms of monads.

Given two monads $(C,T,\eta,\mu)$ and $(D,S,\eta',\mu')$, a monad morphism from $(C,T)$ to $(D,S)$ consists of a pair $(f,\phi)$, where $f$ is a vertical 1-cell $C\to D$ and $\phi$ is a 2-cell
\[
\begin{tikzcd}
	C \rar[tick][domA]{T} \dar[][swap]{f}
		& C \dar{f} \\
	D \rar[tick][codA,swap]{S}
		& D
	\twocellA{\phi}
\end{tikzcd}
\]
which commutes with the unit and multiplication 2-cells in the sense of the two equations
\begin{equation}\label{Eq:MonoidMorphismUnit}
\begin{tikzcd}
	C \rar[tick][domA]{\id_C} \dar[equal]
		& C \dar[equal] \\
	C \rar[tick][codA,domB]{T} \dar[][swap]{f}
		& C \dar{f} \\
	D \rar[tick][codB,swap]{S}
		& D
	\twocellA{\eta}
	\twocellB{\phi}
\end{tikzcd}
=
\begin{tikzcd}
	C \rar[tick][domA]{\id_C} \dar[][swap]{f}
		& C \dar{f} \\
	D \rar[tick][codA,domB]{\id_D} \dar[equal]
		& D \dar[equal] \\
	D \rar[tick][swap,codB]{S}
		& D
	\twocellA{\id_f}
	\twocellB{\eta'}
\end{tikzcd}
\end{equation}
and
\begin{equation}\label{Eq:MonoidMorphismMult}
\begin{tikzcd}
	C \rar[tick][]{T} \dar[equal]
		& |[alias=domA]| C \rar[tick][]{T}
		& C \dar[equal] \\
	C \ar[tick]{rr}[codA,domB]{T} \dar[swap]{f}
		&& C \dar{f} \\
	D \ar[tick]{rr}[codB,swap]{S}
		&& D
	\twocellA{\mu}
	\twocellB{\phi} 
\end{tikzcd}
=
\begin{tikzcd}
	C \rar[tick][domA]{T} \dar[swap]{f}
		& C \rar[tick][domB]{T} \dar{f}
		& C \dar{f} \\
	D \rar[tick][codA]{S} \dar[equal]
		& |[alias=domC]| D \rar[tick][codB]{S}
		& D \dar[equal] \\
	D \ar[tick]{rr}[codC,swap]{S}
		&& D
	\twocellA{\phi}
	\twocellB{\phi}
	\twocellC{\mu'}
\end{tikzcd}
\end{equation}

\begin{definition}
	Given any double category $\dblcat{D}$, we will write $\Mon(\dblcat{D})$ for the category of monads in $\dblcat{D}$, consisting of monads and monad morphisms as defined above. The category $\Comon(\dblcat{D})$ of comonads in $\dblcat{D}$ is defined to be the category $\Mon(\dblcat{D}^{\text{op}})$ of monads in $\dblcat{D}^{\text{op}}$.
\end{definition}

\begin{example}
	The category $\Mon(\Span(\Cat{Set}))$ is precisely the category of small categories. It is an easy and enlightening exercise to work this out for oneself.
\end{example}

\begin{proposition}
	The categories of (co)monads and (co)lax morphisms in a 2-category $\twocat{D}$ can be given in terms of (co)monads in the double category of squares as follows:
	\begin{align*}
		\Mon_{\text{colax}}(\mathcal{D}) &= \Mon(\Sq(\mathcal{D})) \\
		\Comon_{\text{colax}}(\mathcal{D}) &= \Comon(\Sq(\mathcal{D})) \\
		\Mon_{\text{lax}}(\mathcal{D}) &= \Mon(\Sq(\mathcal{D}^{\text{op}}))^{\text{op}} \\
		\Comon_{\text{lax}}(\mathcal{D}) &= \Comon(\Sq(\mathcal{D}^{\text{op}}))^{\text{op}}
	\end{align*}
	where by $\twocat{D}^{\text{op}}$ we mean the 2-category obtained by reversing the direction of all 1-cells (but not 2-cells).
\end{proposition}
\begin{proof}
	Immediate from the definitions. Readers unfamiliar with (co)lax morphisms of monads can take this as the definition.
\end{proof}

\section{Double Functors}

The natural notion of functor between double categories is a straightforward generalization of lax functors between monoidal categories. Recall that we are using the symbol $\otimes$ to denote horizontal composition.

\begin{definition}\label{Def:LaxDblFunc}
	Let $\dblcat{D}$ and $\dblcat{E}$ be double categories. A \emph{lax double functor} $F\colon\dblcat{D}\to\dblcat{E}$ consists of:
	\begin{compactitem}
		\item Functors $F_0\colon\dblcat{D}_0 \to\dblcat{E}_0$ and $F_1\colon\dblcat{D}_1 \to\dblcat{E}_1$ such that $sF_1=F_0s$ and $tF_1=F_0t$
		\item Natural transformations with globular components $F_{\otimes}\colon F_1X\otimes F_1Y\to F_1(X\otimes Y)$ and $F_I\colon I_{F_0C}\to F_1(I_C)$, which satisfy the usual coherence axioms for a lax monoidal functor.
	\end{compactitem}
\end{definition}

A lax double functor $F$ for which the components of $F_I$ and $F_{\otimes}$ are identities will be called \emph{strict}. For the intermediate notion where the components of $F_I$ and $F_{\otimes}$ are (vertical) isomorphsims, we will simply refer to $F$ as a double functor.

\begin{proposition}\label{Prop:LaxFuncMonad}
	A lax double functor $F\colon\dblcat{D}\to\dblcat{E}$ induces a functor $F\colon\Mon(\dblcat{D})\to\Mon(\dblcat{E})$.
\end{proposition}
\begin{proof}
	This works just like the case for monoidal categories. For instance, if $X$ is a monad in $\dblcat{D}$, $FX$ has the multiplication
	\[
	\begin{tikzcd}
		C \rar[tick][]{FX} \dar[equal] 
			& |[alias=domA]| C \rar[tick][]{FX} 
			& C \dar[equal] \\
		C \ar[tick]{rr}[codA,domB]{F(X\otimes X)} \dar[equal] 
			&& C \dar[equal] \\
		C \ar[tick]{rr}[codB,swap]{FX} && C
		\twocellA{F_{\otimes}}
		\twocellB{F\mu}
	\end{tikzcd}
	\]
	The fact that $F$ takes monad morphisms to monad morphisms can easily be checked using the naturality of $F_I$ and $F_{\otimes}$.
\end{proof}

We will have need for a condition on a lax double functor which implies a sort of converse to~\cref{Prop:LaxFuncMonad}. This condition is a slight strengthening of the notion of fully-faithful functor which makes sense for lax functors.

\begin{definition}\label{Def:FullFaithfulLaxFunc}
	A lax double functor $F\colon\dblcat{D}\to\dblcat{E}$ is fully-faithful on 2-cells if, for any fixed $X_1,X_2,Y,f,g$, the induced function from 2-cells in $\dblcat{D}$ of the shape
	\[
	\begin{tikzcd}
		C_0 \dar[swap]{f} \rar[tick]{X_1} & C_1 \rar[tick]{X_2} & C_2 \dar{g} \\
		D_0 \ar[tick]{rr}[swap]{Y} && D_1
	\end{tikzcd}
	\]
	to 2-cells in $\dblcat{E}$ of the shape
	\[
	\begin{tikzcd}
		FC_0 \dar[swap]{Ff} \rar[tick]{FX_1} & FC_1 \rar[tick]{FX_2} & FC_2 \dar{Fg} \\
		FD_0 \ar[tick]{rr}[swap]{FY} && FD_1,
	\end{tikzcd}
	\]
	which takes a 2-cell $\theta$ to $F(\theta)\circ F_{\otimes}$, is a bijection, and if similarly the induced function from 2-cells of the shape
	\[
	\begin{tikzcd}
		C \rar[tick]{I_{C}} \dar[swap]{f} & C \dar{g} \\
		D_0 \rar[tick][swap]{Y} & D_1
	\end{tikzcd}
	\qquad\text{to}\qquad
	\begin{tikzcd}
		FC \rar[tick]{I_{FC}} \dar[swap]{Ff} & FC \dar{Fg} \\
		FD_0 \rar[tick][swap]{FY} & FD_1
	\end{tikzcd}
	\]
	taking a 2-cell $\phi$ to $F(\phi)\circ F_I$ is a bijection.
\end{definition}
\begin{remark}
	\Cref{Def:FullFaithfulLaxFunc} implies the function on 2-cells $\theta$ with a single horizontal 1-cell in the domain is also bijective. We leave the details of the (simple) proof to the reader.
\end{remark}
\begin{proposition}\label{Prop:FullFaithfulMonads}
	Let $F\colon\dblcat{D}\to\dblcat{E}$ be a fully-faithful lax double functor. Given any horizontal 1-cell $X$ in $\dblcat{D}$, a monoid structure on $FX$ in $\dblcat{E}$ lifts uniquely to a monoid structure on $X$ such that the induced functor $F\colon\Mon(\dblcat{D})\to\Mon(\dblcat{E})$ takes $X$ to $FX$.

	Similarly, a vertical 1-cell $f\colon X\to Y$ for which $Ff$ is a monoid morphism must also be a monoid morphism.

	In other words, the diagram of categories is a pullback:
	\[
	\begin{tikzcd}
		\Mon(\dblcat{D}) \rar{F} \dar[swap]{U} & \Mon(\dblcat{E}) \dar{U} \\
		\dblcat{D} \rar[swap]{F} & \dblcat{E}.
	\end{tikzcd}
	\]
\end{proposition}
\begin{proof}
	Simply use the surjectivity of the fully-faithful functor to lift the unit and multiplication 2-cells from $FX$ to $X$, then use the injectivity to show that the unitary and associativity equations on $FX$ imply those on $X$.
\end{proof}