\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}

\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}.
Suppose we are given the following data:

\begin{enumerate}
    \item For each value type $A$, a monoid $\pv_A$ and homomorphism 
    \[ \ptbv_A : \pv_A \to \{ f \in \vf(A,A) \mid f \bisim \id \} \]

    \item For each computation type $B$, a monoid $\pv_B$ and homomorphism
    \[ \ptbe_B : \pe_B \to \{ g \in \ef(B,B) \mid g \bisim \id \} \]

    \item For each value type $A$, a distinguished endomorphism
    $\delta_A \in \ef(FA, FA)$ such that $\delta_A \bisim \id_{FA}$.
\end{enumerate}

Then we can construct a \hyperref[def:step-2-model]{step-2 intensional model}.
\end{lemma}
\begin{proof}
    Write 
    %
    \[ \mathcal M = (\vf, \vsq, \ef, \esq, \Ff, \Fsq, \Uf, \Usq, \arrf, \arrsq). \] 
    %
    Define a step-2 model as follows:
    \begin{itemize}
      \item Value objects are tuples of an object $A$ in $\vf$ along with the monoid
      $\pv_A$ and homomorphism $\ptbv_A$:
      $\ob(\vf') = \{ (A, \pv_A, \ptbv_A) \mid A \in \ob(\vf) \}$.
      
      \item Morphisms are given by morphisms of the underlying objects in $\vf$, i.e.,
       $\vf'((A, \pv_A, \ptbv_A), (A', \pv_{A'}, \ptbv_{A'})) = \vf(A, A')$.
      
      \item Computation objects are tuples 
      $\ob(\ef') = \{ (B, \pe_B, \ptbe_B) \mid B \in \ob(\ef) \}$.
      
      \item Computation morphisms are $\ef'((B, \pv_B, \ptbv_B), (B', \pv_{B'}, \ptbv_{B'})) = \ef(B, B')$.
      
      \item The objects $\vsq'$ and $\esq'$ are the same as those of $\vsq$ and $\esq$.
      
      \item The morphisms of $\vsq'$ and $\esq'$ are the same as those of $\vsq$ and $\esq$.
    %   \item $\ob(\vsq') = \ob(\vsq)$
    %   \item $\ob(\esq') = \ob(\esq)$
    %   \item $\vsq'(c, c') = \vsq(c, c')$
    %   \item $\esq'(d, d') = \esq(d, d')$
      
      % 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}.
    Suppose we are given the following data:

    Then we can construct a \hyperref[def:step-3-model]{step-3 intensional model}.
\end{lemma}
\begin{proof}

\end{proof}

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


\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$.