~ohad-kammar/ohads-thesis/trunk

\Section{Conservative restriction}\sectionlabel{cat cons rest}
For any effect hierarchy $\Signature$, let  $\pair\ValCat\Monad$ be a \cbpv{} model, let  $\arities$ be a type
assignment for $\carrier\Signature$ in $\ValCat$,  and, for all $\mop
\in \carrier\Signature$, an assignment of an algebraic operation of
type $\arity\Ar\Pa$ for $\Monad$.  These data constitute a semantic
model that ignores the effect hierarchy, and specifies meaning to all
the effects together. Our goal is to
construct a $\Signature$-model that takes the effect hierarchy into
account, when the \cbpv{} model is given \emph{algebraically}, as in \definitionref+{non-hierarchical algebraic cbpv model}. Recall that in this
case, a $\regcard$-Power category replaces $\ValCat$, the type
assignment is
$\regcard$-presentable, a
$\regcard$-Lawvere $\ValCat$-theory $\mL$ replaces $\Monad$, and algebraic
operations in this Lawvere theory replace the effect operations.

Our construction proceeds in two steps. First, we note that for every
$\e \in \E$ there is an \emph{initial} Lawvere theory
$\mL_{\pair\e\arities}$ amongst all Lawvere theories that have an operation of type $\arity\Pa\Ar$
for every $\mop \of \arity\Pa\Ar$ in $\e$. Because $\mL$ has
operations of type $\arity\Pa\Ar$ for every $\mop \of \arity\Pa\Ar$,
initiality implies the existence of a unique Lawvere theory morphism
\(
\LawHomo_{\e} \of \mL_{\pair\e\arities} \to \mL
\). The second step is to factorise this morphism using a
factorisation system of $\Lawvere\ValCat$:
\[
\LawHomo_{\e} \of \mL_{\pair\e\arities} \xepimor{\LawEpi_{\e}} \mL_{\e}
\xmonomor{\LawMono_{\e}} \mL
\]
This factorisation yields a $\Signature$-model, which we call the
\defterm{conservative restriction model}.


We need a few auxiliary definitions.
\begin{definition}
  Let $\ValCat$ be a $\regcard$-Power category with respect to the
  cartesian closed structure.
  A \defterm{$\regcard$-presentable signature $\LawSignature$}
  is a pair $\pair{\carrier\LawSignature}{\arities}$ consisting of a
  set $\carrier\LawSignature$ and a $\regcard$-presentable type assignment
    $\arities$ for $\carrier\LawSignature$ in $\ValCat$.

  \noindent
  Let $\LawSignature$ be a $\regcard$-presentable signature.
  A \defterm{$\LawSignature$-theory} is a pair
  $\pair\mL{\LawOpsem\mL\placeholder}$, where:
  \begin{itemize}
  \item $\mL$ is a $\regcard$-Lawvere $\ValCat$-theory, and
  \item $\LawOpsem\mL\placeholder$ assigns to each $\mop \of
    \arity\Ar\Pa$ in $\carrier\LawSignature$ an operation
    $\LawOpsem\mL\mop \of \arity\Ar\Pa$ in $\mL$.
  \end{itemize}

  \noindent
  Let $\mL$, $\mLv$ be two $\LawSignature$-theories. A \defterm{morphism
  $\LawHomo$ of $\LawSignature$-theories from $\mL$ to $\mLv$} is a
  morphism of Lawvere theories $\LawHomo \of \mL \to \mLv$ such that,
  for every $\mop \in \carrier\LawSignature$, $\LawHomo$ maps
  $\LawOpsem\mL\mop$ to $\LawOpsem\mLv\mop$.
\end{definition}

\begin{example}\examplelabel{lawvere signature, sig-theory, sig-theory
  morphisms}
  Take $\ValCat$ to be $\Set$, and let $\ValCat$ be any \emph{finite}
  set denoting storable values. Take $\LawSignature$ to be the
  signature with $\carrier\LawSignature$ a two element set
  $\set{\lookupop, \updateop}$ and the finitely-presentable type
  assignment to be $\lookupop \of \StorVal$, $\updateop \of
  \arity\terminal\StorVal$. Thus $\LawSignature$ is a
  finitely-presentable type assignment.

  The (finitary) Lawvere theory $\GlobalStateTheory$ is the Lawvere
  theory corresponding to the finitary global state monad
  $\GlobalStateMonad$. As we saw in \exampleref{IO to global state
    morphism}, this is a $\LawSignature$-theory. Moreover, the theory
  $\IOTheory[\parent\StorVal]$ is also a $\LawSignature$-theory, where
  $\lookupop$ is interpreted as the input operation and $\updateop$ as
  the output operation.

  Finally, in \exampleref{IO to global state morphism} we saw a
  Lawvere theory morphism $\LawHomo \of \IOTheory[\parent\StorVal] \to
  \GlobalStateTheory$ mapping input and output to look-up and update,
  respectively. Thus, $\LawHomo$ is a morphism of
  $\LawSignature$-theories.
\end{example}

The first ingredient in our construction is the following theorem:
\begin{theorem}\theoremlabel{initial signature theory}
  For every $\regcard$-presentable signature $\LawSignature$ in
  $\ValCat$ there exists an initial $\LawSignature$-theory
  $\SignatureTheory\LawSignature$.
\end{theorem}

\begin{proof}%
  Our proof consists of two parts. First, we establish the existence
  of the initial $\LawSignature$-theory when $\carrier\LawSignature$
  is a singleton $\set{\mop}$ using standard techniques for
  \defterm{free monads}. Once the existence of the
  $\SignatureTheory{\set{\mop \of \arity\Ar\Pa}}$ is established, we use the
  cocompleteness of $\Lawvere\ValCat$, and show that the required
  $\LawSignature$-theory is the coproduct of
  these Lawvere theories, namely
  \[
  \SignatureTheory\LawSignature =
  \sum_{\substack{\mop \in \carrier\LawSignature\\\mop \of
      \arity\Ar\Pa}}\SignatureTheory{\set{\mop\of\arity\Ar\Pa}}
  \]
  %
  Our use of free monads is not essential, but merely a
  convenience, for we can thus refer to published work on free
  monads. Other techniques, e.g., enriched
  sketches~\cite{kelly:basic-concepts-of-enriched-category-theory} can
  be used too, but we will not elaborate on them further. In order to
  not tie the proof to free monads, we
  isolated their use to a small part of the proof, and
  the rest of the proof does not depend on the use of free monads.

  Let $\SignatureFunctor$ be the evident $\ValCat$-endofunctor over $\ValCat$ given by
  \begin{mapdef*}
    \SignatureFunctor &\definedby \power\Ar{\copower\Pa{\parent\placeholder}} = (\Pa\times{\parent\placeholder})^{\Ar}
  \end{mapdef*}%
  Note that the underlying ordinary functor $\ordinary\SignatureFunctor$ preserves $\regcard$-directed
  colimits, as it is the composition of two adjoint
  functors between locally $\regcard$-presentable categories (see
  \theoremref{ranked adjoints}).  Hyland et
  al.~\cite[Section~2, prior to
    Example~6]{hyland-plotkin-power:sum-and-tensor}, employing
  techniques described by
  Kelly~\cite{kelly:a-unified-treatment-of-transfinite-constructions-for-free-algebras-free-monoids-colimits-associated-shieaves-and-so-on},
  describe several sufficient conditions for the existence of the free
  monad for $\SignatureFunctor$. For
  our purposes, it suffices that $\ordinary\SignatureFunctor$ is
  $\regcard$-ranked, $\ValCat$-enriched, and $\ValCat$ is locally
  $\regcard$-presentable, and then the \defterm{free $\ValCat$-monad $\FreeMonad\SignatureFunctor$}
  for $\SignatureFunctor$ exists. Its crucial three properties are:
  \begin{itemize}
  \item $\FreeMonad\SignatureFunctor$ is a $\regcard$-ranked $\ValCat$-monad;
  \item $\FreeMonad\SignatureFunctor$ has a generic effect $\mgen \of \arity\Ar\Pa$; and
  \item if $\Monadv$ is any other $\ValCat$-monad and $\mgenv \of \arity\Ar\Pa$
    is a generic effect for $\Monadv$, then there exists a unique
    $\ValCat$-monad morphism from $\FreeMonad\SignatureFunctor$ to
    $\Monadv$ mapping $\mgen$ to $\mgenv$.
  \end{itemize}
%
  By invoking \theoremref{monad<->theory preserves operations}, deduce
  that $\SignatureTheory{\set{\mop\of\arity\Ar\Pa}} \definedby
  \MonadTheory{\FreeMonad\SignatureFunctor}$ is the required Lawvere
  theory.

  Next, for an arbitrary $\regcard$-presentable signature $\LawSignature$, choose:
  \[
  \SignatureTheory\LawSignature \definedby
  \sum_{\substack{\mop \in \carrier\LawSignature\\\mop \of
      \arity\Ar\Pa}}\SignatureTheory{\set{\mop\of\arity\Ar\Pa}}
  \]
  And interpret each $\mop \in \carrier\LawSignature$ as $
  \LawOpsem{\SignatureTheory\LawSignature}\mop \definedby
  \injection_{\mop}\parent{\LawOpsem{\SignatureTheory{\set{\mop\of\arity\Ar\Pa}}}\mop}$, i.e.:
  \[
  \terminal \xto{\LawOpsem{\SignatureTheory{\set{\mop\of\arity\Ar\Pa}}}\mop}
  \homset[\LawCat{\SignatureTheory{\set\mop\of\arity\Ar\Pa}}]\Ar\Pa
  \xto{\injection_{\mop}}
  \sum_{\substack{\mop \in \carrier\LawSignature\\\mop \of
      \arity\Ar\Pa}}\SignatureTheory{\set{\mop\of\arity\Ar\Pa}}
  \]
  If $\mL$ is any other $\LawSignature$-theory, then, for each
  $\mop\in\carrier\LawSignature$, $\mL$ is a
  $\set{\mop\of\arity\Ar\Pa}$-theory, and there is a unique
  morphism $\LawHomo_{\mop} \of
  \SignatureTheory{\set{\mop\of\arity\Ar\Pa}} \to \mL$ preserving
  the interpretation of $\mop$. Choose as $\LawHomo \of
  \SignatureTheory\LawSignature \to \mL$ the coproduct morphism
  $\LawHomo \definedby
  \coprodmorphismseq[\mop\in\carrier\LawSignature]{\LawHomo_{\mop}}$.
  Then we have:
  \inlinediagram{free-theory-proof-01}

  Conversely, if $\LawHomov \of \SignatureTheory\LawSignature \to \mL$
  is any other $\LawSignature$-theory morphism, then $\LawHomov_{\mop}
  \definedby \LawHomov \compose \injection_{\mop}$ is a
  $\set{\mop\of\arity\Ar\Pa}$-theory morphism from
  $\SignatureTheory{\set{\mop\of\arity\Ar\Pa}}$ to $\mL$, hence
  $\LawHomov_{\mop} = \LawHomo_{\mop}$. For all $\mop\in\carrier\LawSignature$, we have
  $\LawHomov\compose\injection_{\mop} =
  \LawHomo\compose\injection_{\mop}$, hence $\LawHomov = \LawHomo$, and
  we have uniqueness.
\end{proof}

\begin{example}\examplelabel{initial sig-theory}
Let $\StorVal$ be a finite set denoting storable values. Consider the
signature $\LawSignature$ from \exampleref{lawvere signature, sig-theory, sig-theory
  morphisms}, $\set{\lookupop\of\StorVal,
  \updateop\of\arity\terminal\StorVal}$. Consider the input/output
theory $\IOTheory[\parent\StorVal]$ from \exampleref{lawvere signature, sig-theory, sig-theory
  morphisms}. We will show $\IOTheory[\parent\StorVal]$ is the initial
$\LawSignature$-theory.

We already saw that $\IOTheory[\parent\StorVal]$ is a $\LawSignature$-theory.
Let $\pair\mL{\LawOpsem\mL\placeholder}$ be any other
$\LawSignature$-theory. We therefore have a corresponding monad $\Monad$
over $\Set$ with algebraic operations $\lookupop \of \StorVal$ and
$\updateop \of \arity\terminal\StorVal$.

For every set $\mX$, define inductively:
\begin{mapdef*}
  \mmorph_{\mX} \of & \IOMonad[\parent\StorVal]\mX &\to \Monad\mX \\
  \mmorph_{\mX} \of
    & \mx & \mapsto \unit(\mx) \\
    & \pair I{\seq[\mval\in\StorVal]{\mterm_{\mval}}} & \mapsto \lookupop(\ilam\mval{\mmorph_{\mX}(\mterm_{\mval})})(\unitval) \\
    & \triple O\mval\mterm                          & \mapsto \updateop(\ilam\unitval{\mmorph_{\mX}(\mterm)})(\mval)
\end{mapdef*}%
To establish that $\mmorph$ is a monad morphism from
$\IOMonad[\parent\StorVal]$ to $\Monad$, we use the following special
case of a result by Plotkin and
Power~\cite[Proposition~1]{plotkin-power:algebraic-operations-and-generic-effects},
adapted to include parameter types:
\begin{quote}
  Let $\Monad$ be a monad over $\Set$, and $\mop \of \arity\Ar\Pa$ an algebraic operation for $\Monad$. Then:
  \begin{enumerate}
  \item\label{algebraic operations naturality} the transformation
    $\mop \of (\Monad\placeholder)^{\Ar} \to
    (\Monad\placeholder)^{\Pa}$ is natural; and
  \item\label{algebraic operations respect multiplication} this
    transformation respects the monadic multiplication $\monmult$ in
    the sense that, for all $\ilam\mar{\hat\mterm_{\mar}}$ in
    $(\Monad^2\mX)^{\Ar}$ and $\mpa \in \Pa$:
    \[
    \mop(\ilam\mar{\monmult(\hat\mterm_{\mar})})(\mpa) =
    \ilam\mpa{\monmult(\mop(\ilam\mar{\hat\mterm_{\mar}})(\mpa))}
    \]
  \end{enumerate}
\end{quote}
Straightforward calculations show that the naturality of $\unit$,
$\lookupop$, and $\updateop$ implies that of $\mmorph$, and that, by
definition, $\mmorph$ preserves the monadic unit. A straightforward
inductive argument using the monad laws and property~\ref{algebraic
  operations respect multiplication} above shows that $\mmorph$
preserves the monadic multiplication.

Straightforward calculation shows that $\mmorph$ preserves the
operations. Indeed, for every $\ilam\mval{\mterm_{\mval}}$ in
$(\IOMonad[\parent\StorVal]\mX)^{\StorVal}$, we have:
\inlinediagram{initial-signature-theory-01}
Thus, $\mmorph$ maps $\inputop$ to $\lookupop$. A similar calculation
shows that $\mmorph$ maps $\outputop$ to $\updateop$. Therefore, using
the equivalence between Lawvere theories and ranked monads, we deduce
there exists a $\LawSignature$-theory morphism $\LawHomo \of \IOTheory[\parent\StorVal]
\to \mL$, corresponding to $\mmorph$.

To conclude, assume $\LawHomov \of \IOTheory[\parent\StorVal] \to \mL$ is any
$\LawSignature$-theory morphism. We therefore have a monad morphism
$\hat\mmorph \of \IOMonad[\parent\StorVal] \to \Monad$, mapping
$\inputop$ and $\outputop$ to $\lookupop$ and $\updateop$,
respectively. A straightforward inductive argument using the
preservation of the unit and the mapping of the operations shows that
$\hat\mmorph$ and $\mmorph$ coincide. We will only demonstrate how
$\mmorph$ and $\hat\mmorph$ agree on $\pair I{\seq{\mterm_{\mval}}}$,
  if they agree over all components $\mterm_{\mval}$. As $\hat\mmorph$
  maps $\inputop$ to $\lookupop$, we have:
\inlinediagram{initial-signature-theory-02}
Thus, \[
\hat\mmorph(\pair I{\seq{\mterm_{\mval}}})
=
\lookupop(\ilam\mval{\hat\mmorph(\mterm_{\mval})})(\unitval)
\explain={induction hypothesis}
\lookupop(\ilam\mval{\mmorph(\mterm_{\mval})})(\unitval)
\explain={\DefinitionExp{\mmorph}}
\mmorph(\pair I{\seq{\mterm_{\mval}}})
\]
and $\hat\mmorph$ and $\mmorph$ agree on $\pair
I{\seq{\mterm_{\mval}}}$.

As $\mmorph$, $\hat\mmorph$ coincide, $\LawHomo$ and $\LawHomov$
coincide. Thus, $\IOTheory[\parent\StorVal]$ is the initial
$\LawSignature$-theory $\SignatureTheory{\LawSignature}$.
Similar arguments show that the theories  $\ITheory[\parent\StorVal]$
and $\OTheory[\parent\StorVal]$ corresponding to the monads
$\IMonad[\parent\StorVal]$ and $\OMonad[\parent\StorVal]$, respectively, are the initial
$\set{\lookupop\of\StorVal}$-, and
$\set{\updateop\of\arity\terminal\StorVal}$-theories, respectively.
\end{example}

The following theorem is our central construction:
\begin{theorem}[conservative restriction model]\theoremlabel{categorical
  conservative restriction}
  Let $\Opset$ be a set, and
  \[
  \mModel = \seq{\regcard, \ValCat,\arities,\mL,\LawOpsem\mL\placeholder}
  \] an algebraic \cbpv{} $\Opset$-model. For every effect
  hierarchy $\Signature$ whose set of operation is
  $\Opset$, and for every factorisation system $\pair{\FunctorFact\Epi}{\FunctorFact\Mono}$
  in $\Lawvere\ValCat$, the following data define an algebraic $\Signature$-model
  \[
  \conservative\mModel \definedby
\seq{\regcard, \ValCat, \arities, {\TheoryPresheaf\placeholder,
    \algopsem[\placeholder]\placeholder}}
  \] together with the auxiliary data
  $\seq{\LawSignature_{\placeholder}, \LawHomo_{\placeholder},
    \LawEpi_{\placeholder}, \LawMono_{\placeholder}, \LawHomos_{\placeholder}}$, where:
\begin{itemize}
\item $\LawSignature_{\placeholder}$ assigns to every $\e \in \E$ the
  $\regcard$-presentable signature given by restricting
  $\arities$ to the subset $\e \subset\Opset$,
  $\LawSignature_{\e} \definedby \pair\e{\restrict\arities\e}$;
\item $\LawHomo_{\placeholder}$ assigns to every $\e \in \E$ the
  unique morphism $\LawHomo_{\e} \of
  \SignatureTheory{\LawSignature_{\e}} \to \mL$ mapping, for every
  $\mop \in \e$, the operation
  $\LawOpsem{\SignatureTheory{\LawSignature_{\e}}}\mop$ to
  $\LawOpsem\mL\mop$, where $\SignatureTheory{\LawSignature_{\e}}$ is
  the initial $\LawSignature_{\e}$ theory from \theoremref{initial signature theory};
\item for every $\e \in \E$,
  $\triple{\TheoryPresheaf{\e}}{\LawEpi_{\e}}{\LawMono_{\e}}$ is a specified
  $\pair{\FunctorFact\Epi}{\FunctorFact\Mono}$ factorisation:
  \[
  \LawHomo_{\e} \of \SignatureTheory{\LawSignature_{\e}}
  \xepimor{\LawEpi_{\e}} \TheoryPresheaf{\e} \xmonomor{\LawMono_{\e}} \mL
  \]
\item $\algopsem[\placeholder]\placeholder$ assigns to each $\e \in
  \E$ and $\mop \in \e$ the unique operation $\algopsem\mop$ in
  $\mL_{\e}$ such that $\LawEpi_{\e}$ maps
  $\LawOpsem{\SignatureTheory{\LawSignature_{\e}}}\mop$ to
    $\algopsem\mop$, and then, $\LawMono_{\e}$ maps
    $\algopsem{\mop}$ to $\LawOpsem\mL\mop$.
\item $\LawHomos_{\placeholder}$ assigns to each $\e \subset\e'$ in
  $\E$ the unique morphism $\LawHomos_{\e\subset\e'} \of
  \SignatureTheory{\LawSignature_{\e}} \to \TheoryPresheaf{\e'}$ that, for every
  $\mop \in \e$, maps
  $\LawOpsem{\SignatureTheory{\LawSignature_{\e}}}\mop$ to
  $\algopsem[\e']\mop$;
\item $\TheoryPresheaf\placeholder$ assigns to every $\e \subset\e'$
  in $\E$ the unique fill-in morphism:
  \inlinediagram{conservative-restriction-model-01}
  and, moreover, this morphism is in $\FunctorFact\Mono$.
\end{itemize}
We call $\conservative\mModel$ the \defterm{conservative restriction $\Signature$-model} for
the given $\Opset$-model, \defterm{relative to the given
  factorisation system. }
\end{theorem}

\begin{proof}%
First, we show these data are well-defined. Consider any $\e \in \E$. As $\arities$ is a
$\regcard$-presentable type assignment,
$\LawSignature_{\e}$ is a well-defined $\regcard$-presentable type assignment in
$\ValCat$. If we restrict $\LawOpsem\mL\placeholder$ to $\e$, we
obtain a $\LawSignature_{\e}$-theory
$\pair\mL{\restrict{\LawOpsem\mL\placeholder}\e}$. By initiality,
there exists a unique morphism $\LawHomo_{\e} \of
\SignatureTheory{\LawSignature_{\e}} \to \mL$ preserving the
interpretations of all the operations in $\e$. Thus $\LawHomo_{\e}$ is
well-defined, and consequently, so are $\TheoryPresheaf\e$,
$\LawEpi_{\e}$, and $\LawMono_{\e}$.

Consider any $\mop \in \e$. By \corollaryref{unique algebraic
operation via monad morphism} and \theoremref{monad<->theory preserves
operations}, there exists a unique algebraic operation
$\algopsem\mop$ for $\TheoryPresheaf\e$ such that $\LawEpi_{\e}$ maps
$\LawOpsem{\SignatureTheory{\LawSignature_{\e}}}\mop$ to $\algopsem\mop$,
and $\algopsem\mop$ is well-defined. Since both $\LawHomo$ and
$\LawEpi$ preserve the interpretation of $\mop$, $\LawHomo_{\e} =
\LawMono_{\e}\compose\LawEpi_{\e}$, we deduce by \corollaryref{unique algebraic
operation via monad morphism} and \theoremref{monad<->theory preserves
operations} that $\Mono_{\e}$ also preserves the
interpretation of $\mop$.

Consider any $\e \subset \e'$ in $\E$. By restricting
$\algopsem[\e']\placeholder$ to $\e$, we obtain a
$\LawSignature_{\e}$-theory
$\pair{\TheoryPresheaf{\e'}}{\restrict{\algopsem[\e']\placeholder}{\e}}$. Therefore,
there exists a unique morphism $\LawHomos_{\e\subset\e'} \of
\SignatureTheory{\LawSignature_{\e}}\to \TheoryPresheaf{\e'}$
preserving the interpretations of the effects in $\e$, and
$\LawHomos_{\placeholder}$ is well-defined.

Thus, both $\LawMono_{\e}\compose \LawEpi_{\e}$ and
$\LawMono_{\e'}\compose \LawHomos_{\e\subset\e'}$ are
$\LawSignature_{\e}$-theory homomorphisms. Initiality of
$\SignatureTheory{\LawSignature_{\e}}$ means that
\inlinediagram{conservative-restriction-model-02}

By the orthogonality property of factorisation systems, we deduce the
existence of a unique fill-in morphism:
\numbereddiagram[\diagramlabel{conservative restriction model diagonal
construction}]{conservative-restriction-model-03}
The commutativity of these two triangles implies, again by \corollaryref{unique algebraic
operation via monad morphism} and \theoremref{monad<->theory preserves
operations}, that $\TheoryPresheaf{\e\subset\e'}$ preserves the
operations in $\e$. Also, note that Bousfield's factorisation
theorem~(\theoremref{bousfield's factorisation theorem}(\ref{bousfield
composition condition})) implies that
$\TheoryPresheaf{\e\subset\e'}$ is an $\FunctorFact\Mono$-morphism.

These data do yield an algebraic $\Signature$-model. Indeed, by their
choice, $\regcard$ is a regular cardinal, and $\ValCat$ a
$\regcard$-Power category. Our choice of $\TheoryPresheaf\placeholder$
indeed yields a functor from $\E$ to $\Lawvere\ValCat$. First, note
that $\LawEpi_{\e}$ is a $\LawSignature_{\e}$-morphism from
$\SignatureTheory{\LawSignature_{\e}}$ to $\TheoryPresheaf\e$, hence
initiality implies $\LawEpi_{\e} =
\LawHomos_{\e\subset\e}$. Consequently,
\inlinediagram{conservative-restriction-model-04}
By orthogonality we deduce that $\TheoryPresheaf{\e\subset\e} =
\id$. Consider any $\e \subset \e' \subset \e''$ in $\E$, then
${\TheoryPresheaf{\e'\subset\e''}\compose\LawHomos_{\e\subset\e'}}$ is a
$\LawSignature_{\e}$-theory morphism from $\SignatureTheory{\LawSignature_{\e}}$ to
$\TheoryPresheaf{\e''}$. By initiality,
\numbereddiagram[\diagramlabel{conservative restriction model lemma}]{conservative-restriction-model-05}
Thus, on the one hand, we have:
\inlinediagram{conservative-restriction-model-06}
Thus, by definition,
$\TheoryPresheaf{\e\subset\e''} =
\TheoryPresheaf{\e'\subset\e''}\compose\TheoryPresheaf{\e\subset\e'}$. Thus,
we have a functor $\TheoryPresheaf \of \E \to \Lawvere\ValCat$. By
fiat, $\algopsem\placeholder$ assigns operations as required, and we
have seen that $\TheoryPresheaf\placeholder$ preserves them.
\end{proof}

\begin{example}\examplelabel{global state conservative restriction}
  Let $\Signature$ be the effect hierarchy for global state, and
  $\StorVal$ a finite set such that $\cardinality\StorVal \geq 2$
  denoting storable values. Consider the algebraic \cbpv{}
  $\Opset$-model for global state from \exampleref{global
    state algebraic cbpv model}, and the
  ${\FunctorFact{\text{surjective}}}$-${\FunctorFact{\text{injective}}}$
  factorisation system arising from the surjective-injective
  factorisation system of $\Set$ by \theoremref{lawvere
    factorisation}. We work out the explicit description of the
  conservative restriction model.

  Comparing the construction of the initial morphism $\mmorph \of
  \IOMonad[\parent\StorVal] \to \GlobalStateMonad$ in
  \exampleref{initial sig-theory} to the definition of the morphisms
  $\LawHomo \of \IOTheory[\parent\StorVal] \to \GlobalStateTheory$ in
  \exampleref{IO to global state morphism}, and
  $\LawHomo_{\set\lookupop} \of \ITheory[\parent\StorVal] \to
  \EnvTheory$ and $\LawHomo_{\set\updateop} \of
  \OTheory[\parent\StorVal] \to \OverwriteTheory$ from
  \exampleref{global state factorisation}, shows these are indeed the
  initial $\Opset$-, $\set{\lookupop}$-, and
  $\set{\updateop}$-theory morphisms, respectively. The initial
  $\emptyset$-theory morphism $\LawHomo_{\emptyset} \of \PresOp[\aleph_0](\Set)
  \to \GlobalStateTheory$ is the functor
  $\LawFunctor\GlobalStateTheory\placeholder$.

  In \exampleref{IO to global state morphism} we noted that the monad
  morphism corresponding to $\LawHomo_{\Opset}$ is surjective,
  From \propositionref{lawvere factorisation
    epi characterisation} we conclude that $\LawHomo_{\Opset}$ is in the class
  $\FunctorFact{\text{surjective}}$. Therefore, we have the
  factorisation:
  \[
  \LawHomo_{\Opset} \of \IOTheory[\parent\StorVal]
  \xepimor{\LawHomo_{\Opset}}
  \GlobalStateTheory \xmonomor{\id}
  \GlobalStateTheory
  \]
  In \exampleref{global state factorisation} we presented a
  factorisation of $\LawHomo_{\set{\lookupop}}$ and $\LawHomo_{\set{\updateop}}$:
  \begin{mapdef*}
  \LawHomo_{\set\lookupop} &\of \ITheory[\parent\StorVal]
  &\xtwoheadrightarrow{\LawEpi_{\set\lookupop}} \EnvTheory
  \xrightarrowtail{\LawMono_{\set\lookupop}} \GlobalStateTheory
  \\
  \LawHomo_{\set\updateop} &\of \OTheory[\parent\StorVal]
  &\xtwoheadrightarrow{\LawEpi_{\set\updateop}} \OverwriteTheory
  \xrightarrowtail{\LawMono_{\set\updateop}} \GlobalStateTheory
  \end{mapdef*}%
  The $\mX,\terminal$
  components of this functor act on morphisms by post-composing with
  the monadic unit $\unit_{\GlobalState}$ (see
  \exampleref{monad->theory construction}). As $\StorVal$ is
  non-empty, this monadic unit is injective, hence post-composing with
  it yields a monomorphism between the homsets. Thus,
  $\LawHomo_{\emptyset}$ is a
  $\FunctorFact{\text{injective}}$-morphism, and we have the
  factorisation:
  \[
  \LawHomo_{\emptyset} \of \PresOp[\aleph_0](\Set) \xepimor{\id} \PresOp[\aleph_0](\Set) \xmonomor{\LawHomo_{\emptyset}}\GlobalStateTheory
  \]

  Therefore, the object part of the functor $\TheoryPresheaf\placeholder$ for the
  conservative restriction model agrees with the model in
  \exampleref{global state algebraic cbpv model}. We know that the
  $\FunctorFact{\text{injective}}$-part of the factorisation preserves
  the operations, hence uniquely determines them. As these arrows are
  precisely the morphisms
  $\TheoryPresheaf{\e\subset\Opset}$ in the model from
  \exampleref{global state algebraic cbpv model}, we know they
  preserve the operations. Therefore, the operations in the
  conservative restriction model coincide with the operations in the
  model from \exampleref{global state algebraic cbpv model}. The fact
  that the   $\FunctorFact{\text{injective}}$-part of the
  factorisation coincides with   $\TheoryPresheaf{\e\subset\Opset}$ in the model from
  \exampleref{global state algebraic cbpv model} also means the
  lower-right triangle in the orthogonality square defining
  $\TheoryPresheaf{\e\subset\e'}$ commutes. Because they preserve the
  operations, initiality of $\SignatureTheory{\LawSignature_{\e}}$
  means the upper-left triangle also commutes. Therefore, the
  morphism parts of the functors $\TheoryPresheaf\placeholder$ of the
  two models coincide.

  In conclusion, the model in \exampleref{global state algebraic
    cbpv model} is the conservative restriction model.
\end{example}

%%% When you add recursion, there should be an example here for
%%% conservative restricting some recursion model.

This example illustrates that the conservative restriction model
construction uniformly gives rise to a natural, intuitive
$\Signature$-model that seemed previously non-uniform.  It also
demonstrates that the conservative restriction models allow us to
avoid explicitly \emph{specifying} an exponentially large
structure. Instead, we only need to define the desired algebraic
\cbpv{} model, and then \emph{derive} the data we require as
properties of this structure. As we will see, the conservative
restriction model is tightly related to the underlying \cbpv{} model
that gives rise to it. However, specifying a Lawvere theory is still an
elaborate process: even when the theory is given as a monad, we need
to enrich it, and verify it has a rank.

In summary, we defined the hierarchical algebraic models, presented
the categorical conservative restriction construction, and showed that
when we apply it to global state we obtain the global state
hierarchical model.