\section{Call-by-push-value}

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 $l : \calE(F A,F A')$ and $B \in \calE$ the morphism $l \tok B : \calV(U(A' \to B),U(A\to B))$ as
  \[ t:U(A'\to B) \vdash l \tok B = \{ \lambda x. x' \leftarrow l\,[\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 $l : \calE(F A_1,FA_2)$ and $A' \in \calV$ the morphism $l \timesk A_2$ as
  \[ \bullet : F(A_1\times A_2) \vdash l \timesk A_2 = (x_1,x_2) \leftarrow \bullet; x_1' \leftarrow l[\ret x_1]; \ret (x_1',x_2) : F(A_1'\times A_2)\]
  and $A_1 \timesk l$ 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 l = Ul$
\end{enumerate}

Functoriality in each argument is easily established, meaning for
example for the function type is functorial in each argument:
\begin{enumerate}
\item $(l \circ l') \tok B = (l' \tok B) \circ (l \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 : l \ltdyn_{F c_o}^{F c_i} l'$ and a horizontal morphism $d : B \rel B'$ of appropriate type, we get a square
\[ \alpha \tok d : l \tok B \ltdyn_{U(c_o \to d)}^{U(c_i \to d)} l' \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.

\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} with dyn.

Then we can construct a \hyperref[def:step-2-model]{step-2 intensional model} with dyn.
\end{lemma}
\begin{proof}
    % Write 
    % %
    % \[ \mathcal M = (\vf, \vsq, \ef, \esq, \Ff, \Fsq, \Uf, \Usq, \arrf, \arrsq). \] 
    % %

    Define a step-2 model $\mathcal M'$ as follows:
    \begin{itemize}
      \item Value objects are tuples consisting of:
      \begin{itemize}
        \item A value object $A$ in $\vf$ 
        \item A monoid of ``pure'' perturbations $P_A$ 
        \item A homomorphism of monoids $\ptb_A : P_A \to \{ f \in \vf(A, A) \mid f \bisim \id_A \}$
        \item A monoid of ``impure'' perturbations $P^K_A$ that contains a distinguished element $\delta^*$
        \item A homomorphism of monoids $\ptbk_A : P^K_A \to \{ \phi \in \ef(FA, FA) \mid \phi \bisim \id_{FA} \}$
        such that $\ptbk_A(\delta^*) = \delta_A^*$
      \end{itemize}  

      \item Computation objects are tuples consisting of:
      \begin{itemize}
        \item A computation object $B$ in $\ef$
        \item A monoid of ``pure'' perturbations $P_B$
        \item A homomorphism of monoids $\ptb_B : P_B \to \{ \phi \in \ef(B, B) \mid \phi \bisim \id_B \}$
        \item A monoid of ``impure'' perturbations $P^K_B$
        \item A homomorphism of monoids $\ptbk_B : P^K_B \to \{ g \in \vf(UB, UB) \mid g \bisim \id_{UB} \}$.
      \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.
   
    \end{itemize}

    Before introducing the relations, we make a definition.

    \begin{definition}[push-pull structure]
      Let $c : A \rel A'$ be a value relation of $\mathcal M$. A \emph{value push-pull structure} $\piv_c$ for $c$ 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 $\push^K : P^K_A \to P^K_{A'}$ 
              such that for all $\delta^K_l \in P^K_A$ we have $\delta^K_l \ltdyn_{Fc}^{Fc} \push(\delta^K_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$.
        \item A function $\pull^K : P^K_{A'} \to P^K_A$
              such that for all $\delta^K_r \in P^K_{A'}$ we have $\pull(\delta^K_r) \ltdyn_{Fc}^{Fc} \delta^K_r$.
      \end{itemize}

      For $d : B \rel B'$ a computation relation, we define a \emph{computation push-pull structure} $\pie_d$ for $d$
      in an analogous manner.
    \end{definition}


    Now we continue with the description of the construction:
    \begin{itemize}

      \item The objects of $\vsq'$ (i.e., the value relations) are pairs consisting of:
      \begin{itemize}
        \item A value relation $c \in \vsq$
        \item A push-pull structure $\piv_c$ for $c$
      \end{itemize}

      The objects of $\esq'$ are defined analogously.
            
      \item The morphisms of $\vsq'$ and $\esq'$ are given by the morphisms of $\vsq$ and $\esq$.
      
      % Functors \times, +, F, U, arrow
     
      % \item We define $F$ on objects by $F (A, \pv_A, \ptbv_A) = (FA, (1 + \pv_A), h_F)$
      % where $1$ is the trivial monoid, $+$ is the coproduct in the category of monoids, and $h_F$ is the homomorphism defined as follows:

      % \item We define $U$ on objects by $U (B, \pe_B, \ptbe_B) = (UB, \pe_B, h_U)$
      % where $h_U(p_B) = U(\ptbe_B(p_B))$.
      
      % \item We define $(A, \pv_A, \ptbv_A) \arr (B, \pe_B, \ptbe_B) = (A \arr B, \pv_A \times \pe_B, h_\arr)$
      % where $\times$ is the product in the category of monoids, and $h_\arr$ is defined by 
      % $h_\arr(p_A, p_B) = \ptbv_A(p_A) \arr \ptbe_B(p_B)$.
    \end{itemize}
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\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}
\begin{proof}
  Write 
  %
  \[ \mathcal M = (\vf, \vsq, \ef, \esq, \Ff, \Fsq, \Uf, \Usq, \arrf, \arrsq). \] 
  %

  We begin with a definition.

  \begin{definition}[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}).
  
  Likewise, let $d : B \rel B'$. 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}
  
  (Notice that the direction of the morphism is opposite in the definition of right-representation structure.)

  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})$ where:
    \begin{itemize}
      \item $c$ is a value relation in $\mathcal M$, and 
      \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$
      \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}
\end{proof}

% 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 
% $\Fsq' (c, \rho^L_c, \rho^R_{Fc}) = (\Fsq c, \rho^R_{Fc}, UF(\rho^L_c))$ and
% $\Usq' (d, \rho^R_d, \rho^L_{Ud}) = (\Usq d, \rho^L_{Ud}, FU(\rho^R_d))$.

% We define $(c, \rho^L_c) \arr (d, \rho^R_d) = (c \arr d, \rho^R_{c \arr d})$.



% We now verify that the construction meets the requirements of a step-3 model.
% First, we check that composition of value relations (resp. computation relations)
% is well-defined.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\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}
  
  
  % More formally, we define an extensional model $\mathcal M_e$ as follows.
  % \begin{itemize}
  %   \item 
  % \end{itemize}
\end{proof}



\section{Adequacy}\label{sec:appendix-adequacy}

In this section, we show an adequacy result for the extensional model of GTT we obtained by
applying the abstract construction introduced in Section
\ref{sec:extensional-model-construction} to the concrete model

First we establish some notation. Fix a morphism $f : 1 \to \li \Nat \cong \li \Nat$.
We write that $f \da n$ to mean that there exists $m$ such that $f = \delta^m(\eta n)$
and $f \da \mho$ to mean that there exists $m$ such that $f = \delta^m(\mho)$.

Recall that $\ltls$ denotes the relation on value morphisms defined as the bisimilarity-closure
of the intensional error-ordering on morphisms.
More concretely, we have $f \ltls g$ iff there exists $f'$ and $g'$ with

\[ f \bisim f' \le g' \bisim g. \]

The result we would like to show is as follows:
\begin{lemma}
If $f \ltls g : \li \Nat$, then:
\begin{itemize}
  \item If $f \da n$ then $g \da n$.
  \item If $g \da \mho$ then $f \da \mho$.
  \item If $g \da n$ then $f \da n$.
\end{itemize}
\end{lemma}

Unfortunately, this result is actually not provable!
Roughly speaking, the issue is that this is a ``global'' result, and it is not possible
to prove such results inside of the guarded setting. 
In particular, if we tried to prove a result such as the above in the guarded setting,
we would run into a problem where we would have a natural number ``stuck'' under a $\later$
with no way to get at the underlying number.

Thus, to prove our adequacy result, we need to leave the guarded setting and pass back
to the normal set-theoretic world.
As mentioned in the Technical Background section (Section \ref{sec:sgdt}), we can do this
using \emph{clock quantification}.

Recall that all of the constructions we have made in SGDT take place in the context of a clock $k$.
All of our uses of the later modality and guarded recursion happen with respect to this clock.
For example, consider the definition of the lift monad by guarded recursion in Section \ref{TODO}.
% We define the lift monad $\li^k X$ as the guarded fixpoint of $\lambda \tilde{T}. X + 1 + \later^k_t (\tilde{T}_t)$.
We can view this definition as being parameterized by a clock $k$: $\li^k : \type \to \type$.
Then for $X$ satisfying a certain technical requirement, we can define the ``global lift'' monad as $\li^{gl} X = \forall k. \li^k X$.


It can be shown that the global lift monad is isomorphic to the so-called Delay monad of Capretta \cite{TODO}.


% We have been writing the type as $\li X$, but it is perhaps more accurate to write it as $\li^k X$ to
% emphasize that the construction is parameterized by a clock $k$.