\section{Constructing a Concrete Model}\label{sec:concrete-model}

In this section, we build a concrete extensional model of gradual typing.
We begin by defining a step-1 intensional model, and then
apply the abstract constructions outlined in the previous section
to obtain an extensional model.
We begin with some definitions:
\begin{definition}
A \textbf{predomain} $A$ consists of a set $A$ along with two relations:
\begin{itemize}
    \item A partial order $\le_A$.
    \item A reflexive, symmetric ``bisimilarity'' relation $\bisim_A$.
\end{itemize}
\end{definition}

% TODO: later of a predomain
Given a predomain $A$, we can form the predomain $\later A$.
The underlying set is $\later |A|$ and the relation is defined in the obvious way,
i.e., $\tilde{x} \le_{\later A} \tilde{x'}$ iff $\later_t(\tilde{x}_t \le_A \tilde{x'}_t)$.
Likewise for bisimilarity.
%
We also give a predomain structure to the natural numbers $\mathbb{N}$, where both the
ordering and the bisimiarity relation are equality.
%
Morphisms of predomains are functions between the underlying sets that preserve the ordering
and the bisimilarity relation. More formally:
%
\begin{definition}
Let $A$ and $A'$ be predomains.
A morphism $f : A \to A'$ is a function between the underlying sets such that for all $x, x'$,
if $x \le_A x'$, then $f(x) \le f(x')$, and if $x \bisim_A x'$, then $f(x) \bisim_{A'} f(x')$.
\end{definition}
%
\begin{definition}
An \textbf{error domain} $B$ consists of a predomain $B$ along with the following data:
\begin{itemize}
    \item A distinguished ``error" element $\mho_B \in B$
    \item A morphism of predomains $\theta_B \colon \later B \to B$
\end{itemize}
\end{definition}
%
For an error domain $B$, we define the predomain morphism $\delta_B := \theta_B \circ \nxt$.
%
Morphisms of error domains are morphisms of the underlying predomains that preserve the
algebraic structure. More formally:
%
\begin{definition}
Let $B$ and $B'$ be error domains.
A morphism $\phi : B \wand B'$ is a morphism between the underlying predomains such that:
\begin{enumerate}
    \item $\phi(\mho_B) = \mho_{B'}$
    \item $\phi(\theta_B(\tilde{x})) = \theta_{B'}(\lambda t. \phi(\tilde{x}_t))$
\end{enumerate}
\end{definition}
%
We define a (monotone) relation on predomains $A$ and $A'$ to be a relation on the
underlying sets that is downward-closed under $\le_A$ and upward-closed under $\le_{A'}$.
More formally:
%
\begin{definition}
Let $A$ and $A'$ be predomains. A \emph{predomain relation} between $A$ and $A'$
is a relation $R$ between the underlying sets such that:
\begin{enumerate}
    \item (Downward closure): For all $x_1, x_2 \in A$ and $y \in A'$,
    if $x_1 \le_A x_2$ and $x_2 \mathbin{R} y$, then $x_1 \mathbin{R} y$.
    \item (Upward closure): For all $x \in A$ and $y_1, y_2 \in A'$,
    if $x \mathbin{R} y_1$ and $y_1 \le_{A'} y_2$, then $x \mathbin{R} y_2$.
\end{enumerate}
\end{definition}
%
Composition of relations on predomains is the usual relational composition.
Similarly, we define a (monotone) relation on error domains to be a relation on the
underlying predomains that respects error and preserves $\theta$.
%
\begin{definition}
    Let $B$ and $B'$ be error domains. An \emph{error domain relation} between
    $B$ and $B'$ is a relation $R$ between the underlying predomains such that
    \begin{enumerate}
       \item (Respects error): For all $y \in B'$, we have $\mho_B \mathbin{R} y$.
       \item (Preserves $\theta$): For all $\tilde{x}$ in $\later B$ and $\tilde{y} \in \later B'$,
       if $\later_t( \tilde{x}_t \mathbin{R} \tilde{y}_t )$ then
       $\theta_B(\tilde{x}) \mathbin{R} \theta_{B'}(\tilde{y})$.
    \end{enumerate}
\end{definition}
%
We define composition of error domain relations $R$ on $B_1$ and $B_2$ and $S$
on $B_2$ and $B_3$ to be the least relation containing $R$ and $S$ that respects
error and preserves $\theta$.
Specifically, it is defined inductively by the following rules:
%
\begin{mathpar}
    \inferrule*[right = Comp]
    {b_1 \mathbin{R} b_2 \and b_2 \mathbin{S} b_3}
    {b_1 \mathbin{R \relcomp S} b_3}

    \inferrule*[right = PresErr]
    { }
    {\mho_{B_1} \mathbin{R \relcomp S} b_3}

    \inferrule*[right = PresTheta]
    {\later_t( \tilde{b_1} \mathbin{R \relcomp S} \tilde{b_3} ) }
    {\theta_{B_1}(\tilde{b_1}) \mathbin{R \relcomp S} \theta_{B_3}(\tilde{b_3}) }
\end{mathpar}
%
% We note that this composition has the following universal property.
%
We now describe the ``commuting squares".
Suppose we are given predomains $A_i, A_o, A_i'$, and $A_o'$,
relations $R_i : A_i \rel A_i'$ and $R_o : A_o \rel A_o'$, and morphisms $f : A_i \to A_o, f' : A_i' \to A_o'$
Given a square with these morphisms and relations, we say that the square commutes, written $f \le f'$, if for all
$x \in A_i$ and $x' \in A_i'$ with $x \mathbin{R_i} x'$, we have
$f(x) \mathbin{R_o} f'(x')$.
We make the analogous definition for error domains.

\subsection{Guarded Lift Monad}\label{sec:guarded-lift-monad}

% Lift monad
The guarded error-lift monad $\li$ takes a predomain $A$ to the error domain $\li A$.
It is defined \footnote{Formally, the lift monad $\li A$ is defined as the solution to
the guarded recursive type equation $\li A \cong A + 1 + \later \li A$.} as follows :
%
\begin{align*}
  \li A :=
  \alt \eta \colon A \to \li A
  \alt \mho \colon \li A
  \alt \theta \colon \later (\li A) \to \li A
\end{align*}
%

This captures the intuition that a program may either return a value,
fail at run-time, or take one or more observable steps of computation.
Previous work has studied such a similar construct, called the guarded lift
monad \cite{mogelberg-paviotti2016}; our version here our version augments it with the notion of error.
Since we claimed that $\li A$ is a monad, we need to define the monadic operations
and show that they respect the monadic laws. The return is just $\eta$, and the monadic extend
is defined via guarded recursion by cases on the input.
Verifying that the monadic laws hold uses \lob-induction and is straightforward.

% \eric{Check}
% We can also show that $\li A$ is the free error- and -later algebra on $A$, in that
% for any morphism of predomains $f : A \to UB$, there is a unique morphism of error domains
% $f^* : \li A \to \li A$ extending $f$.

There is a functor $U$ from error domains to predomains that on objects simply returns the
underlying predomain, and on morphisms returns the underlying morphism of predomains.
It is easily verified that $\li A$ is the free error- and later-algebra on the predomain $A$,
so we have that $\li$ is left-adjoint to $U$.
% i.e., error domain morphisms from $\li A$ to $B$ are in one-to-one correspondence with
% predomain morphisms from $A$ to $UB$.

% We define $\delta : U(\li A) \To U(\li A)$ by $\delta(x) = \theta(\nxt x)$.
% We define $\hat{\delta} : \li A \arr \li A$ by $\hat{\delta} = \ext{(\delta \circ \eta)}{}$.
% Note that by definition of $\text{ext}$, we have that $\hat{\delta}$ is a morphism of error domains.

%\subsubsection{Lock-Step Error Ordering}\label{sec:lock-step}

The partial order $\le_{\li A}$ is the lock-step error ordering defined by guarded recursion as follows:
%
\begin{itemize}
    \item 	$\eta\, x \le_{\li A} \eta\, y$ if $x \le_A y$.
    \item 	$\mho \le_{\li A} l$ for all $l$ 
    \item   $\theta\, \tilde{r} \le_{\li A} \theta\, \tilde{r'}$ if
            $\later_t (\tilde{r}_t \le_{\li A} \tilde{r'}_t)$
  \end{itemize}
%
The idea is that two computations $l$ and $l'$ are related if they are in
lock-step with regard to their intensional behavior, up to $l$ erroring.
Given a relation $R : A \rel A'$, we define in an analogous manner a heterogeneous
version of the lock-step error ordering between $\li R : \li A \rel \li A'$.
% We define the action of $\li$ on a relation $R$ between $A$ and $A'$ to be the
% ``heterogeneous" version of the lock-step error ordering.

% TODO action of \li on commuting squares

%\subsubsection{Weak Bisimilarity}\label{sec:weak-bisimilarity}
%
For a predomain $A$, we define a relation on $\li A$, called ``weak bisimilarity",
written $l \bisim l'$. Intuitively, we say $l \bisim l'$ if they are equivalent ``up to delay''.
The weak bisimilarity relation is defined by guarded recursion as follows:
%
\begin{align*}
  &\mho \bisim \mho \\
%
  &\eta\, x \bisim \eta\, y \text{ if } 
    x \bisim_A y \\
%		
  &\theta\, \tilde{x} \bisim \theta\, \tilde{y} \text{ if } 
    \later_t (\tilde{x}_t \bisim \tilde{y}_t) \\
%	
  &\theta\, \tilde{x} \bisim \mho \text{ if } 
    \theta\, \tilde{x} = \delta^n(\mho) \text { for some $n$ } \\
%	
  &\theta\, \tilde{x} \bisim \eta\, y \text{ if }
    (\theta\, \tilde{x} = \delta^n(\eta\, x))
  \text { for some $n$ and $x \in A$ such that $x \bisim_A y$ } \\
%
  &\mho \bisim \theta\, \tilde{y} \text { if } 
    \theta\, \tilde{y} = \delta^n(\mho) \text { for some $n$ } \\
%	
  &\eta\, x \bisim \theta\, \tilde{y} \text { if }
    (\theta\, \tilde{y} = \delta^n (\eta\, y))
  \text { for some $n$ and $y \in A$ such that $x \bisim_A y$ }
\end{align*}
%
When both sides are $\eta$, then we ensure that the underlying values are related
by the bisimilarity relation on $A$.
When one side is a $\theta$ and the other is $\eta x$ (i.e., one side steps),
we stipulate that the $\theta$-term runs to $\eta y$ where $x$ is bisimilar to $y$.
Similarly when one side is $\theta$ and the other $\mho$.
If both sides step, then we allow one time step to pass and compare the resulting terms.
In this way, the definition captures the intuition of terms being equivalent up to
delays.

% It can be shown (by \lob-induction) that the step-sensitive relation is symmetric.
% However, it can also be shown that this relation is \emph{not} transitive:
% The argument is the same as that used to show that the step-insensitive error
% ordering $\semltbad$ described above is not transitive. Namely, we show that
% if it were transitive, then it would have to be trivial in that $l \bisim l'$ for all $l, l'$.
% that if this relation were transitive, then it would relate all values of type $\li A$.


% internal hom for predomains and error domains
Given predomains $A$ and $A'$, we can form the predomain of
predomain morphisms from $A$ to $A'$, denoted $A \To A'$.
\begin{itemize}
    % Should we give the definition involving x and x'?
    \item The ordering is defined by $f \le_{A \To A'} f'$ iff for all
    $x \in A$, we have $f(x) \le_{A'} f'(x)$.
    \item The bisimilarity relation is defined by $f \bisim_{A \To A'} f'$ iff
    for all $x, x' \in A$ with $x \bisim_{A} x'$, we have $f(x) \bisim_{A'} f'(x')$. 
\end{itemize}
%
Given $f : A_1' \to A_1$ and $g : A_2 \to A_2'$ we define the predomain morphism
$f \To g : (A_1 \To A_2) \to (A_1' \To A_2')$ by $\lambda h. \lambda x'. g(h(f(x')))$.

% TODO: include this?
% The monadic extension operation $\ext{\cdot}{} : (A_1 \To U (\li A_2)) \To (\li A_1 \To U(\li A_2))$
% is a morphism of predomains from $A_1 \To U(\li A_2)$ to $U(\li A_1) \To U(\li A_2)$, i.e.,
% it preserves the ordering and bisimilarity relations.


% Given a predomain $A$ and error domain $B$, we define $A \arr B := A \To UB$.
We note that $A \To UB$ carries a natural error domain structure
(in the below, the lambda is a meta-theoretic notation):
\begin{itemize}
    \item The error is given by $\lambda x . \mho_B$
    \item The $\theta$ operation is defined by
      \[ \theta_{A \To UB}(\tilde{f}) = \lambda x . \theta_B(\lambda t . \tilde{f}_t(x)). \]
\end{itemize}

Given a predomain $A$ and error domain $B$, we define
$A \arr B$ to be the error domain such that $U(A \arr B) = A \To UB$,
and whose error and $\theta$ operations are as defined above.
We can define the functorial action of $\arr$ on morphisms
$f \arr \phi$ in the obvious way.
%
It is easily verified that $A \arr B$ is an exponential of $UB$ by $A$
in the category of predomains and their morphisms.

Lastly, given a relation of predomains $R$ between $A$ and $A'$, and a relation
of error domains $S$ between $B$ and $B'$, we define the relation $R \arr S$
between $A \arr B$ and $A' \arr B'$ in the obvious way, i.e., $f \in A \arr B$
is related to $g \in A' \arr B'$ iff for all $x \in A$ and $x' \in A'$ with
$x \mathrel{R} x'$, we have $f(x) \mathrel{S} g(x')$.
%
One can verify that this relation is indeed a relation of error domains
in that it respects error and preserves $\theta$.

With all of the above data, we can form a step-1 intensional model of gradual typing
(See Definition \ref{def:step-1-model}).

\subsection{The Dynamic Type}
The predomain representing the dynamic type will be defined using guarded recursion
as the solution to the equation
\footnote{In this section, we write $F$ instead of $\li$ so that the notation follows that of the abstract model section.}
%
\[ D \cong \mathbb{N}\, + (D \times D)\, + \laterhs U(D \arr FD). \]
%
% Note that the operators in the above equation are all combinators for predomains, so
% this also defines the ordering and the bisimilarity relation for $D$.

For the sake of clarity, we name the ``constructors" $\text{nat}$, $\text{times}$,
and $\text{fun}$, respectively.
%
We define $e_\mathbb{N} : \mathbb{N} \to D$ to be the injection into the first
component of the sum, and $e_\times : D \times D \to D$ to be the injection into
the second component of the sum, and $e_\to : U(D \arr F D)$ to be the morphism
$\nxt$ followed by the injection into the third component of the sum.

Explicitly, the ordering on $D$ is given by:
%
\begin{align*}
    \tnat(n) \le \tnat(n') 
        &\iff n = n' \\
    \ttimes (d_1, d_2) \le \ttimes (d_1', d_2')
        &\iff d_1 \le d_2 \text{ and } d_1' \le d_2'\\
    \tfun(\tilde{f}) \le \tfun(\tilde{f'}) 
        &\iff \later_t(\tilde{f}_t \le \tilde{f'}_t)
\end{align*}
%
We define a relation $\inat : \mathbb{N} \rel D$ by
$(n, d) \in \inat$ iff $e_\mathbb{N} \le_D d$.
We similarly define $\itimes : D \times D \rel D$ by
$((d_1, d_2), d) \in \itimes$ iff $e_\times(d_1, d_2) \le_D d$,
and we define $\text{inj}_\to : U(D \arr F D) \rel D$ by
$(f, d) \in \iarr$ iff $e_\to(f) \le_D d$.

Now we define the perturbations for $D$.
Recall from our construction of a model with perturbations
(Section \ref{sec:constructing-perturbations}) that for each value
type $A$ we associate a monoid $P_A$ of perturbations
and a homomorphism into the monoid of endomorphisms bisimilar to the identity,
and likewise for computation types.
We define the perturbations for $D$ via least-fixpoint in the category of monoids as
%
\( P_D \cong (P_{D \times D}) \times P_{U(D \to FD)}. \)
%
Unfolding the definitions, this is the same as
%
\( P_D \cong (P_D \times P_D) \times (\mathbb{N} \times P_D^{op} \times \mathbb{N} \times P_D). \)
%
We now explain how to interpret these perturbations as endomorphisms.
We define $\ptb_D : P_D \to \{ f : D \to D \mid f \bisim \id \}$ below,
% via the universal property of the coproduct of monoids, giving a case for each of the generators.
% In the below, note the use of the functorial action of $\arr$ on morphisms.
%
% \[ P_D \cong (P_D \times P_D) \times (P_D \times (\mathbb{N} \times P_D)), \]
%
\begin{align*}
 \ptb_D(p_{\text{times}}, p_{\text{fun}}) &= \lambda d.\text{case $d$ of}  \\
 &\alt \tnat(m) \mapsto \tnat(m) \\
    &\alt \ttimes(d_1, d_2) \mapsto {\ttimes(\ptb_{D \times D}(p_\text{times})(d_1, d_2))} \\
    &\alt \tfun(\tilde{f}) \mapsto {\tfun(\lambda t. \ptb_{U(D \to FD)}()(\tilde{f}_t))} \\
\end{align*}
    % \item $\ptb_D(1)$
    % \item $\ptb_D(\delta^K_D)$ is defined similarly to the previous but has
    % \[ \id \arr i^K(\delta^K_D) \] instead.
    % \item $\ptb_D(\delta^K_D) = \lambda d.\text{case $d$ of}$
    %   \begin{align*} 
    %     &\alt \ttimes(d_1, d_2) \mapsto {\ttimes(i^K(\delta^K_D)(d_1), d_2)} \\
    %     &\alt d' \to d'
    %   \end{align*}
    % \item $\ptb_D(\delta^K_D)$ is defined similarly to the previous but has 
    % \[ (d_1, \ptb_D(\delta^K_D)(d_2)) \] instead.
One can verify that this defines a homomorphism from $P_D \to \{ f : D \to D : f \bisim \id \}$.
We claim that the three relations $\inat$, $\itimes$, and $\iarr$
%and their lifted versions 
satisfy the push-pull property.
As an illustrative case, we establish the push-pull property for the relation $\iarr$.
We define $\pull_{\iarr} : P_D \to P_{U(D \arr FD)}$ by\( \pull_{\iarr}(p_{\text{times}}, p_{\text{fun}}) = p_{\text{fun}}, \)
% (recall that $P_{U(D \arr FD)} = \mathbb{N} \times P_D^{op} \times \mathbb{N} \times P_D$).
%
i.e., we simply forget the other perturbation.
%
We define $\push_{\iarr} : P_{U(D \arr FD)} \to P_D$ by \( \push{\iarr}(p_{\text{fun}}) = (\id, p_{\text{fun}}) \).
%
Showing that the relevant squares commute is straightforward.
%
% To do so, consider an arbitrary perturbation $p$ on $D$. 
% Let $(f, d) \in \iarr$. This means that $d$ must be of the form $\tfun{\tilde{f}}$. 
% When we interpret the perturbation on $D$, obtaining and endomorphism to which we then apply $d$,
% we will be perform the action that was performed by the perturbation on the other side and thus
% we will be done by our assumption that $f$ is related to $d$.


We next claim that the relations $\inat$, $\itimes$, and $\iarr$ are quasi-left-representable,
and that their lifts are quasi-right-representable.
Indeed, since the relations are functional, it is easy to see that they are quasi-left-representable
where the perturbations are taken to be the identity.
%
For quasi-right-representability, the most interesting case is $\li(\iarr)$.
Defining the projection $p_{\iarr} : FD \to FU(D \to FD)$ is equivalent to defining
$p' : D \to UFU(D \to FD)$. We define
\begin{align*}
 p' = \lambda d.\text{case $d$ of}   &\alt \tnat(m) \mapsto \mho \\
    &\alt \ttimes(d_1, d_2) \mapsto \mho \\
    &\alt \tfun(\tilde{f}) \mapsto \theta (\lambda t. \eta(\tilde{f}_t)).
\end{align*}
%
We define $\dellp_D = \delrp_D = \delta_{FD}$.
Then it is easy to show using the definition of $\iarr$ that the squares for $\dnl$ and $\dnr$ commute.
% Then for $\dnr$, we need to show that if $(f, d) \in \iarr$ then
%
It is also straightforward to establish the retraction property for
each of these three relations. In the case of $\iarr$, we
have that the property holds up to a delay.

% \subsection{Obtaining an Extensional Model}

Now that we have defined an intensional model with an interpretation for the dynamic type, we can apply
the abstract constructions introduced in Section \ref{sec:extensional-model-construction}.
Doing so, we obtain an extensional model of gradual typing, where the squares are given by the
``bisimilarity closure'' of the intensional error ordering.

\subsection{Adequacy}\label{sec:adequacy}

In this section, we prove an adequacy result for the concrete extensional model of GTT we obtained in the previous section.
applying the abstract constructions introduced in Section
\ref{sec:extensional-model-construction} to the concrete model built in the previous section.
%\ref{sec:concrete-model}.

First we establish some notation. Fix a morphism $f : 1 \to \li \mathbb{N} \cong \li \mathbb{N}$.
We write $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.
That is, we have $f \ltls g$ iff there exists $f'$ and $g'$ with
%
\[ f \bisim_{\li \mathbb{N}} f' \le_{\li \mathbb{N}} g' \bisim_{\li \mathbb{N}} g. \]
%
Here $\le_{\li \mathbb{N}}$ is the lock-step error ordering, and
$\bisim_{\li \mathbb{N}}$ is weak bisimilarity.
First observe that in this ordering, the semantics of error is not equivalent to
the semantics of the diverging term.
The main result we would like to show is as follows:
\begin{lemma}
If $f \ltls g : \li \mathbb{N}$, 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$ or $f \da \mho$.
\end{itemize}
\end{lemma}
%
Unfortunately, this 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 the above result 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 out the underlying number.
%
Thus, to prove our adequacy result, we need to leave the guarded setting and pass back
to the more familiar, set-theoretic world with no internal notion of step-indexing.
We can do this using a process known as \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 have taken place with respect to this clock.
For example, recall the definition of the lift monad by guarded recursion.
% 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 known as \emph{clock-irrelevance},
\footnote{A type $X$ is clock-irrelevant if there is an isomorphism $\forall k.X \cong X$.}
we can define the ``global lift'' monad as $\li^{gl} X := \forall k. \li^k X$.

It can be shown that there is an isomorphism between the global lift monad and the
delay monad of Capretta \cite{lmcs:2265}.
Recall that, given a type $X$, the delay monad $\text{Delay}(X)$ is defined as the coinductive
type generated by 
$\tnow : X \to \delay(X)$ and $\tlater : \delay(X) \to \delay(X)$.

% solution to the equation

% \[ \text{Delay}(X) \cong X + \text{Delay}(X). \]

It can be shown that for a clock-irrelevant type $X$, $\li^{gl} X$ is a final
coalgebra of the functor $F(Y) = X + 1 + Y$ (For example, this follows from Theorem 4.3 in
\cite{kristensen-mogelberg-vezzosi2022}.) 
\footnote{The proof relies on the existence of an operation  
$\mathsf{force} : \forall k. \later^k A \to \forall k. X$ that
allows us to eliminate the later operator under a clock quantifier.
This must be added as an axiom in guarded type theory.}
Since $\delay(X + 1)$ is also a final coalgebra
of this functor, then we have $\li^{gl} X \cong \delay(X + 1)$.

Given a predomain $X$ on a clock-irrelevant type, we can define a
``global'' version of the lock-step error ordering and the
weak bisimilarity relation on elements of the global lift; the former is defined by
%
\( x \le^{gl}_X y := \forall k. x[k] \le y[k], \)
%
and the latter is defined by
%
\( x \bisim^{gl}_X y := \forall k. x[k] \bisim y[k]. \)
%
On the other hand, we can define coinductively a ``lock-step error ordering"
relation on $\delay(X + 1)$:
%
\begin{mathpar}
  \inferrule*[]
  { }
  {\tnow (\inr\, 1) \ledelay d}

  \inferrule*[]
  {x_1 \le_X x_2}
  {\tnow (\inl\, x_1) \ledelay \tnow (\inl\, x_2)}

  \inferrule*[]
  {d_1 \ledelay d_2}
  {\tlater\, d_1 \ledelay \tlater\, d_2}
\end{mathpar}
%
And we similarly define by coinduction a ``weak bisimilarity'' relation on $\delay(X + 1)$, which uses
a relation $d \Da x_?$ between $\delay(X+1)$ and $X+1$ that is defined as 
$d \Da x_? := \Sigma_{m \in \mathbb{N}} d = \tlater^m(\tnow\, x_?)$.
Then weak bisimilarity is defined by the rules
%
\begin{mathpar}
  \inferrule*[]
  {x_? \bisim_{X + 1} y_?}
  {\tnow\, x_? \bisimdelay \tnow\, y_? }

  \inferrule*[]
  {d_1 \Da x_? \and x_? \bisim_{X + 1} y_?}
  {\tlater\, d_1 \bisimdelay \tnow\, y_? }

  \inferrule*[]
  {d_2 \Da y_? \and x_? \bisim_{X + 1} y_?}
  {\tnow\, x_? \bisimdelay \tlater\, d_2}

  \inferrule*[]
  {d_1 \bisimdelay d_2}
  {\tlater\, d_1 \bisimdelay \tlater\, d_2 }

  % \inferrule*[]
  % {d_1 \Da x_? \and d_2 \Da y_? \and x_? \bisim_{X + 1} y_?}
  % {d_1 \bisimdelay d_2}

  % \inferrule*[]
  % {d_1 \bisimdelay d_2}
  % {\tlater d_1 \bisimdelay \tlater d_2 }

\end{mathpar}
%
Note the similarity of these definitions to the corresponding guarded definitions.
By adapting the aforementioned theorem to the setting of inductively-defined relations,
we can show that both the global lock-step error ordering and the global weak bisimilarity
admit coinductive definitions. In particular, modulo the above isomorphism
between $\li^{gl} X$ and $\delay(X+1)$, the global version of the lock-step
error ordering is equivalent to the lock-step error ordering on $\delay(X + 1)$,
and likewise, the global version of the weak bisimilarity relation is equivalent to the
weak bisimilarity relation on $\delay(X + 1)$.

This implies that the global version of the extensional term precision semantics for
$\li^{gl} X$ agrees with the corresponding notion for $\delay(X + 1)$.
Then adequacy follows by proving the corresponding
result for $\delay(X + 1)$ which in turn follows from the definitions of the relations.


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

% Need : nat is clock irrelevant, as well as the inputs and outputs of effects
% Axioms about forcing clock
% Adapt prior argument to get that the defining of the global bisim
% and global lock-step error ordering are coinductive