\Section{Algebraic \cbpv{} models}\sectionlabel{algebraic cbpv models}
We define a subclass of \cbpv{} models arising from a Lawvere
theory.

\begin{definition}
  Let $\regcard$ be a regular cardinal, and $\ValCat$ a
  locally $\regcard$-presentable category, and $\mX$ a set. A
  \defterm{$\regcard$-presentable type assignment for $\mX$ in $\ValCat$} is a type
  assignment for $\mX$ in $\Pres\ValCat$.
\end{definition}

Note that every locally $\regcard$-presentable type assignment in
$\ValCat$ induces an ordinary type assignment in $\ValCat$, as
$\Pres\ValCat$ is a subcategory of $\ValCat$.

\begin{example}\examplelabel{presentable type assignment}
  If $\StorVal$ is a finite set denoting storable values, the type
  assignment from \exampleref{type-assignment-example}: \[
  \lookupop \of \StorVal \qquad\updateop \of
  \arity\terminal\StorVal
  \]
  is a finitely-presentable
  type assignment for $\set{\lookupop, \updateop}$ in $\Set$.
\end{example}


We can now define algebraic models of \cbpv{}:

\begin{definition+}{\algebraic{definition}{non-hierarchical cbpv model}}
\definitionlabel+{non-hierarchical algebraic cbpv model}
  Let $\Opset$ be a set. An \defterm{\DELTA{algebraic} \cbpv{}
    $\Opset$-model} is a quintuple
  \[
  \seq{\regcard, \ValCat,\arities,\mL,\LawOpsem\mL\placeholder}
  \] where:
  \begin{itemize}
  \item \DELTA{$\regcard$ is a regular cardinal};
  \item $\ValCat$ is a \DELTA{$\regcard$-Power category with respect to the
    cartesian closed structure}, called the
    \defterm{value category};
  \item $\arities$ is a \DELTA{$\regcard$-presentable} type assignment for $\Opset$ in
    $\ValCat$;
  \item \DELTA{$\mL$} is a
    \DELTA{$\regcard$-Lawvere $\ValCat$-theory.}
  \item $\DELTA{\LawOpsem\mL\placeholder}$ assigns to every $\mop \of
    \arity\Ar\Pa$ in $\Opset$ an algebraic operation
    $\DELTA{\LawOpsem\mL\mop} \of \arity\Ar\Pa$ for $\DELTA{\mL}$.
  \end{itemize}
\end{definition+}

To aid the presentation, we use the plus suffix to reflect an
algebraic reformulation of a previously visited concepted. Thus,
\definitionref+{non-hierarchical algebraic cbpv model} is an algebraic
reformulation of \definitionref{non-hierarchical cbpv model}.

\begin{example}\examplelabel{global state algebraic cbpv model}
  The global state \cbpv{} model in \exampleref{global state cbpv
    model} can be viewed as an algebraic \cbpv{} model. Take
  $\regcard$ to be $\aleph_0$, $\ValCat$ to be $\Set$, $\arities$ to
  be the finitely-presentable type assignment for global state from
  \exampleref{presentable type assignment}, $\mL$ to be the global
  state theory $\GlobalStateTheory$, and $\algopsem[]\placeholder$ as
  the interpretation of look-up and update, as in \exampleref{IO to global state morphism}.
\end{example}

More generally, let
\(
  \seq{\regcard, \ValCat,\arities,\mL,\LawOpsem\mL\placeholder}
\)
be an algebraic $\Opset$-model.
Note that we can apply
the categorical equivalence $\Lawvere\ValCat
\equivalent \EnrichedRankedMonad\ValCat$ to $\mL$ and obtain a
$\regcard$-ranked strong monad over $\ValCat$. In light of \theoremref{monad<->theory
  preserves operations}, we have a $\Opset$-model
\[
\seq{\ValCat, \arities, \LawMonad\mL, \operation{\LawOpsem\mL\placeholder}{}}
\] Conversely, given a $\Opset$-model \[
\seq{\ValCat, \arities,
  \Monad, \opsem[]\placeholder}
\]
such that there is a regular cardinal $\regcard$ which makes $\ValCat$
a $\regcard$-Power category with respect to the cartesian structure,
$\arities$ a $\regcard$-presentable type assignment, and $\Monad$ be
$\regcard$-ranked, we obtain an algebraic $\Signature$-model. These
constructions are not inverse to each other. However, by composing the
two constructions we get a model in which the monad/theory is
isomorphic to the monad/theory of the starting model, and this
isomorphism preserves the operations.  The proper setting for this
fact requires us to introduce morphisms of $\Opset$-models. Then, this
fact can be phrased as a categorical equivalence between categories of
models. However, we have no other interest in morphisms of models and
in categorical constructions on models apart from the equivalence we
just described here. Therefore, we do not study morphisms of models in
this thesis.

To summarise, we presented enriched Lawvere theories and their
properties, and specialised our \cbpv{} models to models arising out
of some Lawvere theory and its operations.
