~ohad-kammar/ohads-thesis/trunk

\Chapter{Relational models}{We search our lives forever for perfection
in relations}{Simply Red}\chapterlabel{predicates}
\cats{}%
In this
chapter we study a useful subclass of our categorical models in which
the objects are suitable \defterm{relations}, subsets in the
set-theoretic case and \wchain-closed subsets in the domain-theoretic
case. Relational models organise the data required to present
\defterm{logical relations}
proofs~\cite{filinski-on-the-relations-between-monadic-semantics,mitchell:type-systems-for-programming-languages,
  reynolds:on-the-relation-between-direct-and-continuation-semantics}
for relating different semantic models.

We leave a general account of relational models to future work. Here,
we only consider predicates over sets. However, we
structure our account in a form we believe holds in greater
generality.

First, in \sectionref{logical relations}, we introduce set-theoretic logical
relations as a category. Next, in \sectionref{monadic lifting}, we present our \defterm{monadic lifting}
construction, which we use in \corollaryref{free lifting} to relate the conservative
restriction model of \theoremref{categorical conservative restriction}
and the benchmark model of \exampleref{benchmark model}.

\Section{Set-theoretic logical relations}\sectionlabel{logical relations}
We define predicates over sets:
\begin{definition}The category $\PredCat[\Set]$ of set-theoretic
  predicates is given as follows:
  \begin{itemize}
    \item
    the \textbf{objects} consist of pairs $\pair \mX\mPred$ where $\mX$ is a
    set and $\mPred$ is a subset of $\mX$; and
    \item
    the \textbf{morphisms} from $\pair\mX\mPred$ to $\pair\mY\mPredv$ consist of pairs
    $\pair \mmorph{\lmorph}$ where $\mmorph \of \mX \to \mY$ is a
    function and $\lmorph \of \mPred \to \mPredv$ such that
    \inlinediagram{predicate-morphisms-01}
  \end{itemize}
\end{definition}
We will denote objects of $\PredCat$ as $\mPred\subset\mX$, and say
that $\mPred$ is a \defterm{predicate over $\mX$}. Note that
if $\lmorph$ exists, then it is uniquely determined by $\mmorph$, and
we say that $\mmorph$ \defterm{lifts} to a morphism from
$\mPred\subset\mX$ to $\mPredv\subset\mY$. Also note that $\PredCat$
is categorically equivalent to the full subcategory of the arrow
category $\Set^{\ArrowCat}$ induced by the morphisms in the
$\Mono$-class of the surjection-injection factorisation system of
$\Set$.

As is well-known:
\begin{proposition}
  The category $\PredCat$ is cartesian closed and has all products and
  coproducts. As a consequence, it is distributive.
  This structure is given as follows:
  \begin{itemize}
    \item \textbf{products:} We have, $\prod_{\mind \in
      \IndexSet}\parent{\mPred_{\mind}\subset\mX_{\mind}} =
      \parent{\prod_{\mind\in\IndexSet}\mPred_{\mind}} \subset
      \parent{\prod_{\mind\in\IndexSet}\mX_{\mind}}$, and the
      set-theoretic projections lift to the product of predicates. Given,
      for all $\mind \in \IndexSet$, a morphism
      ${\pair{\mmorph_{\mind}}{\lmorph_{\mind}}\of\mPredv\subset\mY\to\mPred_{\mind}\subset\mX_{\mind}}$,
      then $\prodmorphismseq{\pair{\mmorph_{\mind}}{\lmorph_{\mind}}}
      =
      \pair{\prodmorphismseq{\mmorph_{\mind}}}{\prodmorphismseq{\lmorph_{\mind}}}$.
    \item \textbf{coproducts:} Similarly, $\sum_{\mind \in
      \IndexSet}\parent{\mPred_{\mind}\subset\mX_{\mind}} =
      \parent{\sum_{\mind\in\IndexSet}\mPred_{\mind}} \subset
      \parent{\sum_{\mind\in\IndexSet}\mX_{\mind}}$, and the
      set-theoretic injections lift to the coproduct of predicates. Given,
      for all $\mind \in \IndexSet$, a morphism
      $\pair\mmorph\lmorph\of\mPred_{\mind}\subset\mX_{\mind}\to\mPredv\subset\mY$,
      then $\coprodmorphismseq{\pair{\mmorph_{\mind}}{\lmorph_{\mind}}}
      =
      \pair{\coprodmorphismseq{\mmorph_{\mind}}}{\coprodmorphismseq{\lmorph_{\mind}}}$.
    \item \textbf{exponentials:}
      $\parent{\mPredv\subset\mY}^{\mPred\subset\mX} =
      \mPredr\subset{\mY^{\mX}}$, where $\mPredr$ is the subset of all
      functions from $\mX$ to $\mY$ that lift. Explicitly,
      \[
      \mPredr = \set{\mmorph \of \mX \to \mY \suchthat \text{ for all
          $\mpred$ in $\mPred$, $\mmorph(\mpred) \in \mPredv$}}
      \]
      The evaluation map lifts to the evaluation map in
      $\PredCat$, and for every predicate morphism
      \[
      \pair\mmorph\lmorph\of
      \parent{\mPreds\subset\mZ}\times\parent{\mPred\subset\mX} \to \mPredv
      \subset\mY
      \] the curried function $\ilam\mX\mmorph$ lifts to $\ilam{\mPred\subset\mX}{\pair\mmorph\lmorph}$.
  \end{itemize}
\end{proposition}
\begin{proof}%
  Jacobs~\cite[Section~9.2 and
    Exercise~9.2.1]{jacobs:categorical-logic-and-type-theory} includes
  this structure as an
  exercise. Katsumata~\cite{katsumata:relating-computational-effects-by-TT-lifting-journal}
  spells it out in detail.
\end{proof}

The following category is the central concept of this chapter:
\begin{definition}
  The category $\LogRel$ of set-theoretic logical relations is given
  by:
  \begin{itemize}
  \item the \textbf{objects} $\mX$ consist of triples
    $\triple{\mX_1}{\mX_2}{\lX}$, where $\mX_1$ and $\mX_2$ are
    sets and $\lX$ is a predicate over $\mX_1\times\mX_2$; and
  \item the \textbf{morphisms} $\mmorph \of \mX\to\mY$ consist of triples
    $\triple{\mmorph_1}{\mmorph_2}{\lmorph}$, where
    $\pair{\mmorph_1\times\mmorph_2}{\lmorph}$ is a predicate morphism
    from $\lX \subset \mX_1\times\mX_2$ to $\lY \subset\mY_1\times\mY_2$.
  \end{itemize}
\end{definition}

We have the following forgetful functors:
\begin{mapdef*}[2]
  \SetPairFun &\of \LogRel &\to \Set\times\Set                                                           & \CodFun     &\of \PredCat &\to\Set \\
              &\hphantom{\of}\triple{\mX_1}{\mX_2}{\lX} &\mapsto \pair{\mX_1}{\mX_2}                      &        &\hphantom{\of}\mPred \subset\mX&\to\mX\\
              &\hphantom{\of}\triple{\mmorph_1}{\mmorph_2}{\lmorph} &\mapsto \pair{\mmorph_1}{\mmorph_2}  &              &\hphantom{\of}\pair{\mmorph}\lmorph &\mapsto \mmorph
  \\
  \PredFun    &\of \LogRel &\to \PredCat \\
              &\hphantom{\of}\triple{\mX_1}{\mX_2}{\lX} &\mapsto \lX \subset \mX_1\times\mX_2 \\
              &\hphantom{\of}\triple{\mmorph_1}{\mmorph_2}{\lmorph}&\mapsto \pair{\mmorph_1\times\mmorph_2}{\lmorph}
\end{mapdef*}%
In fact, $\LogRel$ arises as the pullback square in the (large)
category of categories and functors:
\inlinediagram{logical-relations-pullback-01} This known
characterisation is part of the logical relations folklore, see, for example,
Katsumata~\cite{katsumata:relating-computational-effects-by-TT-lifting-journal}.
We expect this characterisation to be useful when
generalising from sets and subsets to objects in a category and their
predicates.  As in $\PredCat$, note that the morphism $\lmorph$, if it
exists, is uniquely determined by the components $\mmorph_1$,
$\mmorph_2$. When $\lmorph$ exists, we say that
$\pair{\mmorph_1}{\mmorph_2}$ \defterm{lifts} to $\LogRel$.

The following result is well-known:
\begin{proposition}
  The category $\LogRel$ is cartesian closed and has all products and
  coproducts. As a consequence, it is distributive. The functor
  $\SetPairFun$ preserves the products, coproducts and this closed
  structure. Explictly, these structures are given as follows:
  \begin{itemize}
    \item \textbf{products:} $\prod_{\mind \in
      \IndexSet}\mX^{\mind} =
      \triple{\prod_{\mind\in\IndexSet}\mX_1^{\mind}}
             {\prod_{\mind\in\IndexSet}\mX_2^{\mind}}
             {\dot{\prod}_{\mind\in\IndexSet}\mX^{\mind}}
$ where
      \[
       {\dot{\prod}_{\mind\in\IndexSet}\mX^{\mind}}
       = {\set{\pair{\seq{\mx_1^{\mind}}}{\seq{\mx_2^{\mind}}}\suchthat
                 \forall
                 \mind\in\IndexSet.\pair{\mx_1^{\mind}}{\mx_2^{\mind}}\in\lX^{\mind}}}
             \] The
      pair of set-theoretic projections lifts to the product of predicates. Given,
      for all $\mind \in \IndexSet$, a morphism
      $\mmorph^{\mind}\of\mY
      \to \mX^{\mind}$,
      then the pair $\pair{\prodmorphismseq[\mind\in\IndexSet]{\mmorph_1^{\mind}}}
                 {\prodmorphismseq[\mind\in\IndexSet]{\mmorph_2^{\mind}}}$
                 lifts to $
      \prodmorphismseq[\mind\in\IndexSet]{\mmorph^{\mind}}$.
    \item \textbf{coproducts:} $\sum_{\mind \in
      \IndexSet}\mX^{\mind} =
      \triple{\sum_{\mind\in\IndexSet}\mX_1^{\mind}}
             {\sum_{\mind\in\IndexSet}\mX_2^{\mind}}
             {\sum_{\mind\in\IndexSet}\lX  ^{\mind}}$. Note that
             indeed we have\[
             \sum\lX^{\mind} \subset \sum(\mX_1^{\mind}\times\mX_2^{\mind})\subset\parent{\sum\mX_1^{\mind}}\times{(\sum\mX_2^{\mind}})
             \] The
      pair of set-theoretic injections lifts to the coproduct of predicates. Given,
      for all $\mind \in \IndexSet$, a logical relations morphism
      $\mmorph^{\mind}\of\mX^{\mind}\to\mY$,
      then the pair
      $\pair{\coprodmorphismseq[\mind\in\IndexSet]{\mmorph_1^{\mind}}}
            {\coprodmorphismseq[\mind\in\IndexSet]{\mmorph_2^{\mind}}}$
                 lifts to $\coprodmorphismseq[\mind\in\IndexSet]{\mmorph^{\mind}}$.
    \item \textbf{exponentials:}
      $\mY^{\mX} =
      \triple{\mY_1^{\mX_1}}{\mY_2^{\mX_2}}{\mPredr}$, where
      \[
      \mPredr = \set{\pair{\mmorph_1}{\mmorph_2} \in
        \mY_1^{\mX_1}\times \mY_2^{\mX_2} \suchthat \text{ for all
          $\pair{\mx_1}{\mx_2}$ in $\lX$, $\pair{\mmorph_1(\mx_1)}{\mmorph_2(\mx_2)} \in \lY$}}
      \]
      The pair $\pair\eval\eval$ lifts to the evaluation map in
      $\PredCat$, and for every logical relation morphism
      \(
      \mmorph \of
      \mZ\times \mX \to
      \mY
      \) the pair of functions
      $\pair{\ilam{\mX_1}{\mmorph_1}}{\ilam{\mX_2}{\mmorph_2}}$ lifts
      to $\ilam\mX\mmorph$.
  \end{itemize}
\end{proposition}

\begin{proof}%
  A vast generalisation of this result using bifibrations is discussed by
  Jacobs~\cite[Section~9.2]{jacobs:categorical-logic-and-type-theory}.
  Katsumata~\cite{katsumata:relating-computational-effects-by-TT-lifting-journal}
  spells out this structure for a more specialised situation, using
  faithful bifibrations, that
  includes our notion of logical relations.
\end{proof}

\Section{Monadic lifting}\sectionlabel{monadic lifting}
Our goal is to construct \emph{relational} \cbpv{} models, i.e., models in $\LogRel$, relating two
models in $\Set$. Such models are given by a pair of
monads. Straightforward calculation shows that if $\Monad_1$,
$\Monad_2$ are two (strong) monads over (cartesian) categories
$\ValCat_1$, $\ValCat_2$, then setting $\Monad\pair\mx\my$ to
$\pair{\Monad_1\mx}{\Monad_2\my}$ yields a monad over
$\ValCat_1\times\ValCat_2$, with the monadic structure given
componentwise, i.e. the unit by $\pair{\unit_1}{\unit_2}$ and the
multiplication by $\pair{\monmult_1}{\monmult_2}$.  The following
definition captures the data we will need in our logical relations
models.

\begin{definition}
  Let $\pair{\Monad_1}{\Monad_2}$ be a pair of (strong) monads
  over $\Set$. A \defterm{lifting} of $\Monad_1$, $\Monad_2$ to $\LogRel$ is a
  strong monad $\Monad$, such that:
  \begin{itemize}
  \item for every logical relation $\mX$, $\Monad\mX$ is a lifting of
    $\Monad_1\mX_1$ and $\Monad_2\mX_2$, and we write \( \Monad\mX =
    \triple{\Monad_1\mX_1}{\Monad_2\mX_2}{\RelMon\mX} \);
  \item for every logical relation morphism
    $\mmorph$,
    $\pair{\Monad_1\mmorph_1}{\Monad_2\mmorph_2}$ lifts to $\Monad\mmorph$;
  \item the monadic unit $\pair{\unit_1}{\unit_2}$ lifts to the unit
    of $\Monad$;
  \item the monadic multiplication $\pair{\monmult_1}{\monmult_2}$
    lifts to the multiplication of $\Monad$; and
  \item the monadic strength $\pair{\strength_1}{\strength_2}$ lifts
    to the strength of $\Monad$.
  \end{itemize}
\end{definition}
Note that, in order to lift a given pair of monads $\Monad_1$,
$\Monad_2$, the only additional structure required is the relation
part $\RelMon\triple{\mX_1}{\mX_2}\lX$ of the monad $\Monad$.  The
remainder of the monadic structure of the lifting is uniquely determined by the monadic
structure of $\Monad_1$ and $\Monad_2$, i.e., we only need to validate
that the existing structure satisfies these properties.

\begin{example}
  Every pair of monads $\Monad_1$, $\Monad_2$ admits a lifting via the
  total relation, i.e., by setting $\RelMon\triple{\mX_1}{\mX_2}\lX \definedby
  \Monad_1\mX_1\times\Monad_2\mX_2$.
\end{example}

The models, i.e. monads, Benton et al.~\cite{benton-kennedy:monads-effects-and-transformations,
  benton-kennedy-hofmann-beringer:reading-writing-and-relations,
  benton-buchlovsky:semantics-of-an-effect-analysis-for-exceptions,
  benton-kennedy-beringer-hofmann:transformations-with-dynamic-allocation,
  benton-kennedy-beringer-hofmann:transformations-ho-store} use to validate
effect-dependent transformations are lifted models. Due to time
and space constraints, we do not describe these models here
explicitly.

\begin{lemma}
  Let $\Monad$ be a lifting of $\Monad_1$,$\Monad_2$. Let $\Algebra_1$,
  $\Algebra_2$ be algebras for $\Monad_1$, $\Monad_2$, respectively,
  and $\Algebra$
  a lifting of the algebra structure, i.e., a predicate
  $\lAlgebra \subset
  \carrier{\Algebra_1}\times\carrier{\Algebra_2}$ such that the
  pair of algebra maps
  $\pair{\algebra[\Algebra_1][\placeholder]}{\algebra[\Algebra_2][\placeholder]}$
  lifts.  Thus, such a $\Algebra$ is an algebra for $\Monad$.

  \noindent
  Further, for all logical relations morphisms $\mmorph \of \mX \times \mY
  \to \carrier\Algebra$, the pair of monadic liftings
  $\pair{\lifting{\mmorph_1}}{\lifting{\mmorph_2}}$ lifts to the
  monadic lifting $\lifting\mmorph \of \mX
  \times \Monad\mY \to \carrier\Algebra$.
\end{lemma}
\begin{proof}%
  As $\lifting\mmorph$ is expressed using
  $\ilam\placeholder\placeholder$, $\Monad$, and the tupling
  morphism, the monadic lifting also lifts to $\LogRel$.
\end{proof}

We define the lifting of other concepts, such as generic
effects, monad morphisms, and algebraic operations similarly. Let $\Ar$, $\Pa$
be logical relations. Let $\mgen_1 \of \arity{\Ar_1}{\Pa_1}$,
$\mgen_2\of\arity{\Ar_2}{\Pa_2}$ be generic effects for the monads
$\Monad_1$, $\Monad_2$, respectively. We say the pair
$\pair{\mgen_1}{\mgen_2}$ lifts to a generic operation of type
$\arity\Ar\Pa$ for $\Monad$ when the pair lifts as a function $\Pa \to
\Monad\Ar$.

Similarly, let $\mop_i$ be two algebraic operations of types
$\arity{\Ar_i}{\Pa_i}$ for $\Monad_i$, $i = 1,2$. The pair $\pair
{\mop_1}{\mop_2}$ lifts when, for every $\Monad$-algebra $\Algebra$,
the components $\pair{\mop_1^{\Algebra_1}}{\mop_2^{\Algebra_2}}$
lift.
%
Let $\Monad$, $\Monadv$ be liftings of $\Monad_1$, $\Monad_2$, and
$\Monadv_1$, $\Monadv_2$,
respectively. A pair of monad morphism $\MonadMorphism_i \of \Monad_i
\to \Monadv_i$, $i = 1,2$ lifts when each component
$\pair{\MonadMorphism_1}{\MonadMorphism_2}$ lifts to a morphism of logical
relations $\MonadMorphism_{\mX} \of \Monad\mX \to \Monadv\mX$.

Let $\Opset$ be a set of operations. Let $\arities_1$, $\arities_2$ be
set-theoretic type assignments for $\Opset$. A lifting of
$\arities_1$,$\arities_2$ is a type assignment $\arities$ for $\Opset$
in $\LogRel$, such that, for every $\mop \in \Opset$, if $\arities$
assigns $\mop \of \arity\Ar\Pa$, then $\arities_i$ assigns $\mop \of
\arity{\Ar_i}{\Pa_i}$, for $i = 1,2$.  In the following, we are only
concerned with such type assignment liftings which assign the pair of
diagonal relations for every operation.
%
Given two
set-theoretic \cbpv{} $\Opset$-models
\[
\seq{\Set, \Monad_1, \arities_1, \opsem[1]\placeholder}, \qquad
\seq{\Set, \Monad_2, \arities_2, \opsem[2]\placeholder}
\]
a {lifting} of these models is a \cbpv{} $\Opset$-model
\[
\seq{\LogRel, \Monad, \arities, \opsem[]\placeholder}
\] such that $\Monad$ is a lifting of the given monads,
$\arities$ is a lifting of the type assignments, and, for every $\mop$
in $\Opset$, $\opsem[]\mop$ is a lifting of $\opsem[1]\mop$, $\opsem[1]\mop$.
Our goal is to lift a given pair of set-theoretic \cbpv{}
$\Opset$-models to such a relational model. In order to present our construction we
require the following auxiliary notion.

\begin{definition}
Let $\Monad_1$, $\Monad_2$ be monads over $\Set$, let $\mX$ be a logical
relation, and let ${\mPredr \subset \Monad_1\mX_1\times\Monad_2\mX_2}$ be a
relation.
\begin{itemize}
\item We say that \defterm{the monadic unit respects $\mPredr$  at
  $\mX$} if $\unit_1\times\unit_2[\lX] \subset \mPredr$.
\item Let $\Ar$, $\Pa$ be logical relations and $\mop_1 \of \arity{\Ar_1}{\Pa_1}$, $\mop_2\of{\Ar_2}{\Pa_2}$ be
  algebraic operations for $\Monad_1$, $\Monad_2$.  We say that
  \defterm{the operations $\pair{\mop_1}{\mop_2}$ respect $\mPredr$
  at $\mX$ under $\pair\Ar\Pa$} when
  $\pair{\mop_1^{\F\mX_1}}{\mop_2^{\F\mX_2}}$ lifts to a logical
  relation morphism:
  \[
  \mop^{\F\mX} \of \triple{\Monad_1\mX_1}{\Monad_2\mX_2}{\mPredr}^{\Ar} \to \triple{\Monad_1\mX_1}{\Monad_2\mX_2}{\mPredr}^{\Pa}
  \]
  Explicitly, this condition holds when, for every
  $\pair{\mparcomp_1}{\mparcomp_2} \in
  (\Monad_1\mX_1)^{\Ar_1}\times(\Monad_2\mX_2)^{\Ar_2}$, for which
  $\pair{\mar_1}{\mar_2} \in \lAr$ implies
  $\pair{\mparcomp_1(\mar_1)}{\mparcomp_2(\mar_2)} \in \mPredr$, we
  have, for every pair $\pair{\mpa_1}{\mpa_2}\in\lPa$
  \[
  \pair{\mop_1(\mparcomp)(\mpa_1)}{\mop_2(\mparcomp_2)(\mpa_2)} \in
  \mPredr
  \]
\end{itemize}
\end{definition}

We present the central construction of this chapter:
\begin{theorem}\theoremlabel{lifting construction}
  Let
  $\Opset$ be a set of operations. Consider any two
  set-theoretic \cbpv{} $\Opset$-models
  \[
  \seq{\Set, \Monad_1, \arities_1, \opsem[1]\placeholder}, \qquad
  \seq{\Set, \Monad_2, \arities_2, \opsem[2]\placeholder}
  \]
  Let $\arities$ be a lifting of $\arities_1$, $\arities_2$.

  For every logical relation $\mX$, set
  $\Monad\mX \definedby \triple{\Monad_1\mX_1}{\Monad_2\mX_2}{\Intersect\RelFam\mX}$,
  where $\RelFam\mX$ is the set of all relations $\mPredr \subset
  \Monad_1\mX_1\times\Monad_2\mX_2$ such that:
  \begin{itemize}
  \item the monadic unit respects $\mPredr$; and
  \item for every $\mop \in \Opset$, $\mop \of \arity\Ar\Pa$ via
    $\arities$, the operations $\pair{\mop_1}{\mop_2}$ respect
    $\mPredr$ at $\mX$ under $\pair\Ar\Pa$.
  \end{itemize}
  Then:
  \begin{itemize}
  \item $\Monad$ is a lifting of $\Monad_1$, $\Monad_2$;
  \item for every $\mop \in \Opset$,
    $\pair{\opsem[1]{\mop_1}}{\opsem[2]{\mop_2}}$ lift to an operation
    $\opsem[]{\mop} \of \arity\Ar\Pa$ for $\Monad$;
  \end{itemize}
  Thus, $\seq{\LogRel, \Monad, \arities, \opsem[]\placeholder}$ is
  a lifting of the two given models to $\arities$. In addition,
  \begin{itemize}
  \item for every other lifting
    \[
    \seq{\LogRel, \Monadv, \arities, \opsemv[]\placeholder}
    \]
    of the two given models with the same type assignment lifting,
    there is a (necessarily unique) monad morphism between the corresponding free liftings:
    \[
    \triple\id\id{\MonadMorphism} \of \Monad \to \Monadv
    \]
    preserving the operations in $\Opset$.
  \end{itemize}

  We call $\Monad$ the \defterm{free lifting of $\Monad_1$ and $\Monad_2$ via
    $\arities$}, and the resulting \cbpv{} $\Opset$-model the
  \defterm{free lifting model}.
\end{theorem}

\begin{proof}%
  We proceed as follows. First, we show that for every logical
  relation $\mX$, $\Intersect\RelFam\mX \in \RelFam\mX$. Next, we show
  that the action of $\Monad$ on morphisms lifts. Thus $\Monad$ is
  indeed an endofunctor over $\LogRel$. We then show the monadic unit,
  multiplication and strength lift to $\Monad$. Thus, $\Monad$ is a
  strong monad. Next, we show the operations lift, and obtain a
  lifting of the \cbpv{} models. Finally, we show that this model is
  free.

  Consider any logical relation $\mX$, and set $\mPredr \definedby
  \Intersect\RelFam\mX$.

  Consider any $\mPredr' \in \RelFam\mX$. As the unit respects
  $\mPredr'$, $\unit_1\times\unit_2[\lX]\subset \mPredr'$. Therefore
  \[
  \unit_1\times\unit_2[\lX] \subset \Intersect\RelFam\mX = \mPredr
  \]
  i.e., the unit respects $\mPredr$.

  Consider any $\mop \in \Opset$, $\mop \of \arity\Ar\Pa$. Consider any
  $\pair{\mparcomp_1}{\mparcomp_2} \in
  (\Monad_1\mX_1)^{\Ar_1}\times(\Monad_2\mX_2)^{\Ar_2}$ satisfying,
  for every $\pair{\mar_1}{\mar_2} \in \lAr$,
  $\pair{\mparcomp(\mar_1)}{\mparcomp_2(\mar_2)} \in \mPredr$. Consider any
  $\pair{\mpa_1}{\mpa_2}\in \lPa$.

  Consider any $\mPredr'\in\RelFam\mX$. For every
  $\pair{\mar_1}{\mar_2} \in \lAr$, we have:
  \[
  \pair{\mparcomp_1(\mar_1)}{\mparcomp_2(\mar_2)} \in \mPredr \subset \mPredr'
  \]
  As $\mop$ respects $\mPredr'$, we deduce that
  \[
  \pair{\opsem[1]{\mop}(\mparcomp_1)(\mpa_1)}{\opsem[2]{\mop}(\mparcomp_2)(\mpa_2)}
  \in \mPredr'
  \]
  As we considered an arbitrary $\mPredr'\in\RelFam\mX$, we deduce
  that:
  \[
  \pair{\opsem[1]{\mop}(\mparcomp_1)(\mpa_1)}{\opsem[2]{\mop}(\mparcomp_2)(\mpa_2)}
  \in \Intersect\RelFam\mX = \mPredr
  \]
  and $\mop$ respects $\mPredr$. We showed thus that both the unit and
  operations respect $\mPredr$, i.e., $\mPredr$ is in $\RelFam\mX$.

  Next, consider any predicate morphism
  $\mmorph = \triple{\mmorph_1}{\mmorph_2}\lmorph \of \mX \to \mY$. Denote
  $\mPredr \definedby \Intersect\RelFam\mX$, $\mPreds \definedby
  \Intersect\RelFam\mY$.
  Set $\mPredr' \definedby
  \inv*{\Monad_1\mmorph_1\times\Monad_2\mmorph_2}[\mPreds]$. Then
  $\mPredr' \in \RelFam\mX$.

  The the unit respects relation $\mPredr'$. Indeed,
  \begin{align*}
  \Monad_1\mmorph_1\times\Monad_2\mmorph_2[\unit_1\times\unit_2[\lX]]
  &=
  (\Monad_1\mmorph_1\compose\unit_1)\times(\Monad_2\mmorph_2\compose\unit_2)[\lX]
  \\&
  \explain={\NaturalityExp{\unit_i}}
  (\unit_1\compose\mmorph_1)\times(\unit_2\compose\mmorph_2)[\lX]
  \explain\subset{$\mmorph \of \mX\to\mY$}
 \unit_1\times\unit_2[\lY]
  \explain\subset{$\mPreds \in \Intersect\RelFam\mY$}
  \mPreds
  \end{align*}
  Therefore
  \[
  \unit_1\times\unit_2[\lX] \subset
  \inv*{\Monad_1\mmorph_1\times\Monad_2\mmorph_2}[\mPreds] = \mPredr'
  \]
  and the unit respects $\mPredr'$.

  Consider any $\mop \in \Opset$, $\mop \of \arity\Ar\Pa$. Then $\mop$ respects the
  relation $\mPredr'$. Indeed, consider any
  $\pair{\mparcomp_1}{\mparcomp_2} \in
  (\Monad_1\mX_1)^{\Ar_1}\times(\Monad_2\mX_2)^{\Ar_2}$ satisfying,
  for every $\pair{\mar_1}{\mar_2} \in \lAr$,
  $\pair{\mparcomp(\mar_1)}{\mparcomp_2(\mar_2)} \in
  \mPredr'$, i.e.,
  \[
  \pair{\Monad_1\mmorph_1(\mparcomp_1(\mar_1))}{\Monad_2\mmorph_2(\mparcomp_2(\mar_2))}
  \in \mPreds
  \]
  Consider any $\pair{\mpa_1}{\mpa_2}\in \lPa$. As $\mPreds$ respects
  $\mop$, we have
  \[
  \pair{\opsem[1]\mop\parent{\vphantom{\sum}\lam{\mar_1}{\Monad_1\mmorph_1(\mparcomp_1(\mar_1))}}(\mpa_1)}
       {\opsem[2]\mop\parent{\vphantom{\sum}\lam{\mar_2}{\Monad_2\mmorph_2(\mparcomp_2(\mar_2))}}(\mpa_2)}
       \in \mPreds
  \]
  Therefore
  \begin{align*}
    \Monad_1\mmorph_1\times\Monad_2\mmorph_2&(\pair{\opsem[1]\mop(\mparcomp_1)(\mpa_1)}
                                                 {\opsem[1]\mop(\mparcomp_1)(\mpa_1)})
    \\&=
    \pair{\Monad_1\mmorph_1(\opsem[1]\mop(\mparcomp_1)(\mpa_1))}
         {\Monad_2\mmorph_2(\opsem[2]\mop(\mparcomp_2)(\mpa_2))}
    \\&\explain={\NaturalityExp{\opsem[i]\mop} (see
      \exampleref{initial sig-theory})}
    \pair{\opsem[1]\mop\!\parent{\vphantom{\sum}\lam{\mar_1}{\Monad_1\mmorph_1(\mparcomp_1(\mar_1))}}\!(\mpa_1)}
         {\opsem[2]\mop\!\parent{\vphantom{\sum}\lam{\mar_2}{\Monad_2\mmorph_2(\mparcomp_2(\mar_2))}}\!(\mpa_2)}
    \in \mPreds
  \end{align*}
  Hence,
  \[
  \pair{\opsem[1]\mop(\mparcomp_1)(\mpa_1)}
       {\opsem[1]\mop(\mparcomp_1)(\mpa_1)}
       \in
       \inv*{\Monad_1\mmorph_1\times\Monad_2\mmorph_2}[\mPreds] = \mPredr'
  \]
  and thus $\mop$ respects $\mPredr'$.

  We showed that the unit and the operations respect $\mPredr'$, hence
  $\mPredr' \in \RelFam\mX$, and thus $\mPredr \subset
  \mPredr$. Therefore
  \[
  \Monad_1\mmorph_1\times\Monad_2\mmorph_2[\mPredr]
  \subset
  \Monad_1\mmorph_1\times\Monad_2\mmorph_2[\mPredr']
  \subset
  \mPreds
  \]
  Thus, $\pair{\Monad_1\mmorph_1}{\Monad_2\mmorph_2}$ lifts. We
  therefore have an endofunctor $\Monad$ over $\LogRel$.

  The monadic unit lifts, as the unit respects $\Intersect\RelFam\mX$.
  The monadic multiplication also lifts. Indeed, consider any logical
  relation $\mX$.  Denote $\mPredr \definedby \Intersect\RelFam\mX$,
  $\mPreds \definedby \Intersect\RelFam\Monad\mX$.  Set $\mPreds'
  \definedby \inv*{\monmult_1\times\monmult_2}[\mPredr]$. Then
  $\mPreds' \in \RelFam\Monad\mX$.

  Indeed,
  \[
  \monmult_1\times\monmult_2[\unit_1\times\unit_2[\mPredr]]
  \explain={\MonadLawExp}
  \id\times\id{}[\mPredr] = \mPredr
  \]
  Therefore, $\unit_1\times\unit_2[\mPredr] \subset \mPreds'$, and the
  unit respects $\mPreds'$.  Consider any $\mop \in \Opset$, $\mop \of
  \arity\Ar\Pa$. Then $\mop$ respects the relation $\mPreds'$. Indeed,
  consider any $\pair{\mparcomp_1}{\mparcomp_2} \in
  (\Monad_1\mX_1)^{\Ar_1}\times(\Monad_2\mX_2)^{\Ar_2}$ satisfying,
  for every $\pair{\mar_1}{\mar_2} \in \lAr$,
  $\pair{\mparcomp(\mar_1)}{\mparcomp_2(\mar_2)} \in \mPreds'$, i.e.,
  \( \pair{\monmult_1(\mparcomp_1(\mar_1))}
     {\monmult_2(\mparcomp_2(\mar_2))}\) is in \(\mPredr \).  Consider any
     $\pair{\mpa_1}{\mpa_2}\in \lPa$. As $\mop$ respects $\mPredr$, we
     have
  \[
  \pair{\opsem[1]\mop(\monmult_1\compose \mparcomp_1)(\mpa_1)}
       {\opsem[2]\mop(\monmult_2\compose \mparcomp_2)(\mpa_2)}
       \in \mPredr
  \]
  Therefore,
  \begin{multline*}
    \monmult_1\times\monmult_2(\pair
                                   {\opsem[1]\mop(\mparcomp_1)(\mpa_1)}
                                   {\opsem[2]\mop(\mparcomp_2)(\mpa_2)})
    \\
    \begin{aligned}[t]
     &=\pair{\monmult_1(\opsem[1]\mop(\mparcomp_1)(\mpa_1))}
         {\monmult_2(\opsem[2]\mop(\mparcomp_2)(\mpa_2))}
    \\&\explain={see \exampleref{initial sig-theory}}
  \pair{\opsem[1]\mop(\monmult_1\compose \mparcomp_1)(\mpa_1)}
       {\opsem[2]\mop(\monmult_2\compose \mparcomp_2)(\mpa_2)}
       \in \mPredr
       \end{aligned}
  \end{multline*}
  and thus $\mop$ respects $\mPreds'$. We showed the unit and the
  operations respect $\mPreds'$, hence $\mPreds' \in
  \RelFam\Monad\mX$. Consequently, $\monmult$ lifts.

  Consider any logical relations $\mX$, $\mY$. From
  Kock~\cite{kock:strong-functors-and-monoidal-monads} follows that,
  for all $\pair{\mx_i}{\mcomp_i}\in\mX_i\times\Monad_i\mY_i$,
  $\strength_i(\mx_i, \mcomp_i) =
  \Monad_i(\lam{\my_i}{\pair{\mx_i}{\my_i}})(\mcomp_i)$.  As the
  strengths are expressed using the cartesian closed structure and the
  action of $\Monad_i$ on morphisms, the strengths also
  lift.

  Explicitly, consider any
  $\pair{\pair{\mx_1}{\mcomp_1}}{\pair{\mx_2}{\mcomp_2}} \in
  \mX\lltimes\Monad\mY$.  Consider any $\pair{\my_1}{\my_2}
  \in \lY$. Then, $\pair{\pair{\mx_1}{\my_1}}{\pair{\mx_2}{\my_2}} \in
  \mX\lltimes\mY$. Therefore,
  $\pair{\lam{\my_1}{\pair{\mx_1}{\my_1}}}{\lam{\my_2}{\pair{\mx_2}{\my_2}}}
  $ lifts, hence by applying the lifted monad $\Monad$ we deduce that
  \[
  \pair{\Monad_1(\lam{\my_1}{\pair{\mx_1}{\my_1}})}{\Monad_2(\lam{\my_2}{\pair{\mx_2}{\my_2}})}
  \]
  lifts. As $\pair{\mcomp_1}{\mcomp_2}\in \Intersect\RelFam\mY$, we
  deduce that $\pair{\strength_1(\mx_1, \mcomp_1)}{\strength_2(\mx_2,
    \mcomp_2)} \in \Intersect\RelFam(\mX\times\mY)$, and the monadic
  strengths lift.

  Every operation in $\Opset$ lifts. Indeed, consider any $\mop \in
  \Opset$, $\mop \of \arity\Ar\Pa$. For every logical relation $\mX$,
  as $\opsem[]\mop$ respects $\Intersect\RelFam\mX$, we deduce that
   $\opsem[]\mop$ lifts at the component $\F\mX$. Recall that all
  components of an algebraic operation $\mop \of \arity{\Ar_i}{\Pa_i}$
  can be expressed in terms of
  the component $\mop_{\F\Ar_i}$, the cartesian closed structure, and
  the strong monadic structure (see the proof of
  \corollaryref{operation-determined-by-free-component} and
  \theoremref{operations-vs-effects}).  We have just shown all these
  structures lift to logical relations, therefore all components of
  the interpretation of $\mop$ lift. Thus, all operations in $\Opset$
  lift.

  Finally, let $\seq{\LogRel, \Monadv, \arities,
    \opsemv[]\placeholder}$ be any other lifting. Then $\pair\id\id$
  lifts to a monad morphism from $\Monad$ to $\Monadv$. Indeed,
  consider any logical relation $\mX$, and denote $\Monadv\mX =
  \triple{\Monad_1\mX_1}{\Monad_2\mX_2}{\mPredr}$. Because $\Monadv$
  is a lifting, the monadic unit lifts, hence the unit respects
  $\mPredr$.  Similarly, because $\opsemv[]\placeholder$ is a lifting,
  all the operations in $\Opset$ respect $\mPredr$. Therefore,
  $\mPredr \in \RelFam\mX$, hence $\Intersect\RelFam\mX \subset
  \mPredr$. Therefore the pair of identities lift to a morphism
  $\Monad\mX \to \Monadv\mX$. Thus $\seq{\LogRel, \Monad, \arities,
    \opsem[]\placeholder}$ is the free lifting.
\end{proof}

Our construction also extends to monad morphisms:
\begin{theorem}\theoremlabel{op preserving morphisms lift}
  Let $\Opset$ be a set of operations. Consider any four set-theoretic
  \cbpv{}
  $\Opset$-models:
  \begin{align*}
  \seq{\Set, \Monad_1, \arities_1, \opsem[1]\placeholder},&
  \seq{\Set, \Monad_2, \arities_2, \opsem[2]\placeholder},\\
  \seq{\Set, \Monadv_1, \arities_1, \opsemv[1]\placeholder},&
  \seq{\Set, \Monadv_2, \arities_2, \opsemv[2]\placeholder}
  \end{align*}
  Let $\arities$ be a lifting of $\arities_1$,$\arities_2$.
  Every pair of monad morphisms $\MonadMorphism_1 \of \Monad_1 \to \Monadv_1$, $\MonadMorphism_2 \of
  \Monad_2 \to \Monadv_2$ that preserve the
  operations in $\Opset$ lifts to a monad morphism
  \[
  \triple{\MonadMorphism_1}{\MonadMorphism_2}{\MonadMorphism} \of
  \Monad \to \Monadv
  \]
  As a consequence, this monad morphism preserves the lifted
  operations.
\end{theorem}

\begin{proof}%
  The proof amounts to showing that each component of the pair of monad
  morphisms lifts.  We proceed along the same lines of the
  previous proof. Consider any logical relation $\mX$, and denote
  $\mPredr \definedby
  \inv*{\MonadMorphism_1\times\MonadMorphism_2}[\Intersect\RelFam'\mX]$,
  where $\RelFam'\mX$ is the relation component of $\Monadv\mX$.  The
  preservation of units under monad morphisms implies the monadic unit respects $\mPredr$.
  The assumption that the monad
  morphisms preserves the operations implies the operations in $\Opset$ respect $\mPredr$.  Thus, $\mPredr \in
  \RelFam\mX$, and
  $\pair{\MonadMorphism_1}{\MonadMorphism_2}$ lifts.%
\end{proof}

Before we conclude our discussion of set-theoretic lifting, we
investigate its action on diagonal relations, i.e., logical relations
of the form $\triple\mX\mX=$.
\begin{lemma}
  Let $\Opset$ be a set of operations. Consider any two \cbpv{}
  $\Opset$-models with the same type assignment:
  \[
  \seq{\Set, \Monad_1, \arities, \opsem[1][]\placeholder},
  \seq{\Set, \Monad_2, \arities, \opsem[2][]\placeholder}
  \]
  Let $\MonadMorphism \of \Monad_1 \to \Monad_2$ be a monad morphism
  preserving the operations in $\Opset$.

  Denote by $\arities$ the lifting of $\arities$,$\arities$,
  assigning to each operation the pair of diagonal relations of its
  type assignment via $\arities$, i.e., if $\arities(\mop) =
  \pair\Ar\Pa$, then $\arities(\mop) = \pair{\triple\Ar\Ar=}{\triple\Pa\Pa=}$.  Denote by $\Monad_{\Opset}$ the free
  monad for the signature $\pair{\Opset}{\arities}$. Denote by
  $\mepi \of \Monad_{\Opset} \to \Monad_1$ the (unique) monad morphism
  preserving $\Opset$.

  For every set $\mX$, there exists a (unique) function $\mmorph \of
  \Monad_{\Opset}\mX \to \Intersect\RelFam\triple\mX\mX=$ satisfying
  \inlinediagram{diagonal-lifting-lemma-01}
\end{lemma}

\begin{proof}%
  We use the inductive description of $\Monad_{\Opset}$ as the term algebra for the signature induced by $\pair\Opset\arities$.
  We construct $\mmorph$ by induction, essentially as
  $\prodmorphism{\id}{\MonadMorphism}\compose\mmorphv$. Because
  the monadic unit respects $\RelMon\mX$ that preserves the
  operations in $\Opset$, $\mmorph$ is well-defined. We then prove by
  induction on $\Monad_{\Opset}\mX$ that the square commutes for all
  $\mcomp \in \Monad_{\Opset}\mX$. Uniqueness of $\mmorph$ follows as
  inclusions are monic.
\end{proof}

We can now calculate the explicit description of the action of a class
of free lifting on diagonal relations:
\begin{theorem}\theoremlabel{monad morphism simulation}
  Let $\Opset$ be a set of operations, $\Monad_2$ be a finitary monad,
  and
  \[
  \seq{\Set, \Monad_2, \arities, \opsem[2]\placeholder}
  \] be a \cbpv{} $\Opset$-model. Let $\Monad_{\Opset}$ be the free
  monad for the signature $\pair\Opset\arities$, and denote by $\Monad_{\Opset}
  \xepimor{\mepi}\Monad_1\xmonomor{\mmono}\Monad_2$ the conservative
  restriction factorisation corresponding to the surjection-injection
  factorisation of $\Set$, giving rise to the \cbpv{} $\Opset$-model
  \[
  \seq{\Set, \Monad_1, \arities, \opsem[1]\placeholder}
  \]
  Let $\arities$ be the diagonal lifting of $\arities$, and $\Monad$
  be the free lifting arising from $\arities$.

  For every set $\mX$,
  \[
  \RelMon\triple\mX\mX=
  =
  \prodmorphism\id\mmono[\Monad_1\mX]
  =
  \set{\pair{\mcomp}{\mmono(\mcomp)}
  \suchthat{\mcomp \in \Monad_1\mX}}
  \]
\end{theorem}

\begin{proof}%
  Consider any set $\mX$. Denote $\mPredr \definedby
  \RelMon\triple\mX\mX=$, $\mPreds \definedby
  \prodmorphism\id\MonadMorphism[\Monad_1\mX]$. We show that $\mPredr
  = \mPreds$.
   First, note that the unit respects $\mPreds \subset
  \Monad_1\mX\times\Monad_2\mX$ by the definition of monad morphisms,
  and the operations respect $\mPreds$ by the definition of
  preservation of operations by monad morphisms. Therefore, by
  definition, $\mPredr \subset\mPreds$.

  For the converse inclusion, recall that the $\Epi$-morphisms in the
  factorisation system of finitary monads arising from the injection-surjection
  factorisation of $\Set$ are componentwise surjective, \corollaryref{epi are epi}.  Therefore, by the previous lemma, we have a
  function $\mmorph \of \Monad_{\Opset}\mX \to \mPredr$, satisfying
  \inlinediagram{diagonal-lifting-lemma-02}
  Therefore, there exists a unique fill-in diagonal
  \inlinediagram{diagonal-lifting-lemma-03}
  Chasing the lower-right triangle shows that, for all $\mcomp \in
  \Monad_1\mX$, $\pair\mcomp{\mmono(\mcomp)} = \mmorphw(\mcomp) \in
  \mPredr$. Thus, $\mPreds  \subset \mPredr$.
\end{proof}

We employ Theorems~\theoremref*{lifting construction}, \theoremref*{op preserving morphisms lift}, and~\theoremref*{monad morphism simulation} to relate the
conservative restriction models and the benchmark models. Consider any
two $\Signature$-models
\[
\mModel_1 = \seq{\Set, \arities_1, \Presheaf_1, \opsem[\placeholder][1]\placeholder},
\qquad \mModel_2 = \seq{\Set, \arities_2, \Presheaf_2, \opsem[\placeholder][2]\placeholder},
\]
for some effect hierarchy $\Signature$. A lifting of $\mModel_1$,
$\mModel_2$ is a $\Signature$-model
\[
\mModel = \seq{\LogRel, \arities, \Presheaf, \opsem[\placeholder]\placeholder}
\]
where:
\begin{itemize}
\item $\arities$ is a lifting of $\arities_1$, $\arities_2$;
\item for every $\e \in \E$, $\Presheaf\e$ is a lifting of
  $\Presheaf_1\e$, $\Presheaf_2\e$;
\item for every $\e\subset \e'$ in $\E$, $\Presheaf(\e\subset\e')$ is
  a lifting of   $\Presheaf_1(\e\subset\e')$,
  $\Presheaf_2(\e\subset\e')$; and
\item for every $\e \in \E$ and $\mop \in \e$, $\opsem\mop$ is a
  lifting of $\opsem[\e][1]\placeholder$,$\opsem[\e][2]\placeholder$.
\end{itemize}

Note that in order to lift two $\Signature$-models, the only
additional structure we require is the lifting of the type assignments
and the lifting of each monad in the hierarchy. The other conditions
are properties that need to be verified.

Using this terminology, we obtain the following corollary:
\begin{corollary}\corollarylabel{free lifting}
  Let $\Signature$ be an effect hierarchy, and $\mModel$ an algebraic
  \cbpv{} $\Opset$-model. Denote by $\arities$ the diagonal lifting
  of the type assignment of $\mModel$. Consider the benchmark model
  (see \exampleref{benchmark model})
  \[
  \benchmark\mModel = \seq{\Set, \arities, \benchmark\Presheaf, \opsem[\placeholder][\benchmarksymbol]\placeholder}
  \]
  and the conservative restriction model (see \theoremref{categorical
  conservative restriction})
  \[
  \conservative\mModel = \seq{\Set, \arities, \conservative\Presheaf, \opsem[\placeholder][\conservativesymbol]\placeholder}
  \]
  The \defterm{conservative comparison relational model} $\mModel$ is
  given by
  \[
  \mModel = \seq{\LogRel, \arities, \Presheaf, \opsem[\placeholder]\placeholder}
  \]
  where for every $\e \in \E$, $\seq{\LogRel,\Presheaf\e, \arities, \opsem\placeholder}$ is the free lifting of
    the two \cbpv{} $\Opset$-models $\seq{\Set, \conservative\Presheaf\e, \arities,
      \opsem[\e][\conservativesymbol]\placeholder}$ and $\seq{\Set, \benchmark\Presheaf\e,
      \arities, \opsem[\e][\benchmarksymbol]\placeholder}$.
  Moreover, for every set $\mX$, we have
  \[
  \Presheaf\e\triple\mX\mX= =
  \triple{\conservative\Presheaf\e\mX}{\benchmark\Presheaf\e\mX}{\pair{\id}{\mmono_{\e}^{\mX}}[\conservative\Presheaf\e\mX]}
  \]
  where $\mmono_{\e}^{\mX} \of \conservative\Presheaf\e\mX \monomor
  \Monad\mX = \benchmark\Presheaf\e\mX$ is the injection given in the
  definition of the conservative restriction model.
\end{corollary}

%%\todo{Domain-theoretic logical relations.}

%%\todo{Continuous lifting}

We defined the category of set-theoretic logical relations models and
presented the free lifting construction, culminating in our central
result, \corollaryref{free lifting}.