diff --git a/paper-new/appendix.tex b/paper-new/appendix.tex
new file mode 100644
index 0000000000000000000000000000000000000000..af3a4412cca5b670143df3459faab39c852c7906
--- /dev/null
+++ b/paper-new/appendix.tex
@@ -0,0 +1,145 @@
+\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$.
+
diff --git a/paper-new/paper.tex b/paper-new/paper.tex
index 2083da00ab5eb4102ada6232b8bf4561845bda84..0f96c9798689bad50f4463da3dfc757df6d67fa2 100644
--- a/paper-new/paper.tex
+++ b/paper-new/paper.tex
@@ -146,6 +146,14 @@
\input{discussion}
+
+\bibliographystyle{ACM-Reference-Format}
+\bibliography{references}
+
+\appendix
+\input{appendix}
+
+
% \section{Discussion}\label{sec:discussion}
% \subsection{Synthetic Ordering}
@@ -162,7 +170,4 @@
% treatment of the error ordering as well.
-\bibliographystyle{ACM-Reference-Format}
-\bibliography{references}
-
\end{document}