diff --git a/paper/gtt.tex b/paper/gtt.tex
index 3b8ec9ef71a597076cfd12802728072f007be019..1d666bfbb0264a7172ba71736fb4c3cdaf444548 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2364,7 +2364,7 @@ value and one when the continuation is a term.
   \end{enumerate}
 \end{proof}
 
-\begin{corollary}[Hom-set formulation of EP Pairs]
+\begin{corollary}[Hom-set formulation of Adjunction]
   For any value embedding-projection pair $V_e,S_p$ from $A$ to $A'$,
   the following are equivalent:
   \begin{mathpar}
@@ -2512,6 +2512,174 @@ TODO: we don't ``need'' this lemma, except to show that GTT is an
   term in a stack (use substitution for the target, decomposition)
 \end{lemma}
 
+\begin{theorem}[Axiomatic Graduality]
+  Let $\rho$ be a dynamic type interpretation. Then the following are true,
+  \begin{mathpar}
+    \inferrule
+    {\Phi : \Gamma \ltdyn \Gamma'\\
+      \Psi : \Delta \ltdyn \Delta'\\
+      \Phi \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
+    {\sem\Gamma \pipe \sem{\Delta'} \vdash \sem M[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]] : \sem{\u B}}
+
+    \inferrule
+    {\Phi : \Gamma \ltdyn \Gamma' \\
+      \Phi \vdash V \ltdyn V' : A \ltdyn A'}
+    {\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn\sem{V'}[\sem\Phi] : \sem {A'}}
+  \end{mathpar}
+\end{theorem}
+\begin{proof}
+  By mutual induction over term dynamism derivations. For the $\beta,
+  \eta$ and reflexivity rules, we use the identity expansion lemma
+  (TODO ref).
+
+  For compatibility rules a pattern emerges.  For universal rules
+  (positive intro, negative elim) are easy, don't need to reason about
+  casts at all. For ``(co)-pattern matching rules'' (positive elim,
+  negative intro), a cast needs to be introduced at a redex and we
+  need to use the \emph{projection} property of casts.  Fortunately,
+  all reasoning about ``shifted'' casts is handled in lemmas, here we
+  only deal with ``nice'' casts.
+  \begin{enumerate}
+    %%  Logical rules:
+  \item TODO: Transitivity
+  \item TODO: Substitution
+  \item TODO: Variables
+  \item TODO: Hole
+    %% Error Rules
+  \item TODO: error is bottom
+  \item TODO: error strictness
+    %% Cast Rules
+  \item TODO: UpCast-L
+  \item TODO: UpCast-R
+  \item TODO: DnCast-R
+  \item TODO: DnCast-L
+    %% Value Compat Rules
+  \item TODO: $0$ elim
+  \item TODO: $+$ intro
+  \item TODO: $+$ elim
+  \item TODO: $1$ intro
+  \item TODO: $1$ elim
+  \item TODO: $\times$ intro
+  \item TODO: $\times$ elim
+  \item TODO: $U$ intro
+  \item TODO: $U$ elim
+    %% Computation Compat Rules
+  \item $\top$ intro:
+    \[
+    \inferrule{}{\{\} \ltdyn \sdncast{\top}{\top}[\{\}]}
+    \]
+    Immediate by $\top\eta$
+  \item $\with$ intro:
+    \[
+    \inferrule
+    {\sem{M_1}[\sem{\Psi}]\ltdyn \sdncast{\u B_1}{\u B_1'}[\sem{M_1'}[\sem{\Phi}]]\\
+     \sem{M_2}[\sem{\Psi}]\ltdyn \sdncast{\u B_2}{\u B_2'}[\sem{M_2'}[\sem{\Phi}]]}
+    {\pair{\sem{M_1}[\sem{\Psi}]}{\sem{M_2}[\sem{\Psi}]}
+    \ltdyn
+    \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]}
+    \]
+    We proceed as follows:
+    \begin{align*}
+      &\pair{\sem{M_1}[\sem{\Psi}]}{\sem{M_2}[\sem{\Psi}]}\\
+      &\ltdyn
+      \pair{\sdncast{\u B_1}{\u B_1'}[\sem{M_1'}[\sem{\Phi}]]}{\sdncast{\u B_2}{\u B_2'}[\sem{M_2'}[\sem{\Phi}]]}\tag{IH}\\
+      &\equidyn
+      \pairone{\pi\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]}\tag{cast reduction}\\
+      &\quad \pairtwo{\pi'\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]}\\
+      &\equidyn
+      \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\pair{\sem{M_1'}[\sem{\Phi}]}{\sem{M_2'}[\sem{\Phi}]}]\tag{$\with\eta$}
+    \end{align*}
+  \item $\with$ elim, we show the $\pi$ case, $\pi'$ is symmetric:
+    \[
+    \inferrule
+    {\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sem{M'}[\sem{\Phi}]]}
+    {\pi\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B_1}{\u B_1'}[\pi\sem{M'}[\sem{\Phi}]]}
+    \]
+    We proceed as follows:
+    \begin{align*}
+      \pi\sem{M}[\sem{\Psi}]
+      &\ltdyn \pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sem{M'}[\sem{\Phi}]]\tag{IH}\\
+      &\equidyn
+      \sdncast{\u B_1}{\u B_1'}[\pi\sem{M'}[\sem{\Phi}]]\tag{cast reduction}
+    \end{align*}
+  \item
+    \[
+    \inferrule
+    {\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}][\supcast{A}{A'}{x}/x']]}
+    {\lambda x:A. \sem{M}[\sem{\Psi}] \ltdyn \sdncast{A \to \u B}{A'\to\u B'}[\lambda x':A'. \sem{M'}[\sem{\Phi}]]}
+    \]
+    We proceed as follows:
+    \begin{align*}
+      &\lambda x:A. \sem{M}[\sem{\Psi}]\\
+      &\ltdyn
+      \lambda x:A. \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}][\supcast{A}{A'}{x}/x']]\tag{IH}\\
+      &\equidyn
+      \lambda x:A. (\sdncast{A \to \u B}{A' \to \u B'}[\lambda x'. \sem{M'}[\sem{\Phi}]])\, x\tag{cast reduction}\\
+      &\equidyn
+      \sdncast{A \to \u B}{A' \to \u B'}[\lambda x'. \sem{M'}[\sem{\Phi}]]\tag{$\to\eta$}
+    \end{align*}
+  \item We need to show
+    \[
+    \inferrule
+    {\sem{M}[\sem{\Psi}] \ltdyn \sdncast{A \to \u B}{A' \to \u B'}[\sem{M'}[\sem{\Phi}]]\\
+     \supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}]}
+    {\sem{M}[\sem{\Psi}]\,\sem{V} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]\, \sem{V'}[\sem{\Phi}]]}
+    \]
+    We proceed:
+    \begin{align*}
+      &\sem{M}[\sem{\Psi}]\,\sem{V}\\
+      &\ltdyn
+      (\sdncast{A \to \u B}{A' \to \u B'}[\sem{M'}[\sem{\Phi}]])\,\sem{V}\tag{IH}\\
+      &\equidyn
+      \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]\,(\supcast{A}{A'}{\sem{V}})]\tag{cast reduction}\\
+      &\ltdyn
+      \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]\,\sem{V'}[\sem{\Phi}]] \tag{IH}
+    \end{align*}
+  \item We need to show
+    \[
+    \inferrule
+    {\supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}]}
+    {\ret\sem{V}\ltdyn \sdncast{\u F A}{\u FA'}[\ret\sem{V'}[\sem{\Phi}]]}
+    \]
+    By hom-set definition of adjunction (TODO ref)
+  \item We need to show
+    \[
+    \inferrule
+    {\sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u F A}{\u F A'}[\sem{M'}[\Phi]]\\
+      \sem{N} \ltdyn \sdncast{\u B}{\u B'}[\sem{N}[\Phi][\supcast{A}{A'} x/x']]}
+    {\bindXtoYinZ {\sem{M}[\sem{\Psi}]} x {\sem{N}}
+    \ltdyn
+    \sdncast{\u B}{\u B'}[{\bindXtoYinZ {\sem{M'}[\sem{\Phi}]} {x'} {\sem{N'}[\sem{\Phi}]}}]}
+    \]
+    We proceed:
+    \begin{align*}
+      &\bindXtoYinZ {\sem{M}[\sem{\Psi}]} x {\sem{N}}\\
+      &\ltdyn \bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\sem{M'}[\Phi]]} x \sdncast{\u B}{\u B'}[\sem{N}[\Phi][\supcast{A}{A'} x/x']] \tag{IH, congruence}\\
+      &\equidyn
+      \bindXtoYinZ {\sdncast{\u F A}{\u F A'}[\sem{M'}[\Phi]]} x\\
+      &\qquad \bindXtoYinZ {\ret\supcast{A}{A'}[x]} {x'}
+      \sdncast{\u B}{\u B'}[\sem{N}[\Phi]] \tag{$\u F\beta$}\\
+      & \ltdyn \bindXtoYinZ {\sem{M'}[\Phi]} {x'} \sdncast{\u B}{\u B'}[\sem{N}[\Phi]] \tag{Projection}\\
+      & \equidyn  \sdncast{\u B}{\u B'}[\bindXtoYinZ {\sem{M'}[\Phi]} {x'} \sem{N}[\Phi]] \tag{commuting conversion}
+    \end{align*}
+  \end{enumerate}
+\end{proof}
+
+\begin{lemma}[Conservativity]
+  If the types of the two terms in dynamism judgment are the same,
+  then that implies an ordering in CBPV between their translations
+  (with no casts inserted).
+  \begin{mathpar}
+    \inferrule
+    {\Gamma \ltdyn \Gamma \vdash M_1 \ltdyn M_2 : \u B \ltdyn \u B}
+    {\sem\Gamma \vdash \sem{M_1} \ltdyn \sem{M_2} : \sem{\u B}}
+  \end{mathpar}
+\end{lemma}
+\begin{proof}
+  By axiomatic graduality and the fact that identity casts are
+  identities.
+\end{proof}
+
 \begin{figure}
   \begin{mathpar}
   \begin{array}{rcl}