~ohad-kammar/ohads-thesis/trunk

\Section{Enriched Lawvere theories}\sectionlabel{lawvere theories}

We recall the relevant notions regarding \defterm{enriched Lawvere
  theories}. Our account follows most closely Power's
account~\cite{power:enriched-lawvere-theories}. A key difference is
that we keep to a
symmetric closed enrichment, rather than the more general biclosed
structure Power considers. The symmetric account dates further back to
Kelly~\cite{kelly:structure-defined-by-finite-limits-in-the-enriched-contexts-i}.

First, we assume the enriching category has the following structure
(see Power's account~\cite[Section~2]{power:enriched-lawvere-theories}).

\begin{definition}
  Let $\regcard$ be a regular cardinal. A \defterm{$\regcard$-Power
    category $\SymMonCat$} is a symmetric monoidal closed category $\seq{\symmoncatcarrier\SymMonCat, \oI, \ox, \oto, \leftunitor,
  \rightunitor, \associator, \symmetry}$ such that:
  \begin{itemize}
  \item $\symmoncatcarrier\SymMonCat$ is locally
    $\regcard$-presentable; and
  \item $\oI$ is $\regcard$-presentable, and if $\symV$, $\symVv$ are
    $\regcard$-presentable, then so is $\symV\ox\symVv$.
  \end{itemize}
\end{definition}

We call an $\aleph_0$-Power category a \defterm{finitary} Power category, and
similarly we call an $\aleph_1$-Power category a \defterm{countably infinitary} Power
category, or simply a countable Power category (although it is
may \emph{not} be a countable category, i.e., have countably many morphisms). We restrict our attention to the following two cases:

\begin{example}
  The category $\Set$ with the cartesian closed structure is a finite
  Power category. Indeed, in \exampleref{set is lfp} we saw that
  $\Set$ is locally finitely presentable. As ${\oI = \set\unitval}$ is finite, and the
  product of finite sets is finite as well, $\Set$ is a finite Power category.
\end{example}

\begin{example}
  The category $\wCPO$ with the cartesian closed structure is a
  countable Power category. Indeed, \theoremref{wcpo is lcp} shows
  that $\wCPO$ is locally countably presentable. As ${\oI =
  \set\unitval}$ is finite, it is countably presentable by \exampleref{finite domains are
      cp}. Let $\mWv$, $\mW$ be two \wcpo{}s with countable domain
  presentations $\dompres_{\mWv} = \triple{\mBasev}\mconsdom{\mcons_{\mWv}}$,
  $\dompres_{\mW} = \triple{\mBase}\mconsdomv{\mcons_{\mW}}$, respectively. Define:
  \begin{mapdef*}
    \mBasew &\definedby& \mBasev\times\mBase \\
    \mconsdomw &\definedby &
    \set{
      \seq[n]{\pair{\mbasev_n}\mbase} \suchthat \seq{\mbasev_n} \in
      \mconsdom, \mbase \in \mBase
    }
    \union
    \set{
      \seq[n]{\pair\mbasev{\mbase_n}} \suchthat \mbasev \in \mBasev, \seq{\mbase_n} \in
      \mconsdomv
    }
    \\
    \mcons_{\mWw} &\definedby&
    \set{
      \seq{\pair{\mbasev_n}\mbase}\mcons\seq{\pair{\mbasev'_n}\mbase}
      \suchthat
      \seq{\mbasev_n} \mcons_{\mWv} \seq{\mbasev'_n},
      \mbase \in \mBase
    }
    \union\\
    &&\set{
      \seq{\pair\mbasev{\mbase_n}}\mcons\seq{\pair\mbasev{\mbase'_n}}
      \suchthat
      \mbasev \in \mBasev,
      \seq{\mbase_n} \mcons_{\mW} \seq{\mbase'_n}
    }
  \end{mapdef*}%
  then $\dompres_{\mWw} = \triple\mBasew\mconsdomw{\mcons_{\mWw}}$
  is a countable domain presentation, and $\mWw \definedby \mWv\times \mW$ is the
  initial $\dompres_{\mWw}$-model. Indeed, setting
  $\domalgebra[\mWw][\pair{\mbasev}\mbase]\definedby
  \pair{\domalgebra[\mWv][\mbasev]}{\domalgebra[\mW][\mbase]}$
  exhibits $\mWw$ as a $\dompres_{\mWw}$-model. For initiality, take
  any other model $\mWw'$. For each $\mbasev \in \mBasev$, due to the
  presence of
  constraints of the form $\seq{\pair\mbasev{\mbase_n}}\mcons\seq{\pair\mbasev{\mbase'_n}}$, the
  function $\mmorphv_{\mbasev} \definedby \ilam\mbase{\domalgebra[\mWw'][\pair\mbasev\mbase]}$
  exhibits a $\dompres_{\mW}$-model $\pair{\mWw'}{\mmorphv_{\mbasev}}$, hence we have a unique
  Scott-continuous $\mmorph_{\mbasev}\of \mW\to\mWw'$ factoring $\domalgebra[\mW]$
  through $\mmorphv_{\mbasev}$. Due to constraints of the form
  $\seq{\pair{\mbasev_n}\mbase}\mcons\seq{\pair{\mbasev'_n}\mbase}$,
  the map $\mmorphv' \definedby \ilam\mbasev{\mmorph_{\mbasev}}$ from
  $\mBasev$ to $\mWw'$ is monotone, hence we have a unique
  Scott-continuous $\mmorphw' \of \mWv \to (\mWw')^{\mWv}$ factoring
  $\domalgebra[\mWv]$ through $\mmorphv'$. Uncurrying then yields the
  unique $\mmorphw \of \mWv\times\mW \xto{\ilam\mWv\mmorphw'} \mWw'$
  factoring $\domalgebra[\mWw]$ through $\domalgebra[\mWw']$. Thus
  $\mWv\times\mW$ has a countable presentation, and $\wCPO$ is a
  countable Power category.
\end{example}

When a category has all (co)powers of objects by
$\regcard$-presentable objects, we say it has all
$\regcard$-(co)powers. Denote by $\Pres\SymMonCat$ the full subcategory of $\SymMonCat$ consisting of
the $\regcard$-presentable objects. When $\SymMonCat$ is a
$\regcard$-Power category, $\Pres\SymMonCat$ contains $\oI$ and
$\symV\ox\symVv$ for every $\regcard$-presentable $\symV$ and
$\symVv$. Thus, $\Pres\SymMonCat$ has all $\regcard$-copowers, hence
the opposite $\SymMonCat$-category $\PresOp\SymMonCat$ has all $\regcard$-powers. Note
that, in light of \propositionref{representative set of lp objects},
$\Pres\SymMonCat$ is essentially small, i.e., it is
$\SymMonCat$-equivalent to a small category.
%
Note that Power~\cite{power:enriched-lawvere-theories} prefers to work with
small categories, hence instead uses the skeleton of our
$\Pres\SymMonCat$.  As we will see later, it will be useful to
have all $\regcard$-presentable objects rather than a set of
representatives, although it will complicate some proofs.

We say that a $\SymMonCat$-functor $\Functor \of
\richCatv \to \richCat$ is \defterm{identity-on-objects} if
$\Obj\richCatv = \Obj\richCat$ and $\Functor \enAv = \enAv$ for all
$\richCatv$-objects $\enAv$. For example, the $\SymMonCat$-functor $\F$ from $\SymMonCat$
to the Kleisli $\SymMonCat$-category $\KleisliCat\SymMonCat\Monad$ that we
study in \exampleref{enriched kleisli category} is identity-on-objects.

\begin{definition}
  Let $\SymMonCat$ be a $\regcard$-Power category. An
  \defterm{enriched $\regcard$-Lawvere $\SymMonCat$-theory $\mL$}
  is a pair $\pair{\LawCat\mL}{\LawFunctor\mL\placeholder}$
  where:
  \begin{itemize}
    \item $\LawCat\mL$ is a $\SymMonCat$ category with
      $\regcard$-powers; and
    \item $\LawFunctor\mL\placeholder \of\PresOp\SymMonCat \to
      \LawCat\mL$ is a $\SymMonCat$-functor that is $\regcard$-power
      preserving and identity-on-objects.
  \end{itemize}
\end{definition}

\begin{example}[{see
      Power~\cite[Construction~3.3]{power:enriched-lawvere-theories}}]\examplelabel{monad->theory
  construction}
Let $\Monad$ be a monad enriched in a $\regcard$-Power category
$\SymMonCat$, and $\F$ the $\SymMonCat$-functor from $\SymMonCat$
to the Kleisli $\SymMonCat$-category $\KleisliCat\SymMonCat\Monad$ we
studied in \exampleref{enriched kleisli category}. Denote by $\PresKleisliCat\SymMonCat\Monad$ the
$\SymMonCat$-category induced by the $\regcard$-presentable objects in
$\SymMonCat$. Then $\F$ restricts to an identity-on-objects
$\regcard$-copower preserving $\SymMonCat$-functor $\F^{\regcard} \of
\Pres\SymMonCat \to \PresKleisliCat\SymMonCat\Monad$. By moving to the
opposite categories, we obtain an identity-on-objects $\regcard$-power
preserving $\SymMonCat$-functor from $\PresOp\SymMonCat$ to
$\opposite{\parent{\PresKleisliCat\SymMonCat\Monad}}$, and consequently a
$\regcard$-Lawvere $\SymMonCat$-theory which we denote by
$\MonadTheory\Monad$.

Explicitly, $\MonadTheory\Monad$ is given as follows. The objects of
$\LawCat{\MonadTheory\Monad}$, as in any $\regcard$-Lawvere
$\SymMonCat$-theory, are the $\regcard$-presentable objects of
$\SymMonCat$. The hom-objects
$\homset[\LawCat{\MonadTheory\Monad}]\symV\symVv$ are given by
$\homset[\SymMonCat]\symVv{\Monad\symV}$. Identities are given by the
monadic unit $\unit$, and the composition by:
\[
\scriptstyle
\enComp[\enA,\enAv,\enAw] \of
\homset[\SymMonCat]\enAw{\Monad\enAv}\ox\homset[\SymMonCat]\enAv{\Monad\enA}
\xto{\id\ox\Monad}
\homset[\SymMonCat]{\enAw}{\Monad\enAv}\ox\homset[\SymMonCat]{\Monad\enAv}{\Monad^2\enA}
\xto{\enComp^{\SymMonCat}\compose\symmetry}
\homset[\SymMonCat]\enAw{\Monad^2\enA}
\xto{\homset[\SymMonCat]{\enA}{\enMonadMult}}
\homset[\SymMonCat]\enAw{\Monad\enA}
\]
The powers $\power\symV\symVw$ are given as $\SymMonCat$ copowers,
i.e., the tensor product $\symV\ox\symVw$.

Finally, the object map of the $\SymMonCat$-functor
$\LawFunctor{\MonadTheory\Monad}\placeholder$ is the identity map, and
its action on hom-objects is given by post-composing with the unit $\unit$:
\[
\LawFunctor{\MonadTheory\Monad}\placeholder \of
\homset[\PresOp\SymMonCat]\symV\symVv
=
\homset[\SymMonCat]\symVv\symV
\xto{\homset[\SymMonCat]\symVv{\unit_{\symV}}}
\homset[\SymMonCat]\symVv{\Monad\symV}
=
\homset[\LawCat{\MonadTheory\Monad}]\symV\symVv
\]
Thus, we have a $\regcard$-Lawvere $\SymMonCat$-theory.
\end{example}

In the sequel, we will present more syntactic and concrete ways to define
Lawvere theories.

\begin{definition}
  Let $\mL$ be a $\regcard$-Lawvere $\SymMonCat$-Theory and $\richCat$ a
  $\SymMonCat$-category with $\regcard$-powers. An
  \defterm{$\mL$-model $\mModel$ in $\richCat$} is a $\SymMonCat$-functor $\mModel \of
  \LawCat\mL \to \richCat$ preserving all $\regcard$-powers.

  \noindent
  Given two models $\mModel$, $\mModel'$, an \defterm{$\mL$-homomorphism $\mhomo$} is a
  $\SymMonCat$-natural transformation from $\mModel$ to $\mModel'$.

  \noindent
  We denote by $\ModCat\mL\richCat$ the full subcategory of the
  (ordinary) category of $\SymMonCat$-functors from $\LawCat\mL$ to
  $\richCat$ and $\SymMonCat$-natural transformations between them
  consisting of the $\mL$-models.
\end{definition}

Let $\mModel$ be an $\mL$-model. Note that for any $\regcard$-presentable $\symV$:
\[
\mModel(\symV)
\explain={identity-on-objects}
\mModel(\LawFunctor\mL\symV)
\isomorphic
\mModel(\LawFunctor\mL{\symV\ox\oI})
\explain\isomorphic{power preservation}
\mModel(\power\symV{\LawFunctor\mL\oI})
\explain*={identity-on-objects}
\mModel(\power\symV\oI)
\explain\isomorphic{power preservation}
\power\symV{\mModel(\oI)}
\]
Therefore, the object map of $\mModel$ is uniquely determined by its action on
$\oI$. We call the object $\mModel(\oI)$ the \defterm{carrier of
  $\mModel$}. In fact, we have the following  functor:
\begin{mapdef*}
\LawU\mL &\of \ModCat\mL\richCat &\to \ordinary\richCat
\\
\LawU\mL &\of \mModel &\mapsto \mModel(\oI)
\\
\LawU\mL &\of (\mModel\xto{\mhomo}\mModel') &\mapsto (\oI \xto{\mhomo_{\oI}} \homset[\richCat]{\mModel(\oI)}{\mModel'(\oI)})
\end{mapdef*}
Note how we regarded $\ModCat\mL\richCat$ as an ordinary
category. In fact, $\ModCat\mL\richCat$ is a $\SymMonCat$-category~\cite[Definition~3.2]{power:enriched-lawvere-theories}.
To explicitly describe this structure, we need to introduce
enriched functor categories, which requires us to review additional
notions from enriched category theory.
As we will not explicitly use this enriched structure in what follows, we treat
$\ModCat\mL\richCat$ merely as an ordinary category.

Power~\cite{power:enriched-lawvere-theories} generalised the usual
bijection between finitary monads and Lawvere theories to the enriched
case in the following manner:
\begin{theorem}[{\cite[Construction~3.3 and
        Theorems~3.4,4.1]{power:enriched-lawvere-theories}}]\theoremlabel{theory->monad
  construction}
  Let $\SymMonCat$ be a $\regcard$-Power category. For every
  $\regcard$-Lawvere $\SymMonCat$-theory $\mL$, the functor $\LawU\mL \of
  \ModCat\mL\SymMonCat \to \SymMonCat$ is \defterm{monadic}, i.e.,
  $\LawU\mL$ has a left adjoint $\LawF\mL \of \SymMonCat \to
  \ModCat\mL\SymMonCat$, and the Eilenberg-Moore category for the resulting monad $\LawMonad\mL =
  \LawU\mL\LawF\mL$ over $\SymMonCat$ is equivalent to
  $\ModCat\mL\SymMonCat$. Furthermore, $\LawMonad\mL$ is
  $\SymMonCat$-enriched and $\regcard$-ranked.
  We call $\LawF\mL$ the \defterm{free model functor} for $\mL$, and
  $\LawMonad\mL$ the \defterm{free model monad} for $\mL$.
\end{theorem}

Using \theoremref{em
  is lp}, we deduce the following:
\begin{theorem}[\cite{hyland-plotkin-power:sum-and-tensor}]
  For every $\regcard$-Lawvere $\SymMonCat$-theory $\mL$, the category
  of $\mL$-models $\ModCat\mL\SymMonCat$ is locally $\regcard$-presentable.
\end{theorem}
Plotkin and Power, in unpublished work, use this theorem to show
indirectly that $\wCPO$ is locally countably presentable by exhibiting
it as a category of $\mL$-models for a suitable countable Lawvere
$\Pos$-enriched theory.

Next, we follow Power~\cite{power:enriched-lawvere-theories} and construct a category of enriched Lawvere theories:
\begin{definition}
  Let $\mL$, $\mL'$ be two $\regcard$-Lawvere $\SymMonCat$-theories. A
  \defterm{morphism $\LawHomo$ from $\mL$ to $\mL'$} is a $\SymMonCat$
  functor $\LawHomo \of \LawCat \mL \to \LawCat {\mL'}$ that is
  identity-on-objects, $\regcard$-power preserving, and satisfies
  \inlinediagram{lawvere-morphism-01}
  %
  Taking $\regcard$-Lawvere $\SymMonCat$-theories as objects and
  their morphisms with the usual functor composition and identities
  yields an ordinary category $\Lawvere\SymMonCat$.
\end{definition}

\begin{example}
  Let $\MonadMorphism \of \Monad \to \Monad'$ be a $\SymMonCat$-monad
  morphism over a $\regcard$-Power category $\SymMonCat$. We saw in
  \exampleref{enriched kleisli category} that $\MonadMorphism$ induces
  an identity-on-objects, copower preserving $\SymMonCat$-functor $M
  \of \KleisliCat\SymMonCat\Monad \to \KleisliCat\SymMonCat{\Monad'}$.
  Therefore, by restricting to the $\regcard$-presentable objects and
  taking the opposite categories, this $\SymMonCat$-functor restricts
  to a morphism of $\regcard$-Lawvere $\SymMonCat$-theories
  $\MonadTheory{\MonadMorphism}$ from the theory
  $\MonadTheory{\Monad}$ to the theory $\MonadTheory{\Monad'}$,
  presented in \exampleref{monad->theory construction}.

  Denote by  $\EnrichedMonad\SymMonCat$ the (ordinary) category of
  $\SymMonCat$-monads and $\SymMonCat$-monad morphisms. Then the construction $\MonadTheory\placeholder$ is an ordinary functor
  from the category $\EnrichedMonad\SymMonCat$
  to the category $\Lawvere\SymMonCat$.
\end{example}

Denote by $\EnrichedRankedMonad\SymMonCat$ the full subcategory of
$\EnrichedMonad\SymMonCat$ consisting of the $\regcard$-ranked
monads. The functor $\MonadTheory\placeholder$ restricts to a functor
from $\EnrichedRankedMonad\SymMonCat$ to $\Lawvere\SymMonCat$.

\begin{theorem}[{\cite[Theorem~4.3]{power:enriched-lawvere-theories}}]\theoremlabel{theory
  <-> ranked monad}
    Let $\SymMonCat$ be a $\regcard$-Power category. The functor
    $\MonadTheory\placeholder \of \EnrichedRankedMonad\SymMonCat \to
    \Lawvere\SymMonCat$ is an equivalence of categories. Its \defterm{adjoint weak inverse} from $\Lawvere\SymMonCat$ to
    $\EnrichedRankedMonad\SymMonCat$ maps every $\regcard$-Lawvere
    $\SymMonCat$-theory $\mL$ to the monad $\LawMonad\mL$ from
    \theoremref{theory->monad construction}.
    In particular:
    \begin{itemize}
    \item for every $\regcard$-Lawvere $\SymMonCat$-theory $\mL$, we
      have $\MonadTheory{\LawMonad\mL} \isomorphic \mL$; and
    \item for every $\regcard$-ranked $\SymMonCat$-monad $\Monad$ over
      $\SymMonCat$, we have $\LawMonad{\MonadTheory{\Monad}}
      \isomorphic \Monad$.
    \end{itemize}
\end{theorem}
In the following we occasionally need the explicit description of
$\LawMonad\placeholder$ on a theory $\mL$. Therefore, we recount a
known technique to reconstruct, up to isomorphism, the functor
$\LawMonad\placeholder$ from the definition of
$\MonadTheory\placeholder$, using the previous theorem. Denote by
${\counit \of \MonadTheory{\LawMonad\placeholder} \to \id}$ the counit
of the equivalence.


  Given a $\SymMonCat$-category $\richCat$ and
  arrows
  \begin{mapdef*}
  \richConcept\mmorph &\of \oI&\oto\homset[\richCat]\enA\enAv
  \\
  \richConcept\mmorphv&\of\oI&\oto\homset[\richCat]\enAw\enAx
  \end{mapdef*}
  define the composition
  arrow~(cf. Kelly~\cite[Section~1.6]{kelly:basic-concepts-of-enriched-category-theory})
  as follows:
  \begin{align*}
    \homset[\richCat]{\richConcept\mmorph}{\richConcept\mmorphv} \of
    \homset[\richCat]\enAv\enAw \xto{\isomorphic}
    \oI\ox\homset[\richCat]\enAv\enAw\ox\oI
    \xto{\mmorphv\ox\id\ox\mmorph}&
    \homset[\richCat]\enAv\enAw\ox\homset[\richCat]\enAv\enAw\ox\homset[\richCat]\enA\enAv
\\    \xto{\id\ox\enComp}&
    \homset[\richCat]\enAv\enAw\ox\homset[\richCat]\enA\enAw
    \xto\enComp
    \homset[\richCat]\enA\enAx
  \end{align*}
  For a Lawvere theory $\mL$, and any arrow $\mmorph \of \mV \from \mVv$
  in $\Pres\SymMonCat$, we define the arrow:
  \[
  \LawFunctor\mL\mmorph \of \oI \xto{\richConcept\mmorph}
  \homset[\PresOp\SymMonCat]\mV\mVv \xto{\LawFunctor\mL\placeholder}\homset[\LawCat\mL]\mV\mVv
  \]
  Straightforward calculations verify the following identities:
  \begin{subequations}
    \begin{align}\label{id preservation identity}
      \LawFunctor\mL{\id[\mV]} &
      = \enId[\mV]^{\LawCat\mL}
      \\\label{enriched composition identity}
      \homset[\LawCat\mL]{\LawFunctor\mL\mmorph}{\LawFunctor\mL\mmorphw}\compose \LawFunctor\mL{\mmorphv}
      &=
      \LawFunctor\mL{\mmorph\compose\mmorphv\compose\mmorphw}
    \end{align}

      \numbereddiagram[\diagramlabel{enriched composition naturality}]{lawvere-theory-factorisation-theorem-31}
      \numbereddiagram[\diagramlabel{enriched composition op-naturality}]{lawvere-theory-factorisation-theorem-34}
      \numbereddiagram[\diagramlabel{enriched functor composition identity}]{lawvere-theory-factorisation-theorem-35}
  \end{subequations}



Let $\mL$ be any Lawvere theory.

First, we recover the action of $\LawMonad\mL$ on objects. Consider
any $\SymMonCat$-object $\mV$, and a $\regcard$-directed diagram
$\mDiag \of \mdirpos \to \SymMonCat$, whose vertices are
$\regcard$-presentable, for which $\mV = \Colim\mDiag$.  We would like
to calculate as follows:
\begin{align*}
\LawMonad\mL\mV &\explain={$\regcard$-ranked monad}
\Colim\LawMonad\mL\compose \mDiag \isomorphic \Colim (\oI \oto
\LawMonad\mL\mDiag(\placeholder)) =
\Colim\homset[\Pres\SymMonCat]{\oI}{\LawMonad\mL\mDiag(\placeholder})
\\&=
\Colim\homset[\LawCat{\MonadTheory{\LawMonad\mL}}]{\mDiag(\placeholder)}\oI
\explain\isomorphic{\theoremref{theory <-> ranked monad}}
\Colim\homset[\LawCat\mL]{\mDiag(\placeholder)}\oI
\end{align*}
However, we need to take some care with the last two transitions, and clarify
what we mean by $\homset[\LawCat\mL]{\mDiag(\placeholder)}\oI$ when
the diagram is applied to morphisms in $\mdirpos$.

Let $\mL$ be any Lawvere theory. We define an ordinary functor
\[
\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI \of \Pres\SymMonCat \to
\SymMonCat
\] The object map maps every
$\regcard$-presentable object $\mV$ to
$\homset[\LawCat\mL]\mV\oI$. Given any morphism
${\mmorph \of \mV \to \mV'}$ between $\regcard$-presentable objects,
we have a $\SymMonCat$-morphism
$\LawFunctor\mL{\mmorph} \of \oI \to \homset[\LawCat\mL]{\mV'}\mV$.
Thus, we define the morphism map by the enriched
precomposition
with $\LawFunctor\mL{\mmorph}$:
\[
\homset[\LawCat\mL]{\LawFunctor\mL\mmorph}\oI \of
\homset[\LawCat\mL]\mV\oI \xto{}
\homset[\LawCat\mL]{\mV'}\oI
\]
In light of \eqref{id preservation identity} and \eqref{enriched
  composition identity},
$\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI$ is a functor.
For any $\regcard$-presentable object $\mV$, define an isomorphism $\NaturalTransformation_{\mV} \of
\LawMonad\mL\mV \xto{\isomorphic} \homset[\LawCat\mL]{\mV}{\oI}$
by:
\[
\NaturalTransformation_{\mV} \of
\LawMonad\mL\mV
\isomorphic \oI \oto
\LawMonad\mL\mV =
\homset[\Pres\SymMonCat]{\oI}{\LawMonad\mL\mV}
=
\homset[\LawCat{\MonadTheory{\LawMonad\mL}}]{\mV}\oI
\overset\counit\isomorphic
\homset[\LawCat\mL]{\mV}\oI
\]
Because $\counit$ is a morphism of Lawvere theories, it follows by
\diagramref{enriched functor composition identity} that $\counit$ is
natural in $\mV$. Consequently, $\NaturalTransformation$ is a natural
isomorphism between the restriction of $\LawMonad\mL$ to the
$\regcard$-presentable objects, i.e., as a functor
from $\Pres\SymMonCat$ to $\SymMonCat$, and
the functor $\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI$.

Consider any diagram $\mDiag \of \mdirpos \to \SymMonCat$, whose vertices are
$\regcard$-presentable, for which $\mV = \Colim\mDiag$. Let
$\mDiag_{\mL} \of \mdirpos \to \SymMonCat$ be the
diagram
$\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI\compose\mDiag$. Then
precomposing $\NaturalTransformation$ with $\mDiag$ yields an
isomorphism $\NaturalTransformation \of \LawMonad\mL \compose \mDiag
\xto\isomorphic \mDiag_{\mL}$.
Thus we have:
\[
\LawMonad\mL\mV = \LawMonad\mL\Colim\mDiag = \Colim\LawMonad\mL\mDiag
\isomorphic \Colim\mDiag_{\mL}
\]

Similarly, to recover the action of $\LawMonad\mL$ on morphisms, we
use \propositionref{ranked functor extension}. Consider any
$\regcard$-directed diagram $\mDiag \of \mdirpos \to
\SymMonCat^{\ArrowCat}$ whose vertices are all
$\regcard$-presentable. The
naturality of $\NaturalTransformation$ yields a natural isomorphism
$\NaturalTransformation^{\ArrowCat} \of \Monad^{\ArrowCat} \to
\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI^{\ArrowCat}$. Define
$\mDiag_{\mL}$ as the composition
$\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI^{\ArrowCat}\compose\mDiag$. We
then have:
\[
\LawMonad\mL\mmorph
\explain\isomorphic{\propositionref{ranked functor extension}}
\Colim\LawMonad\mL^{\ArrowCat}\compose\mDiag
\isomorphic
\Colim\mDiag_{\mL}^{\ArrowCat}
\]
Thus we recover the object map of $\MonadTheory\placeholder$. Let  $\LawHomo \of \mL \to \mLv$ be a morphism of Lawvere
theories.

Consider any $\SymMonCat$-object $\mV$, and a
$\regcard$-directed diagram $\mDiag \of \mdirpos \to \SymMonCat$,
whose vertices are $\regcard$-presentable, for
which ${\mV = \Colim\mDiag}$. We will invoke \propositionref{ranked
  natural transformation extension} on $\LawMonad\LawHomo$. Thus we
construct $\mDiag_{\LawMonad\LawHomo}$ as in \propositionref{ranked
  natural transformation extension}:
  \begin{align*}
    \mDiag_{\LawMonad\LawHomo}\mi &\of \LawMonad\mL\mDiag\mi
    \xto{(\LawMonad\LawHomo)_{\mDiag\mi}} \LawMonad\mLv\mDiag\mi
    & \mi \inObj \mdirpos
    \\
    \mDiag_{\LawMonad\LawHomo}\mmorph &=
    %
    \pair{\LawMonad\mL\mDiag\mi\xto{\LawMonad\mL\mDiag\mmorph}\LawMonad\mL\mDiag\mj}
         {\LawMonad\mLv\mDiag\mi\xto{\LawMonad\mLv\mDiag\mmorph}\LawMonad\mLv\mDiag\mj}
    %
         & \mmorph \of \mi \to \mj \text{ in $\mdirpos$}
  \end{align*}
The components of
$\LawHomo$ form a natural transformation $\LawHomo_{\mV,\oI} \of
\homset[\LawCat\mL]{\mV}\oI \to
\homset[\LawCat\mLv]{\mV}{\oI}$. Thus we construct the diagram
$\mDiag_{\LawHomo}$ as in \propositionref{ranked natural
  transformation extension}. I.e., for $\mi \inObj \mdirpos$,
  \begin{equation}\label{translation <-> monad morphism diagram construction}
    \mDiag_{\LawHomo}\mi \of \homset[\LawCat\mL]{\mDiag\mi}\oI
    \xto{\LawHomo} \homset[\LawCat\mLv]{\mDiag\mi}\oI
  \end{equation}
  and for $\mmorph \of \mi \to \mj$ in $\mdirpos$:
  \[
  \mDiag_{\LawHomo}\mmorph =
  \pair{\homset[\LawCat\mL ]{\mDiag\mi}\oI\xto{\homset[\LawCat\mL ]{\LawFunctor\mL {\mDiag\mmorph}}\oI}\homset[\LawCat\mL ]{\mDiag\mj}\oI}
       {\homset[\LawCat\mLv]{\mDiag\mi}\oI\xto{\homset[\LawCat\mLv]{\LawFunctor\mLv{\mDiag\mmorph}}\oI}\homset[\LawCat\mLv]{\mDiag\mj}\oI}
  \]
The two isomorphisms
$\NaturalTransformation_{\mL} \of \LawMonad\mL \xto{\isomorphic}
\homset[\LawCat\mL]{\LawFunctor\mL\placeholder}\oI$ and $\NaturalTransformation_{\mLv} \of
\LawMonad\mLv \xto{\isomorphic} \homset[\LawCat\mLv]{\LawFunctor\mLv\placeholder}\oI$ then
induce an isomorphism $\hat\NaturalTransformation$ from $\mDiag_{\LawMonad\LawHomo}$
to $\mDiag_{\LawHomo}$. Therefore:
\[
(\LawMonad{\LawHomo})_{\mV}
\explain\isomorphic{\propositionref{ranked natural transformation extension}}
\Colim\mDiag_{\LawMonad\LawHomo}
\isomorphic
\Colim\mDiag_{\LawHomo}
\]
Thus we reconstructed the functor $\LawMonad\placeholder$.

The category $\Lawvere\SymMonCat$ is locally presentable\footnote{John
Power, private communication, 2012.}, but the
proof lies beyond the scope of this thesis. From its local
presentability we deduce the following.
\begin{theorem}[{for a special case, see Hyland et. al~\cite[Theorem~6]{hyland-plotkin-power:sum-and-tensor}}]
  The category $\Lawvere\SymMonCat$ is cocomplete.
\end{theorem}

Therefore, we also know that $\Lawvere\SymMonCat$ is complete. However, in the
sequel we will make use of the fact that the limits in $\Lawvere\SymMonCat$
are given \emph{componentwise:}
\begin{theorem}\theoremlabel{lawvere theory limits}
  Let $\mDiag \of\DiagramIndex \to \Lawvere\SymMonCat$ be a small
  diagram. Every limiting cone $\pair\mL\Functor$ is uniquely
  determined by a collection of component limiting cones
  $\pair{\homset[\LawCat\mL]\enA\enAv}{\Functor_{\enA,\enAv}}$ for
  the
  component diagrams $\homset[\LawCat{\mDiag(\placeholder)}]\enA\enAv$.

  \noindent
  The remainder of the Lawvere theory structure is given as the unique maps
  satisfying, for all $\enA$, $\enAv$:
  \begin{center}
    \inlinediagram*{lawvere-theory-completeness-proof-02}
  \end{center}
  \inlinediagram{lawvere-theory-completeness-proof-08}
  \inlinediagram{lawvere-theory-completeness-proof-04}
\end{theorem}

\begin{proof}%
  First, assume a choice of limiting cones
  $\pair{\homset[\LawCat\mL]\enA\enAv}{\Functor_{\enA,\enAv}}$ for
    the
  component diagrams
  $\homset[\LawCat{\mDiag(\placeholder)}]\enA\enAv$.
  Straightforward calculation shows that we indeed have, for every
  $\enA$, $\enAv$, cones for each of the diagrams above. For example,
  for every $\mmorph \of \mi \to \mj$, we have
  \inlinediagram{lawvere-theory-completeness-proof-41}
  Thus $\powertupleWithCat{\LawCat\mL}\placeholder$ is uniquely
  defined. Using the fact that
  $\powertupleWithCat{\LawCat{\mDiag\mi}}\placeholder$ are
  isomorphisms,  $\invpowertupleWithCat{\LawCat\mL}\placeholder$ is
  uniquely defined. Similar arguments establish the unique existence
  of the other structure maps.

  \lemmaref{lawvere theory construction} completes the
  construction. From \lemmaref{lawvere theory
    construction}(\ref{lawvere theory construction: categories}) we
  have, for all $\mi$:
  \inlinediagram{lawvere-theory-completeness-proof-03}
  Therefore, as
  $\pair{\homset[\LawCat\mL]\enA\enAv}{\Functor_{\enA,\enAv}}$ is a
  limiting cone, we deduce that:
  \inlinediagram{lawvere-theory-completeness-proof-31}
  Thus $\LawCat\mL$ is a $\SymMonCat$-category, and $\Functor^{\mi}$
  become $\SymMonCat$-functors from $\LawCat\mL$ to
  $\LawCat{\mDiag\mi}$.

  Therefore, we can invoke \lemmaref{lawvere theory
    construction}(\ref{lawvere theory construction: powers}).
  From
  \inlinediagram{lawvere-theory-completeness-proof-05}
  we deduce that $\powertupleWithCat{\LawCat\mL}\placeholder$ is an isomorphism. From
  \inlinediagram{lawvere-theory-completeness-proof-06}
  we deduce, by appeal to universality, that
  $\powertupleWithCat{\LawCat\mL}\placeholder$ is $\SymMonCat$-natural, hence
  $\LawCat\mL$ has the power $\power\symV\enAv$. From
  \inlinediagram{lawvere-theory-completeness-proof-07}
  we deduce that $\Functor^{\mi}$ preserves this power.

  We now invoke  \lemmaref{lawvere theory
    construction}(\ref{lawvere theory construction: functors}) for
  $\Functorw \definedby \LawFunctor\mL\placeholder$, and  deduce that:
  \inlinediagram{lawvere-theory-completeness-proof-09}
  Thus $\LawFunctor\mL\placeholder$ is a $\SymMonCat$-functor from
  $\PresOp\SymMonCat$ to $\LawCat\mL$. This functor preserves all
  $\regcard$-powers, as the following calculation shows
  \inlinediagram{lawvere-theory-completeness-proof-71}

  Thus we have a $\regcard$-Lawvere $\SymMonCat$-theory $\mL$,
  and a Lawvere theory morphism $\Functor^{\mi} \of \mL \to \mDiag\mi$
  for every $\mi$. As this morphism is componentwise a cone, we deduce
  that $\pair\mL\Functor$ is a cone.

  Given any other cone $\pair{\mLv}{\Functorv}$, we get componentwise
  cones $\pair{\homset[\LawCat{\mLv}]\enA\enAv}{\Functorv^{\mi}_{\enA,\enAv}}$,
  hence a unique factorisation $\Functorw_{\enA,\enAv} \of
  \homset[\LawCat{\mLv}]\enA\enAv \to
  \homset[\LawCat\mL]\enA\enAv$. Another invocation of \lemmaref{lawvere theory
    construction}(\ref{lawvere theory construction: functors}) shows
  these form the components of a $\SymMonCat$-functor $\Functorw$, and
  another calculation shows it preserves $\regcard$-powers. The
  componentwise uniqueness shows the uniqueness of this functor, hence
  $\pair\mL\Functor$ is the limiting cone for $\mDiag$.

  Conversely, assume we have a limiting cone $\pair\mL\Functor$. As
  $\SymMonCat$ is complete, for every $\enA$, $\enAv$, we have some
  cone $\homset[\mLv]\enA\enAv$ for
  $\homset[\LawCat{\mDiag\mi}]\enA\enAv$. Hence, by the previous
  direction of the proof, these form a limiting cone
  $\pair\mLv\Functorv$, and we have a unique isomorphism
  $\pair\mL\Functor \isomorphic \pair\mLv\Functorv$. As isomorphisms
  of Lawvere theories are componentwise isomorphisms, each component
  $\pair{\homset[\LawCat\mL]\enA\enAv}{\Functor_{\enA,\enAv}}$ is thus
  a limiting cone. The other commutative diagrams follow from
  $\Functor$ being a cone of Lawvere theories, and their uniqueness
  follows from universality.
\end{proof}