\section{Gradual Typing Syntax}
\newcommand{\dynof}[1]{\textrm{dyn}(#1)}
\begin{theorem}
For every $A$, there is a derivation $\dynof A : A \ltdyn D$
\end{theorem}
\begin{proof}
By induction on $A$:
\begin{enumerate}
\item $A = \dyn$, then $r(\dyn) : \dyn \ltdyn \dyn$
\item $A = \nat$, then $\inat : \nat \ltdyn \dyn$
\item $A = A_1 \ra A_2$ then $(\dynof {A_1} \ra \dynof {A_2})\iarr : A_1 \ra A_2 \ltdyn \dyn$
\item $A = A_1 \times A_2$ then $(\dynof {A_1} \times \dynof{A_2})\itimes : A_1 \times A_2 \ltdyn \dyn$
\end{enumerate}
\end{proof}
\begin{theorem}
For any two derivations $c,c' : A \ltdyn A'$ of the same precision
$c \equiv c'$
\end{theorem}
\begin{proof}
\begin{enumerate}
\item We show this by showing that derivations have a canonical
form.
The following presentation of precision derivations has unique derivations
\begin{mathpar}
\inferrule{}{\textrm{refl}(D) : D \ltdyn D}\and
\inferrule{}{\textsf{Inj}_{\text{nat}} : \nat \ltdyn D}\and
\inferrule{}{\textrm{refl}(\nat) : \nat \ltdyn \nat}\and
\inferrule{c : A_i \ra A_o \ltdyn D\ra D}{c(\textsf{Inj}_{\text{arr}}) : A_i \ra A_o \ltdyn \nat}\and
\inferrule{c : A_i \ltdyn A_i' \and d : A_o \ltdyn A_o'}{c \ra d : A_i \ra A_o \ltdyn A_i'\ra A_o'}
%% \inferrule{A_1 \times A_2 \ltdyn D\times D}{A_1 \times A_2 \ltdyn \nat}
%% \inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2'}{A_1 \times A_2 \ltdyn A_1'\times A_2'}
\end{mathpar}
Since it satisfies reflexivity, cut-elimination and congruence, it
is a model of the original theory. Since it is a sub-theory of the
original theory, it is equivalent.
\end{enumerate}
\end{proof}
Type precision is a binary relation on typed terms. The original
gradual guarantee rules are as follows:
\begin{mathpar}
\inferrule
{\Gamma^\ltdyn \vdash M \ltdyn M' : c \and
c : A \ltdyn A'\and
c' : A \ltdyn A_2'
}
{\Gamma^\ltdyn \vdash M \ltdyn (M :: A_2') : c'}
\inferrule
{\Gamma^\ltdyn \vdash M \ltdyn M' : c \and
c : A \ltdyn A'\and
c' : A_2 \ltdyn A'
}
{\Gamma^\ltdyn \vdash (M :: A_2) \ltdyn M' : c'}
\end{mathpar}
Where the cast $M :: A_2$ is defined to be
\[ \dnc {dyn(A_2)}{\upc {dyn(A)} M} \]
These two rules are admissible in our presentation.
For the first rule, we first prove that $\dnc {dyn(A_2)}\upc {dyn(A)} M = \dnc {c'}\upc{c} M$
\begin{align*}
\dnc {dyn(A_2)}\upc {dyn(A)} M
&= \dnc {(c \dynof {A'})}\upc{(c'\dynof{A'})} M \tag{All derivations are equal}\\
&= \dnc {c}\dnc {\dynof{A'}}\upc{\dynof{A'}}\upc{c'} M\tag{functoriality}\\
&= \dnc {c}\upc{c'} M\tag{retraction}\\
\end{align*}
Then the rest follows by the up/dn rules above and the fact that
precision derivations are all equal.
Thus the following properties are sufficient to provide an extensional
model of gradual typing without requiring transitivity of term
precision:
\begin{enumerate}
\item Every precision is representable in the above sense,
\item The association of casts to precision is functorial
\item Type constructors are covariant functorial with respect to
relational identity and composition
\end{enumerate}
\section{Call-by-push-value}
\subsection{Morphisms of CBPV Models}
There are two relevant notions of \emph{morphism} of CBPV models:
\emph{strict} and \emph{lax}.
% morphisms of CBPV models
Given call-by-push-value models
$\mathcal M_1 = (\mathcal V_1, \mathcal E_1, \arr_1, U_1, F_1)$ and
$\mathcal M_2 = (\mathcal V_2, \mathcal E_2, \arr_2, U_2, F_2)$,
A \emph{strict} morphism $G$ from $M_1$ to $M_2$ is given by a pair of functors
$G_{\mathcal{V}}: V_1 \to V_2$ and $G_{\mathcal{E}} : E_1 \to E_2$
that strictly presere the constructors:
\begin{enumerate}
\item $G_{\mathcal{E}} \circ F_1 = F_2 \circ G_{\mathcal{V}}$
\item $G_{\mathcal{V}} \circ U_1 = U_2 \circ G_{\mathcal{E}}$
\item $G_{\mathcal{E}}(A \arr_1 B) = G_{\mathcal{V}}(A) \arr_2 G_{\mathcal{E}}(B)$
\item $G_{\mathcal{V}}(A_1 \times_1 A_2) = G_{\mathcal{V}}(A_1) \times_2 G_{\mathcal{V}}(A_2)$
\item $G_{\mathcal{V}}(1_1) = 1_2$
\end{enumerate}
As well as strictly preserving the corresponding universal morphisms
and coherence isomorphisms.
A lax morphism instead preserves these only up to transformation
\begin{enumerate}
\item $G_{\mathcal{E}} \circ F_1 \Rightarrow F_2 \circ G_{\mathcal{V}}$
\item $G_{\mathcal{V}} \circ U_1 \Rightarrow U_2 \circ G_{\mathcal{E}}$
\item $G_{\mathcal{E}}(A \arr_1 B) \Rightarrow G_{\mathcal{V}}(A) \arr_2 G_{\mathcal{E}}(B)$
\item $G_{\mathcal{V}}(A_1 \times_1 A_2) \Rightarrow G_{\mathcal{V}}(A_1) \times_2 G_{\mathcal{V}}(A_2)$
\item $G_{\mathcal{V}}(1_1) \Rightarrow 1_2$
\end{enumerate}
Additionally a lax morphism should have a relationship between these
transformations and the universal morphisms, but we will only consider
lax morphisms of thin categories, where such conditions hold
trivially.
\subsection{Kleisli Actions of CBPV Type Constructors}
In CBPV models, all the type constructors are interpreted as functors:
\begin{enumerate}
\item $\to : \op\calV \times \calE \to \calE$
\item $\times : \calV \times \calV \to \calV$
\item $F : \calV \to \calE$
\item $U : \calE \to \calV$
\end{enumerate}
That is, they all have functorial actions on \emph{pure} morphisms of
value types and \emph{linear} morphisms of computation types.
%
We use these functorial actions extensively in the construction of
casts and their corresponding perturbations. But when defining
downcasts of value types and upcasts of computation types, we
additionally need a second functorial action of these categories:
functoriality in \emph{impure} morphisms of value types and
\emph{non-linear} morphisms of computation types. These notions of
morphism are given by the \emph{Kleisli} categories $\calVk$ and
$\calEk$ which have value types and computation types as objects but
morphisms are defined as
\[ \calVk(A,A') = \calE(F A, FA')\]
\[ \calEk(B,B') = \calV(U B, U B')\]
with composition given by composition in $\calE/\calV$. That is we
need to define a second functorial action, that agrees with the above
on objects for these Kleisli categories:
\begin{enumerate}
\item $\tok : \op\calVk \square \calEk \to \calEk$
\item $\timesk : \calVk \square \calVk \to \calVk$
\item $\Fk : \calVk \to \calEk$
\item $\Uk : \calEk \to \calVk$
\end{enumerate}
Note that rather than the product of categories we use the ``funny
tensor product'' $\square$. This is because the action on
impure/non-linear morphisms for $\tok/\timesk$ do not satisfy ``joint
functoriality'' but instead only ``separate functoriality'', meaning
we give rather than an action on morphisms in both categories
simultaneously instead an action on each argument categories morphisms
with the object in the other category fixed. The existence of these
functorial actions for $\tok$ and $\timesk$ is reliant on the
\emph{strength} of the adjunction. We describe them using the internal
language of CBPV in order to more easily verify their
existence/functoriality:
\begin{enumerate}
\item For $\tok$ we define for $\phi : \calE(F A,F A')$ and $B \in \calE$ the morphism $\phi \tok B : \calV(U(A' \to B),U(A\to B))$ as
\[ t:U(A'\to B) \vdash \phi \tok B = \{ \lambda x. x' \leftarrow \phi\,[\ret x]; ! t x'\} : U(A \to B) \]
and for $A \in \calV$ and $f : \calV(UB,UB')$ we define $A \tok f : \calV(U(A \to B),U(A\to B'))$ as
\[ t : U(A \to B) \vdash A \tok f = \{ \lambda x. !f[\{ ! t x \}]\} \]
\item For $\timesk$ we define for $\phi : \calE(F A_1,FA_2)$ and $A' \in \calV$ the morphism $\phi \timesk A_2$ as
\[ \bullet : F(A_1\times A_2) \vdash \phi \timesk A_2 = (x_1,x_2) \leftarrow \bullet; x_1' \leftarrow \phi[\ret x_1]; \ret (x_1',x_2) : F(A_1'\times A_2)\]
and $A_1 \timesk \phi$ is defined symmetrically.
\item For $\Uk$ we need to define for $f : \calV(UB,UB')$ a morphism $\Uk f : \calE(FUB,FUB')$. This is simply given by the functorial action of $F$: $\Uk f = F(f)$
\item Similarly $\Fk \phi = U\phi$
\end{enumerate}
Functoriality in each argument is easily established, meaning for
example for the function type is functorial in each argument:
\begin{enumerate}
\item $(\phi \circ \phi') \tok B = (\phi' \tok B) \circ (\phi \tok B)$
\item $\id \tok B = \id$
\item $A \tok (f \circ f') = (A \tok f) \circ (A \tok f)$
\item $A \tok \id = \id$
\end{enumerate}
Finally, note that all of these constructions lift to squares in a
double CBPV model since the squares themselves form a CBPV model and
the projection functions preserve CBPV structure. For instance, given a square
$\alpha : \phi \ltdyn_{F c_o}^{F c_i} \phi'$ and a horizontal morphism $d : B \rel B'$ of appropriate type, we get a square
\[ \alpha \tok d : \phi \tok B \ltdyn_{U(c_o \to d)}^{U(c_i \to d)} \phi' \tok B' \]
\section{Details of the Construction of an Extensional Model}
In Section \ref{sec:extensional-model-construction}, we outline the construction
of an extensional model of gradual typing starting from a step-1 intensional model.
In this section, we provide the details for each of the constructions mentioned there.
\subsection{Constructing a Model with Perturbations}
The goal of this section is to prove the following lemma:
\begin{lemma}\label{lem:step-1-model-to-step-2-model}
Let $\mathcal M$ be a \hyperref[def:step-1-model]{step-1 intensional model}.
Then we can construct a \hyperref[def:step-2-model]{step-2 intensional model}.
\end{lemma}
We begin with a definition and some lemmas that will be useful in the construction
of the model.
\begin{definition}
Let $c : A \rel A'$ be a value relation of $\mathcal M$.
Let $P_A$ be a monoid of perturbations on $A$ and $P_{A'}$ a monoid of perturbations on $A'$.
A \emph{push-pull structure} $\piv_c$ for $c$ with respect to $P_A$ and $P_{A'}$ consists of:
\begin{itemize}
\item A function $\push : P_A \to P_{A'}$
such that for all $\delta^l \in P_A$ we have $\delta^l \ltdyn_c^c \push(\delta^l)$.
\item A function $\pull : P_{A'} \to P_A$
such that for all $\delta_r \in P_{A'}$ we have $\pull(\delta^r) \ltdyn_{c}^c \delta^r$.
\end{itemize}
We define a push-pull structure $\pie_d$ for $d : B \rel B'$ with respect to perturbation monoids
$P_B$ and $P_{B'}$ in an analogous manner.
% \eric{do we need that $\delta^*$ is preserved by push and pull?}
% We stipulate the additional requirement that if $\delta_A^*$ is in $P_B$
% (where $\delta_A^*$ is the distinguished perturbation required to be in every $\ef(FA, FA)$),
% then $\push(\delta_A^*) = \delta_{A'}^*$ and likewise $\pull(\delta_{A'}^*) = \delta_A^*$.
\end{definition}
%%%%%%%%%%%%%%%
% Composition %
%%%%%%%%%%%%%%%
\begin{lemma}\label{lem:push-pull-comp}
Let $c : A \rel A'$ and $c' : A' \rel A''$ be value relations,
and let $P_A, P_{A'}$ and $P_{A''}$ be monoids of perturbations.
Given a push-pull structure $\piv_c$ for $c$ with respect to $P_A$ and $P_{A'}$, and
and a push-pull structure $\piv_{c'}$ for $c'$ with respect to $P_{A'}$ and $P_{A''}$,
we can define a push-pull structure $\piv_{c \comp c'}$ for $c \comp c'$.
Likewise, we can define a push-pull structure for the composition of computation relations.
\end{lemma}
\begin{proof}
We define $\piv_{c \comp c'}$ as the following push-pull structure:
\begin{itemize}
\item $\push_{c \comp c'} = \push_{c'} \circ \push_{c}$
\item $\pull_{c \comp c'} = \pull_{c} \circ \pull_{c'}$
\end{itemize}
We observe that the required squares exist for both push and pull.
In particular, for push we have that $\delta^l \ltdyn_c^c \push_c(\delta^l)$
using the push property for $c$, and then using the push property for $c'$ we have
$\push_c(\delta^l) \ltdyn_{c'}^{c'} \push_{c'}(\push_c(\delta^l))$.
We can then compose these squares horizontally to obtain the desired square.
The pull property follows similarly.
The push-pull structure for the composition of computation relations is defined analogously.
\end{proof}
%%%%%%%%%%%
% U and F %
%%%%%%%%%%%
\begin{lemma}\label{lem:push-pull-U-F}
Let $c : A \rel A'$ and let $P_A$ and $P_{A'}$ be monoids of perturbations.
Given a push-pull structure $\piv_c$ for $c$ with respect to $P_A$ and $P_{A'}$,
we can define a push-pull structure $\pie_{Fc}$ for $F(c)$ with respect to
$\mathbb{N} \times P_{A}$ and $\mathbb{N} \times P_{A'}$.
Likewise, from a push-pull structure for $d$ with respect to $P_B$ and $P_{B'}$,
we can define a push-pull structure for $Ud$ with respect to $\mathbb{N} \times P_B$
and $\mathbb{N} \times P_{B'}$.
\end{lemma}
\begin{proof}
We define $\push_{Fc} : \mathbb{N} \times P_{A} \to \mathbb{N} \times P_{A'}$ by
\[ \push_{Fc}(n, a) = (n, \push_c(a)). \]
Then we need to build the following square:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFsxLDAsIkZBJyJdLFswLDEsIkZBIl0sWzEsMSwiRkEnIl0sWzIsMywiRmMiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFswLDEsIkZjIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMCwyLCIoXFxkZWx0YV97RkF9XiopXm4gXFxjaXJjIFxccHRiX0EoYSkiLDJdLFsxLDMsIihcXGRlbHRhX3tGQSd9XiopXm4gXFxjaXJjIFxccHRiX3tBJ30oXFxwdXNoX2MoYSkpIl1d
\[\begin{tikzcd}[ampersand replacement=\&]
FA \& {FA'} \\
FA \& {FA'}
\arrow["Fc", "\shortmid"{marking}, no head, from=2-1, to=2-2]
\arrow["Fc", "\shortmid"{marking}, no head, from=1-1, to=1-2]
\arrow["{(\delta_{FA}^*)^n \circ \ptb_A(a)}"', from=1-1, to=2-1]
\arrow["{(\delta_{FA'}^*)^n \circ \ptb_{A'}(\push_c(a))}", from=1-2, to=2-2]
\end{tikzcd}\]
This is obtained by pasting $n$ copies of the square $\delta_{FA}^* \ltdyn_{Fc}^{Fc} \delta_{FA'}^*$
on top of the square corresponding to the push property for $c$.
% Given $n \in \mathbb{N}$ we define the push to be $n$.
% Then the required square is $\delta_{FA}^* \ltdyn_{Fc}^{Fc} \delta_{FA'}^*$,
% which exists by the definition of a step-1 model.
% On the other hand, given $a \in P_{A}$, we define the push to be $\push_c(a)$
% and then the required exists by the push property for $c$.
% Defining $\pull_{Fc}$ is symmetric.
The proof for $Ud$ is analogous.
\end{proof}
%%%%%%%%%%%%
% Products %
%%%%%%%%%%%%
\begin{lemma}\label{lem:push-pull-times}
Let $c_1 : A_1 \rel A_1'$ and $c_2 : A_2 \rel A_2'$, and let $P_{A_1}$,
$P_{A_2}$, $P_{A_1'}$ and $P_{A_2'}$ be monoids of perturbations.
Given push-pull structures
$\piv_{c_1}$ with respect to $P_{A_1}$ and $P_{A_1'}$, and
$\piv_{c_2}$ with respect to $P_{A_2}$ and $P_{A_2'}$,
we can define a push-pull structure $\piv_{c_1 \times c_2}$
with respect to $P_{A_1} \times P_{A_2}$ and $P_{A_1'} \times P_{A_2'}$.
% Likewise, given push-pull structures
% $\pie_{Fc_1}$ with respect to $F(P_{A_1})$ and $F(P_{A_1'})$, and
% $\pie_{Fc_2}$ with respect to $F(P_{A_2})$ and $F(P_{A_2'})$,
% we can define a push-pull structure $\pie_{F(c_1 \times c_2)}$
% with respect to $F(P_{A_1} \times P_{A_2})$ and $F(P_{A_1'} \times P_{A_2'})$.
\end{lemma}
\begin{proof}
We define the push function for $\piv_{c_1 \times c_2}$ by
$\push(a_1, a_2) = (\push_{c_1}(a_1), \push_{c_2}(a_2))$ and likewise for $\pull$.
The push property holds because it holds for each component.
The pull property is established similarly.
\end{proof}
%%%%%%%%%
% Arrow %
%%%%%%%%%
\begin{lemma}\label{lem:push-pull-arrow}
Let $c : A \rel A'$ and $d : B \rel B'$.
Given push-pull structures $\piv_c$ for $c$ and $\pie_d$ for $d$,
we can define a push-pull structure $\pie_{c \arr d}$ for $c \arr d$.
% Given push-pull structures $\pie_{Fc}$ for $Fc$ and $\piv_{Ud}$ for $Ud$,
% we can define a push-pull structure $\piv_{U(c \arr d)}$ for $U(c \arr d)$
% with respect to the monoids $(P_{FA})^{op} \oplus P_B$
\end{lemma}
\begin{proof}
Follows from the functorial action of $\arr$ on perturbations and squares.
% and the latter uses the functorial action of $\tok$ on perturbations and squares.
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%
% Model Construction %
%%%%%%%%%%%%%%%%%%%%%%
We now proceed with the construction of the model:
Define a step-2 model $\mathcal M'$ as follows:
\begin{itemize}
\item Value objects are pairs consisting of:
\begin{itemize}
\item A value object $A$ in $\vf$.
\item A monoid $P_A$ of perturbations
and a monoid homomorphism $\ptb_A : P_A \to \{ f \in \vf(A, A) \mid f \bisim \id_A \}$.
\end{itemize}
\item Computation objects are pairs consisting of:
\begin{itemize}
\item A computation object $B$ in $\ef$.
\item A monoid $P_B$ of perturbations and a monoid homomorphism
$\ptb_B : P_B \to \{ \phi \in \ef(B, B) \mid \phi \bisim \id_B \}$.
\end{itemize}
\item Morphisms are given by morphisms of the underlying objects in $\vf$ and $\ef$, respectively.
%, i.e.,
% \[ \vf'((A, P_A, \ptb_A, P^K_A, \ptbk_A), (A', P_{A'}, \ptb_{A'}, P^K_{A'}, \ptbk_{A'})) = \vf(A, A') \]
%
% and likewise for computations.
\item Given objects $(A, P_A, \ptb_A)$ and $(A', P_{A'}, \ptb_{A'})$ a value relation
is a pair consisting of
\begin{itemize}
\item A value relation $c \in \vsq$.
\item A push-pull structure $\piv_c$ for $c$ with respect to $P_A$ and $P_{A'}$.
%\item A push-pull structure $\pie_{Fc}$ for $Fc$ with respect to $P^K_A$ and $P^K_{A'}$.
\end{itemize}
\item Similarly, a computation relation between $(B, P_B, \ptb_B)$ and $(B', P_{B'}, \ptb_{B'})$
consists of
\begin{itemize}
\item A computation relation $d \in \esq$.
\item A push-pull structure $\pie_d$ for $d$ with respect to $P_B$ and $P_{B'}$.
%\item A push-pull structure $\piv_{Ud}$ for $Ud$ with respect to $P^K_B$ and $P^K_{B'}$.
\end{itemize}
\item The squares are the same as the squares of the original model $\mathcal M$
%morphisms of $\vsq'$ and $\esq'$ are given by the morphisms of $\vsq$ and $\esq$.
\item We define composition of relations $(c, \piv_c)$ and $(c', \piv_{c'})$
as $(c \comp c', \piv_{c \comp c'})$ where $\piv_{c \comp c'}$ is as in Lemma
\ref{lem:push-pull-comp}, and likewise for computation relations.
\end{itemize}
% Functors \times, +, F, U, arrow
Now we define the actions of the functors:
\begin{itemize}
\item We define $\times$ on objects by
\[ (A_1, P_{A_1}, \ptb_{A_1}) \times (A_2, P_{A_2}, \ptb_{A_2}) =
(A_1 \times A_2, P_{A_1} \times P_{A_2}, \ptb_{A_1 \times A_2}) \]
where $\ptb_{A_1 \times A_2}(p_1, p_2) = \ptb_{A_1}(p_1) \times \ptb_{A_2}(p_2)$.
Using Lemma \ref{lem:push-pull-times}, we define $\times$ on relations by
\[ (c_1, \piv_{c_1}), (c_2 \piv_{c_2}) =
(c_1 \times c_2, \piv_{c_1 \times c_2}). \]
\item We define $F$ on objects by
\[ F(A, P_A, \ptb_A) = (FA, \mathbb{N} \times P_A, \ptb_{FA}), \]
where we define $\ptb_{FA}(n, a) = (\delta_{FA}^*)^n \circ F(\ptb_A(a))$.
Using Lemma \ref{lem:push-pull-U-F}, we define $F$ on relations by
\[ F(c, \piv_c) = (Fc, \pie_{Fc}). \]
\item We define $U$ on objects by
\[ U(B, P_B, \ptb_B) = (UB, \mathbb{N} \times P_B, \ptb_{UB}), \]
where we define $\ptb_{UB}(n, b) = (\delta_{UB}^*)^n \circ U(\ptb_B(b))$.
Using Lemma \ref{lem:push-pull-U-F}, we define $U$ on relations by
\[ U(d, \pie_d) = (Ud, \piv_{Ud}). \]
We define $\arr$ on objects by
\[ (A, P_A, \ptb_A) \arr (B, P_B, \ptb_B) =
(A \arr B, P_A^{op} \times P_B, \ptb_{A \arr B}), \]
where we define $\ptb_{A \arr B}(a, b) = \ptb_A(a) \arr \ptb_B(b)$.
Using Lemma \ref{lem:push-pull-arrow}, we define $\arr$ on relations by
\[ (c, \piv_c) \arr (d, \pie_d) =
(c \arr d, \pie_{c \arr d}). \]
\end{itemize}
We define a Kleisli arrow operation on perturbations that takes a perturbation
in $P_{UB}$ to a perturbation in $P_{U(A \to B)}$, as follows:
Given a perturbation $u = (n, b) \in P_{UB}$ we define $\id \tok u$ to be
$(n, \id_{P_A}, b) \in P_{U(A \to B)}$.
We need to show that
%
\[ \ptb_{U(A \arr B)}(\id \tok (n, b)) = \id \tok \ptb_{UB}(n, b). \]
%
That is, we need to show that
%
\[ (\delta_{U(A \arr B)}^*)^n \circ U(\id_{A} \arr \ptb_B(b)) =
\id \tok (\delta_{UB}^*)^n \circ U(\ptb_B(b)) \]
%
This can be checked by unfolding the definition of $\tok$; the proof uses the fact that
$\delta_{UB}^*$ commutes with computation morphisms.
%
Given a perturbation $q = (n, a) \in P_{FA}$ we define
$(n, a) \tok \id = (n, a, \id_{P_B}) \in P_{U(A \to B)}$.
We need to show that
%
\[ \ptb_{U(A \arr B)}((n, a) \tok \id) = \ptb_{FA}(n, a) \tok \id. \]
%
By similar reasoning to the above, this holds because $\delta_{FA}^*$
commutes with computation morphisms.
We can similarly construct a Kleisli product operation on perturbations.
Given a perturbation $(n, a_1, a_2) \in P_{F(A_1 \times A_2)}$ we define
$(n, a_1, a_2) \timesk \id = (n, a_1, \id_{P_{A_2}})$,
and likewise we define $\id \timesk (n, a_1, a_2) = (n, \id_{P_{A_1}}, a_2)$.
% We have $\ptb_{U(A \arr B)}(\id \tok (n, b)) = \ptb_{U(A \arr B)}(n, \id, b)$,
% which is equal to $\delta_{U(A \arr B)}^n (\id \to \ptb_B(b))$
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Constructing a Model with Quasi-Representable Relations}
The goal of this section is to prove the following lemma:
\begin{lemma}\label{lem:step-2-model-to-step-3-model}
Let $\mathcal M$ be a \hyperref[def:step-2-model]{step-2 intensional model}.
Then we can construct a \hyperref[def:step-3-model]{step-3 intensional model}.
\end{lemma}
Before proceeding with the proof, we begin with a definition.
\begin{definition}[representation structure]\label{def:representation-structure}
Let $c : A \rel A'$ be a value relation. A \emph{left-representation structure}
$\rho^L_c$ for $c$ consists of a value morphism $e_c \in \vf(A, A')$ such that
$c$ is quasi-left-representable by $e_c$ (see Definition \ref{def:quasi-left-representable}).
We similarly define a {right-representation structure} $\rho^R_c$ for $c$ to consist of a morphism
$p_c \in \vf(A', A)$ such that $c$ is quasi-right-representable by $p_c$ (see Definition \ref{def:quasi-right-representable}).
% (Notice that the direction of the morphism is opposite in the definition of
% right-representation structure.)
Likewise, let $d : B \rel B'$ be a computation relation. Left- and right-representation
structures for $d$ are defined in a similar manner, except the representing morphisms
are now computation morphisms rather than value morphisms.
% Likewise, let $d : B \rel B'$ be a computation relation. A \emph{right-representation structure}
% $\rho^R_d$ for $d$ consists of a computation morphism $p_d \in \ef(B', B)$
% such that $d$ is quasi-right-representable by $p_d$ (see Definition
% \ref{def:quasi-right-representable}).
\end{definition}
% TODO establish the notation
Recall the notion of quasi-order-equivalence as defined in Definition \ref{def:quasi-order-equivalent}.
The following lemma will be useful in showing that two relations are quasi-order-equivalent.
\begin{lemma}\label{lem:left-rep-by-same-morphism}
Let $c, c' : A \rel A'$. If $c$ and $c'$ are both quasi-left-representable
by the same $f$, then $c \qordeq c'$.
Dually, if $d$ and $d'$ are both quasi-right-representable by the same $\phi$, then
$d \qordeq d'$.
\end{lemma}
\begin{proof}
By $\upr$ for $c'$, there exists a perturbation $\delle_{c'}$ and a square
$\upr_{c'} : \delle_{c'} \ltdyn_{c'}^{r(A)} f$.
By $\upl$ for $c$, there exists a perturbation $\delre_c$ and a square
$\upl_c : f \ltdyn_{r(A')}^{c} \delre_c$.
Composing these horizontally we get the following square:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJBIl0sWzEsMCwiQSJdLFsyLDAsIkEnIl0sWzAsMSwiQSJdLFsxLDEsIkEnIl0sWzIsMSwiQSciXSxbMCwxLCJyKEEpIl0sWzEsMiwiYyJdLFszLDQsImMnIiwyXSxbNCw1LCJyKEEnKSIsMl0sWzAsMywiXFxkZWxsZV97Yyd9IiwyXSxbMSw0LCJmIiwyXSxbMiw1LCJcXGRlbHJlX2MiXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
A \& A \& {A'} \\
A \& {A'} \& {A'}
\arrow["{r(A)}", from=1-1, to=1-2]
\arrow["c", from=1-2, to=1-3]
\arrow["{c'}"', from=2-1, to=2-2]
\arrow["{r(A')}"', from=2-2, to=2-3]
\arrow["{\delle_{c'}}"', from=1-1, to=2-1]
\arrow["f"', from=1-2, to=2-2]
\arrow["{\delre_c}", from=1-3, to=2-3]
\end{tikzcd}\]
And since $r(A) \comp c = c$ and $c' \comp r(A') = c'$, we are finished.
The other square (i.e., with $c'$ on top) is constructed in an analogous manner.
\end{proof}
%%%%%%%%%%%%%%%
% Composition %
%%%%%%%%%%%%%%%
\begin{lemma}\label{lem:representation-comp}
In the below, let $c : A \rel A'$ and $c' : A' \rel A''$ and $d : B \rel B'$ and $d' : B' \rel B''$.
\begin{enumerate}
\item Given left-representation structures $\rho^L_c$ for $c$ and $\rho^L_{c'}$ for $c'$,
we can define a left-representation structure for the composition $c \comp c'$
\item Given right-representation structures $\rho^R_d$ for $d$ and $\rho^R_{d'}$ for $d'$,
we can define a right-representation structure for the composition $d \comp d'$
\item Given right-representation structures $\rho^R_{Fc}$ for $Fc$ and $\rho^R_{Fc'}$ for $Fc'$,
we can define a right-representation structure $\rho^R_{F(c \comp c')}$ for $F(c \comp c')$.
\item Given left-representation structures $\rho^L_{Ud}$ for $Ud$ and $\rho^L_{Ud'}$ for $Ud'$,
we can define a left-representation structure $\rho^L_{U(d \comp d')}$ for $U(d \comp d')$.
\end{enumerate}
\end{lemma}
\begin{proof}
\begin{enumerate}
% 1.
\item We define $\rho^L_{c \comp c'}$ as follows. In the definitions of the perturbations,
we make use of the fact that $c$ and $c'$ satisfy the push-pull property.
\begin{itemize}
\item $e_{c \comp c'} = e_{c'} \circ e_c$
\item $\delre_{c \comp c'} = \delre_{c'} \circ \push_{c'}(\delre_c)$
\item $\delle_{c \comp c'} = \pull_c(\delle_{c'}) \circ \delle_c$
\item $\upl$ is the following square: \input{squares/UpL-comp}
The square $(*)$ exists by the push-pull property for $c'$, and the square $(**)$ exists
because $r$ is a unit for horizontal composition, so $r(A') \comp c' = c'$, and so this
is simply the identity square $\id_{c'} \in \vsq(c', c')$.
\item $\upr$ is the following square: \input{squares/UpR-comp}
\end{itemize}
% 2.
\item We define $\rho^R_{d \comp d'}$ as follows:
\begin{itemize}
\item $p_{d \comp d'} = p_d \circ p_{d'}$
\item $\dellp_{d \comp d'} = \dellp_d \circ \pull_d(\dellp_{d'})$
\item $\delrp_{d \comp d'} = \push_{d'}(\delrp_d) \circ \delrp_{d'}$
\item $\dnr$ is the following square: \input{squares/DnR-comp}
Here the square $(*)$ exists by the push-pull property for $d$.
\item $\dnl$ is the following square: \input{squares/DnL-comp}
\end{itemize}
% 3.
\item We define $\rho^R_{F(c \comp c')}$ as follows.
% First, we observe that by Lemma \ref{lem:left-rep-by-same-morphism},
% $F(c \comp c')$ and $Fc \comp Fc'$ are quasi-order-equivalent,
% as both are left-represented by $Fe_c' \circ Fe_c$.
First, we claim that $F(c \comp c')$ and $Fc \comp Fc'$ are
both quasi-left-represented by $Fe_{c'} \circ Fe_c$.
Indeed, we have by part (1) that $e_c' \circ e_c$ left-represents $c \comp c'$,
and then since $F$ preserves perturbations and squares it follows that
$F(e_c' \circ e_c) = Fe_{c'} \circ Fe_c$ quasi-left-represents $F(c \comp c')$.
On the other hand, we also know that $Fe_c$ quasi-left-represents $Fc$ and $Fe_{c'}$
left-represents $Fc'$, so their composition quasi-left-represents $Fc \comp Fc'$.
Thus, by Lemma \ref{lem:left-rep-by-same-morphism}, there is a square $\alpha$ of the form
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJGQSJdLFsyLDAsIkZBJyciXSxbMCwxLCJGQSJdLFsxLDEsIkZBJyJdLFsyLDEsIkZBJyciXSxbMCwxLCJGKGMgXFxjb21wIGMnKSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzIsMywiRmMiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFszLDQsIkZjJyIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzAsMiwiXFxkZWx0YV5sIiwyXSxbMSw0LCJcXGRlbHRhXnIiXSxbOCw5LCJcXGFscGhhIiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
FA \&\& {FA''} \\
FA \& {FA'} \& {FA''}
\arrow["{F(c \comp c')}", "\shortmid"{marking}, no head, from=1-1, to=1-3]
\arrow["Fc", "\shortmid"{marking}, no head, from=2-1, to=2-2]
\arrow["{Fc'}", "\shortmid"{marking}, no head, from=2-2, to=2-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\delta^l}"', from=1-1, to=2-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\delta^r}", from=1-3, to=2-3]
\arrow["\alpha"{description}, draw=none, from=0, to=1]
\end{tikzcd}\]
for some perturbations $\delta^l$ and $\delta^r$.
We define the projection $p_{F(c \comp c')}$ to be $p_{Fc \comp Fc'} \circ \delta^r$.
We define $\dellp_{F(c \comp c')}$ to be $\dellp_{Fc \comp Fc'} \circ \delta^l$
Then we can build the square for $\dnr$ by pasting the square $\alpha$ on top of
the $\dnr$ square for the composition $Fc \comp Fc'$, as shown below:
% https://q.uiver.app/#q=WzAsNyxbMCwwLCJGQSJdLFsyLDAsIkZBJyciXSxbMCwxLCJGQSJdLFsxLDEsIkZBJyJdLFsyLDEsIkZBJyciXSxbMCwyLCJGQSJdLFsyLDIsIkZBIl0sWzAsMSwiRihjIFxcY29tcCBjJykiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsyLDMsIkZjIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMyw0LCJGYyciLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs1LDYsInIoRkEpIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMCwyLCJcXGRlbHRhXmwiLDJdLFsyLDUsIlxcZGVsbHBfe0ZjIFxcY29tcCBGYyd9IiwyXSxbMSw0LCJcXGRlbHRhXnIiXSxbNCw2LCJwX3tGYyBcXGNvbXAgRmMnfSJdLFsxMSwxMywiXFxhbHBoYSIsMyx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsxMiwxNCwiXFxkbnJfe0ZjIFxcY29tcCBGYyd9IiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
FA \&\& {FA''} \\
FA \& {FA'} \& {FA''} \\
FA \&\& FA
\arrow["{F(c \comp c')}", "\shortmid"{marking}, no head, from=1-1, to=1-3]
\arrow["Fc", "\shortmid"{marking}, no head, from=2-1, to=2-2]
\arrow["{Fc'}", "\shortmid"{marking}, no head, from=2-2, to=2-3]
\arrow["{r(FA)}"', "\shortmid"{marking}, no head, from=3-1, to=3-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\delta^l}"', from=1-1, to=2-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\dellp_{Fc \comp Fc'}}"', from=2-1, to=3-1]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\delta^r}", from=1-3, to=2-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{p_{Fc \comp Fc'}}", from=2-3, to=3-3]
\arrow["\alpha"{marking, allow upside down}, draw=none, from=0, to=2]
\arrow["{\dnr_{Fc \comp Fc'}}"{description}, draw=none, from=1, to=3]
\end{tikzcd}\]
We define $\delrp_{F(c \comp c')}$ to be $\delrp_{Fc \comp Fc'} \circ \delta^r$.
For $\dnl$, we paste the identity square $\delta^r \ltdyn \delta^r$ on top of
the $\dnl$ square for the composition $Fc \comp Fc'$, and below that we paste
the square $\id \ltdyn_{F(c \comp c')}^{Fc \comp Fc'} \id$ which we get from
the fact that $F$ is lax.
% https://q.uiver.app/#q=WzAsOSxbMCwwLCJGQScnIl0sWzIsMCwiRkEnJyJdLFswLDEsIkZBJyciXSxbMiwxLCJGQScnIl0sWzAsMiwiRkEiXSxbMiwyLCJGQScnIl0sWzAsMywiRkEiXSxbMiwzLCJGQScnIl0sWzEsMiwiRkEnIl0sWzAsMSwicihGQScnKSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzIsMywicihGQScnKSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzYsNywiRihjIFxcY29tcCBjJykiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFswLDIsIlxcZGVsdGFeciIsMl0sWzIsNCwicF97RmMgXFxjb21wIEZjJ30iLDJdLFs0LDYsIlxcaWQiLDJdLFsxLDMsIlxcZGVsdGFeciJdLFszLDUsIlxcZGVscnBfe0ZjIFxcY29tcCBGYyd9Il0sWzUsNywiXFxpZCJdLFs0LDgsIkZjIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbOCw1LCJGYyciLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsxMiwxNSwicihcXGRlbHRhXnIpIiwzLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzEzLDE2LCJcXGRubF97RmMgXFxjb21wIEZjJ30iLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0=
\[\begin{tikzcd}[ampersand replacement=\&]
{FA''} \&\& {FA''} \\
{FA''} \&\& {FA''} \\
FA \& {FA'} \& {FA''} \\
FA \&\& {FA''}
\arrow["{r(FA'')}", "\shortmid"{marking}, no head, from=1-1, to=1-3]
\arrow["{r(FA'')}", "\shortmid"{marking}, no head, from=2-1, to=2-3]
\arrow["{F(c \comp c')}"', "\shortmid"{marking}, no head, from=4-1, to=4-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\delta^r}"', from=1-1, to=2-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{p_{Fc \comp Fc'}}"', from=2-1, to=3-1]
\arrow["\id"', from=3-1, to=4-1]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\delta^r}", from=1-3, to=2-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\delrp_{Fc \comp Fc'}}", from=2-3, to=3-3]
\arrow["\id", from=3-3, to=4-3]
\arrow["Fc", "\shortmid"{marking}, no head, from=3-1, to=3-2]
\arrow["{Fc'}", "\shortmid"{marking}, no head, from=3-2, to=3-3]
\arrow["{r(\delta^r)}"{marking, allow upside down}, draw=none, from=0, to=2]
\arrow["{\dnl_{Fc \comp Fc'}}"{description}, draw=none, from=1, to=3]
\end{tikzcd}\]
% 4.
\item We define $\rho^L{(U(d \comp d'))}$ in an analogous manner to the above.
\end{enumerate}
\end{proof}
% Want to show: U(d \comp d') is weakly equivalent to U(d) \comp U(d').
% This holds because both are quasi-representable by the same projection
% \begin{lemma}
% Let $\mathcal M$ be a step-3 intensional model, and let
% $d : B \rel B'$ and $d' : B' \rel B''$.
% Let $\rho_\text{comp}$ be an arbitrary right-representation for $d \comp d'$.
% Then the projection $p_{d \circ d'}$ is weakly equivalent to
% \end{lemma}
%%%%%%%%%%%%%
% UF and FU %
%%%%%%%%%%%%%
\begin{lemma}\label{lem:representation-UF-FU}
Let $c : A \rel A'$, and let $\rho^L_c$ be a left-representation structure for $c$.
Then we can define a left-representation structure $\rho^L_{UF(c)}$ for $UF(c)$.
Similarly, let $d : B \rel B'$ and let $\rho^R_d$ be a right-representation structure for $d$.
Then we can define a right-representation structure $\rho^R_{FU(d)}$ for $FU(d)$.
\end{lemma}
\begin{proof}
We define $\rho^L_{UF(c)}$ as follows:
\begin{itemize}
\item $e_{UF(c)} = UF(e_c)$
\item $\delre_{UF(c)} = UF(\delre_c)$ (which is in the monoid of perturbations of $UF(A')$ because the
perturbation monoids are closed under the actions of the functors $F$ and $U$)
\item $\delle_{UF(c)} = UF(\delle_c)$
\item We get the two commuting squares by the functorial action of $UF$ on the two squares for $c$,
i.e., $\upr_{UF(c)} = UF(\upr_c)$
\end{itemize}
We define $\rho^R_{FU(d)}$ in a similar manner.
\end{proof}
%%%%%%%%%%%%
% Products %
%%%%%%%%%%%%
\begin{lemma}\label{lem:representation-product}
Let $c_1 : A_1 \rel A_1'$ and $c_2 : A_2 \rel A_2'$.
Let $\rho^L_{c_1}$ be a left-representation structure for $c_1$, and
let $\rho^L_{c_2}$ be a left-representation structure for $c_2$.
Then we can define a left-representation structure for $c_1 \times c_2$.
Likewise, let $\rho^R_{Fc_1}$ and $\rho^R_{Fc_2}$ be right-representation
structures for $Fc_1$ and $Fc_2$ respectively.
Then we can define a right-representation structure for $F(c_1 \times c_2)$.
\end{lemma}
\begin{proof}
We define $\rho^L_{c_1 \times c_2}$ as follows:
\begin{itemize}
\item $e_{c_1 \times c_2} = e_{c_1} \times e_{c_2}$
\item $\delre_{c_1 \times c_2} = \delre_{c_1} \times \delre_{c_2}$ and
likewise for $\delle_{c_1 \times c_2}$
\item We get the commuting squares via the functorial action of $\times$
on the corresponding squares for $c_1$ and $c_2$.
\end{itemize}
% TODO check this
We define $\rho^R_{F(c_1 \times c_2)}$ as follows:
\begin{itemize}
\item $p_{F(c_1 \times c_2)} = (p_{Fc_1} \timesk A_2) \circ (A_1' \timesk p_{Fc_2})$
\item $\dellp_{F(c_1 \times c_2)} = (\dellp_{Fc_1} \timesk A_2) \circ (A_1 \timesk \dellp_{Fc_2})$
\item $\delrp_{F(c_1 \times c_2)} = (\delrp_{Fc_1} \timesk A_2') \circ (A_1' \timesk \delrp_{Fc_2})$
\item The commuting squares are obtained via the functorial action of $\timesk$ on the squares for $Fc_1$ and $Fc_2$.
\end{itemize}
\end{proof}
%%%%%%%%%
% Arrow %
%%%%%%%%%
\begin{lemma}\label{lem:representation-arrow}
Let $c : A \rel A'$ and $d : B \rel B'$.
Let $\rho^L_c$ be a left-representation structure for $c$,
and let $\rho^R_d$ be a right-representation structure for $d$.
Then we can define a right-representation structure for $c \arr d$.
Likewise, let $\rho^R_{Fc}$ be a right-representation structure for $Fc$,
and let $\rho^L_{Ud}$ be a left-representation structure for $Ud$.
Then we can define a left-representation structure for $U(c \arr d)$.
\end{lemma}
\begin{proof}
We define $\rho^R_{c \arr d}$ as follows:
\begin{itemize}
\item $p_{c \arr d} = e_c \arr p_d \in \ef(A' \arr B', A \arr B)$
(using the functorial action of $\arr$ on morphisms).
\item $\dellp_{c \arr d} = \delle_c \arr \dellp_d$
\item $\delrp_{c \arr d} = \delre_c \arr \delrp_d$
\item The squares $\dnr$ and $\dnl$ are obtained via the functorial action of $\arr$, i.e., we define
\[ \dnr_{c \arr d} = \upr_{c} \arr \dnr_{d} :
(\delle_c \arr \dellp_d) \ltdyn_{r(A \arr B)}^{c \arr d} (e_c \arr p_d), \]
and
\[ \dnl_{c \arr d} = \upl_{c} \arr \dnl_{d}. \]
\end{itemize}
% TODO check this
We define $\rho^L_{U(c \arr d)}$ as follows:
\begin{itemize}
\item $e_{U(c \arr d)} = (p_{Fc} \tok B') \circ (A \tok e_{Ud})$
\item $\delre_{U(c \arr d)} = (\delrp_{Fc} \tok B') \circ (A' \tok \delre_{Ud})$
\item $\delle_{U(c \arr d)} = (\dellp_{Fc} \tok B) \circ (A \tok \delle_{Ud})$
\item The squares $\upl$ and $\upr$ are obtained via the functorial action of $\tok$.
For instance, $\upl$ is given by the following square:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJVKEEgXFx0byBCKSJdLFsyLDAsIlUoQScgXFx0byBCJykiXSxbMiwxLCJVKEEnIFxcdG8gQicpIl0sWzIsMiwiVShBJyBcXHRvIEInKSJdLFswLDEsIlUoQSBcXHRvIEInKSJdLFswLDIsIlUoQScgXFx0byBCJykiXSxbMCwxLCJVKGMgXFx0byBkKSJdLFs0LDIsIlUoYyBcXHRvIHIoQicpKSJdLFs1LDMsIlUocihBJykgXFx0byByKEInKSkiXSxbNCw1LCJwX3tGY30gXFx0b2sgQiciLDJdLFsxLDIsIkEnIFxcdG9rIFxcZGVscmVfe1VkfSJdLFsyLDMsIlxcZGVscnBfe0ZjfSBcXHRvayBCJyJdLFswLDQsIkEgXFx0b2sgZV97VWR9IiwyXSxbMTIsMTAsIlxcaWRfe0ZjfSBcXHRvayBcXHVwbF97VWR9IiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzksMTEsIlxcZG5sX3tGY30gXFx0b2sgXFxpZF97cihCJyl9IiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&,row sep=large]
{U(A \to B)} \&\& {U(A' \to B')} \\
{U(A \to B')} \&\& {U(A' \to B')} \\
{U(A' \to B')} \&\& {U(A' \to B')}
\arrow["{U(c \to d)}", from=1-1, to=1-3]
\arrow["{U(c \to r(B'))}", from=2-1, to=2-3]
\arrow["{U(r(A') \to r(B'))}", from=3-1, to=3-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{p_{Fc} \tok B'}"', from=2-1, to=3-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{A' \tok \delre_{Ud}}", from=1-3, to=2-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\delrp_{Fc} \tok B'}", from=2-3, to=3-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{A \tok e_{Ud}}"', from=1-1, to=2-1]
\arrow["{\id_{Fc} \tok \upl_{Ud}}"{description}, draw=none, from=3, to=1]
\arrow["{\dnl_{Fc} \tok \id_{r(B')}}"{description}, draw=none, from=0, to=2]
\end{tikzcd}\]
\end{itemize}
The construction of $\upr$ is similar.
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%
% Model Construction %
%%%%%%%%%%%%%%%%%%%%%%
Now we can give the proof of the main lemma:
% Write
% %
% \[ \mathcal M = (\vf, \vsq, \ef, \esq, \Ff, \Fsq, \Uf, \Usq, \arrf, \arrsq). \]
% %
We define a step-3 model $\mathcal M'$ as follows:
\begin{itemize}
\item The objects of $\mathcal M'$ are defined to be the same as the objects of $\mathcal M$.
\item The value and computation morphisms in $\mathcal M'$ are the same as those of $\mathcal M$.
\item A value relation is defined to be a tuple $(c, \rho^L_c, \rho^R_{Fc})$ with
\begin{itemize}
\item $c$ a value relation in $\mathcal M$,
\item $\rho^L_c$ a left-representation structure for $c$, and
\item $\rho^R_{Fc}$ a right-representation structure for $Fc$
\end{itemize}
\item Likewise, a computation relation is defined to be a tuple $(d, \rho^R_d, \rho^L_{Ud})$ with
\begin{itemize}
\item $d$ a computation relation in $\mathcal M$,
\item $\rho^R_d$ a right-representation structure for $d$, and
\item $\rho^L_{Ud}$ a left-representation structure for $Ud$.
\end{itemize}
\item Morphisms of value relations (i.e., the value squares) are defined by simply
ignoring the representation structures. That is, a morphism of value relations
$\alpha \in \vsq'((c, \rho^L_c, \rho^R_{Fc}), (c' \rho^L_{c'}, \rho^R_{Fc'}))$ is simply a morphism of value
relations in $\vsq(c, c')$. Likewise for computations.
\end{itemize}
We define horizontal composition of relations and squares as follows:
Let $c : A \rel A'$ and $c' : A' \rel A''$. We define
%
\begin{align*}
((c, \rho^L_c, &\rho^R_{Fc}) \comp (c', \rho^L_{c'}, \rho^R_{Fc'})) =
(c \comp c', \rho^L_{c \comp c'}, \rho^R_{F(c \comp c')}),
\end{align*}
%
and
%
\begin{align*}
((d, \rho^R_d, &\rho^L_{Ud}) \comp (d', \rho^R_{d'}, \rho^L_{Ud'})) =
(d \comp d', \rho^R_{d \comp d'}, \rho^L_{U(d \comp d')}),
\end{align*}
%
where $\rho^L_{c \comp c'}, \rho^R_{F(c \comp c')}, \rho^R_{d \comp d'},$
and $\rho^L_{U(d \comp d')}$ are as defined in Lemma \ref{lem:representation-comp}.
Now we define the functors $F$, $U$, $\times$, and $\arr$.
On objects, the behavior is the same as the respective functors in $\mathcal M$.
For relations, we define
\[ F(c, \rho^L_c, \rho^R_{Fc}) =
(F c, \rho^R_{Fc}, \rho^L_{UF(c)}), \]
and
\[ U(d, \rho^R_d, \rho^L_{Ud}) =
(U d, \rho^L_{Ud}, \rho^R_{FU(d)}), \]
where $\rho^L_{UF(c)}$ and $\rho^R_{FU(d)}$ are as defined in the proof of Lemma
\ref{lem:representation-UF-FU}.
We define \[ (c_1, \rho^L_{c_1}, \rho^R_{Fc_1}) \times (c_2, \rho^L_{c_2}, \rho^R_{Fc_2}) =
(c_1 \times c_2, \rho^L_{c_1 \times c_2}, \rho^R_{F(c_1 \times c_2)}), \]
where $\rho^L_{c_1 \times c_2}$ and $\rho^R_{F(c_1 \times c_2)}$ are as defined in the
proof of Lemma \ref{lem:representation-product}.
Lastly, we define
\[ (c, \rho^L_c, \rho^R_{Fc}) \arr (d, \rho^R_d, \rho^L_{Ud}) =
(c \arr d, \rho^R_{c \arr d}, \rho^L_{U(c \arr d)}), \]
where $\rho^R_{c \arr d}$ and $\rho^L_{U(c \arr d)}$ are as defined in the proof
of Lemma \ref{lem:representation-arrow}.
% We define $(c, \rho^L_c) \arr (d, \rho^R_d) = (c \arr d, \rho^R_{c \arr d})$.
We now establish the quasi-order-equivalence for the functors.
We already showed that $U(d \comp d') \qordeq U(d)U(d')$ and $F(c \comp c'') \qordeq F(c)F(c')$
in the proof of Lemma \ref{lem:representation-comp}.
The other two properties
$(cc') \to (dd') \qordeq (c \to d)(c' \to d')$ and
$(c_1c_1') \times (c_2c_2') \qordeq (c_1 \times c_2)(c_1'\times c_2')$
are proved similarly, noting in both cases that the both relations are
quasi-represented by the same morphism.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Constructing an Extensional Model}\label{sec:extensional-construction-appendix}
We aim to prove the following lemma:
\begin{lemma}\label{lem:step-4-model-to-extensional-model}
Let $\mathcal M$ be a \hyperref[def:step-4-model]{step-4 intensional model}.
Then we can define an extensional model.
\end{lemma}
\begin{proof}
Recall the extensional model construction outlined in Section \ref{sec:extensional-model-definition}.
We first establish the representability properties for this model.
We show the left-representability squares; the right-representability squares are dual.
\begin{itemize}
\item We have the square
% https://q.uiver.app/#q=WzAsNixbMCwwLCJBIl0sWzAsMSwiQSciXSxbNCwxLCJBX3IiXSxbNCwwLCJBX3IiXSxbMiwwLCJBJyJdLFsyLDEsIkEnIl0sWzAsNCwiYyIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzQsMywiY19yIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMCwxLCJlX2MiLDIseyJjdXJ2ZSI6MX1dLFszLDIsIlxccHVzaF97Y19yfShcXGRlbHJlX2MpIiwyLHsiY3VydmUiOjF9XSxbMSw1LCJyKEEnKSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzQsNSwiXFxkZWxyZV9jIiwyXSxbNSwyLCJjX3IiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFswLDEsImVfYyIsMCx7ImN1cnZlIjotMX1dLFszLDIsIlxcaWQiLDAseyJjdXJ2ZSI6LTF9XSxbOSwxNCwiXFxiaXNpbSIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs4LDEzLCJcXGJpc2ltIiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzE2LDExLCIiLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJsZXZlbCI6Miwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
A \&\& {A'} \&\& {A_r} \\
{A'} \&\& {A'} \&\& {A_r}
\arrow["c", "\shortmid"{marking}, no head, from=1-1, to=1-3]
\arrow["{c_r}", "\shortmid"{marking}, no head, from=1-3, to=1-5]
\arrow[""{name=0, anchor=center, inner sep=0}, "{e_c}"', curve={height=6pt}, from=1-1, to=2-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\push_{c_r}(\delre_c)}"', curve={height=6pt}, from=1-5, to=2-5]
\arrow["{r(A')}"', "\shortmid"{marking}, no head, from=2-1, to=2-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\delre_c}"', from=1-3, to=2-3]
\arrow["{c_r}"', "\shortmid"{marking}, no head, from=2-3, to=2-5]
\arrow[""{name=3, anchor=center, inner sep=0}, "{e_c}", curve={height=-6pt}, from=1-1, to=2-1]
\arrow[""{name=4, anchor=center, inner sep=0}, "\id", curve={height=-6pt}, from=1-5, to=2-5]
\arrow["\bisim"{description}, draw=none, from=1, to=4]
\arrow[""{name=5, anchor=center, inner sep=0}, "\bisim"{description}, draw=none, from=0, to=3]
\arrow[draw=none, from=5, to=2]
\end{tikzcd}\]
\item We have the square
% https://q.uiver.app/#q=WzAsNixbMCwwLCJBX2wiXSxbMCwxLCJBX2wiXSxbMiwxLCJBIl0sWzQsMSwiQSciXSxbMiwwLCJBIl0sWzQsMCwiQSJdLFswLDQsImNfbCJdLFs0LDUsInIoQSkiXSxbMSwyLCJjX2wiLDJdLFsyLDMsImMiLDJdLFswLDEsIlxcaWQiLDIseyJjdXJ2ZSI6MX1dLFs1LDMsImVfYyIsMix7ImN1cnZlIjoxfV0sWzQsMiwiXFxkZWxsZV9jIl0sWzAsMSwiXFxwdWxsX3tjX2x9KFxcZGVsbGVfYykiLDAseyJjdXJ2ZSI6LTF9XSxbNSwzLCJlX2MiLDAseyJjdXJ2ZSI6LTF9XSxbMTAsMTMsIlxcYmlzaW0iLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMTEsMTQsIlxcYmlzaW0iLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0=
\[\begin{tikzcd}[ampersand replacement=\&]
{A_l} \&\& A \&\& A \\
{A_l} \&\& A \&\& {A'}
\arrow["{c_l}", from=1-1, to=1-3]
\arrow["{r(A)}", from=1-3, to=1-5]
\arrow["{c_l}"', from=2-1, to=2-3]
\arrow["c"', from=2-3, to=2-5]
\arrow[""{name=0, anchor=center, inner sep=0}, "\id"', curve={height=6pt}, from=1-1, to=2-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{e_c}"', curve={height=6pt}, from=1-5, to=2-5]
\arrow["{\delle_c}", from=1-3, to=2-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\pull_{c_l}(\delle_c)}", curve={height=-6pt}, from=1-1, to=2-1]
\arrow[""{name=3, anchor=center, inner sep=0}, "{e_c}", curve={height=-6pt}, from=1-5, to=2-5]
\arrow["\bisim"{description}, draw=none, from=0, to=2]
\arrow["\bisim"{description}, draw=none, from=1, to=3]
\end{tikzcd}\]
\end{itemize}
We observe that the functoriality of the CBPV connectives on relations up to
order-equivalence is a direct consequence of the functoriality of the CBPV connectives
on relations up to quasi-order-equivalence in the step-4 intensional model, since the
perturbations on both sides of the square are by definition bisimilar to the identity.
Likewise, the retraction properties for the relations
$\iarr{}: U(D \to F D) \rel D$, $\inat : \nat \rel D$, and $\itimes : D \times D \rel D$
hold because they held up to delays in the intensional model, and the delays
disappear in the extensional model construction.
\end{proof}