when an F meets a U

code/gcbpv.agda

@@ -163,96 +163,30 @@ vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map vrefl (VCtx.vty
 
 record VCtxTC : Set where
   field
-    Γ⊤ : VCtx onevar
-    Γ⊥ : VCtx onevar
-    eqvars : Vars Γ⊤ ≡ Vars Γ⊥
-    eqδ    : Vec VTC (VCtx.Vars Γ⊤)
-open VCtxTC
+    Vars : ℕ
+    vty  : Vec VTC Vars
 
+Γ⊤ : VCtxTC -> VCtx onevar
+Γ⊤ Γsq = vctx (VCtxTC.Vars Γsq) (map VTC.A⊤ (VCtxTC.vty Γsq))
 
--- eq-to-compvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥
--- eq-to-compvars Γ⊤ Γ⊥ eq =
---   begin VCtx.Vars Γ⊤
---     ≡⟨ refl ⟩
---     VCtx.Vars (Γ⊤ ⟪ Bot ⟫v)
---     ≡⟨ cong VCtx.Vars eq ⟩
---     VCtx.Vars (Γ⊥ ⟪ Top ⟫v)
---     ≡⟨ refl ⟩
---     VCtx.Vars Γ⊥
---   ∎
-
--- lemlem : forall {I} Vars (vty1 : Vars -> VType I) vty2 -> record { Vars = Vars ; vty = vty1 } ≡ record { Vars = Vars; vty = vty2 } -> vty1 ≡ vty2
--- lemlem Vars vty1 vty2 refl = refl
-
--- lem : ∀ (Γ⊥ : VCtx onevar) ->
---         (Γ⊤ : VCtx onevar) ->
---       (p  : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) -> 
---       (x : VCtx.Vars Γ⊤) -> 
---       VCtx.vty (Γ⊤ ⟪ Bot ⟫v) x ≡ VCtx.vty (Γ⊥ ⟪ Top ⟫v) (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x)
--- lem Γ⊥ Γ⊤ p x with (eq-to-compvars Γ⊤ Γ⊥ p)
--- lem Γ⊥ record { Vars = .(VCtx.Vars Γ⊥) ; vty = vty⊤ } p Vars⊥ | refl =
---   begin
---     vty⊤ Vars⊥ ⟨ Bot ⟩v
---     ≡⟨ refl ⟩
---     VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = λ x → vty⊤ x ⟨ Bot ⟩v }) Vars⊥
---     ≡⟨ cong (λ x → VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = x }) Vars⊥) (lemlem (VCtx.Vars Γ⊥) (λ z → vty⊤ z ⟨ Bot ⟩v) ((λ x → VCtx.vty Γ⊥ x ⟨ Top ⟩v)) p) ⟩
---     VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = λ x → VCtx.vty Γ⊥ x ⟨ Top ⟩v }) Vars⊥
---     ≡⟨ refl ⟩
---     VCtx.vty Γ⊥ Vars⊥ ⟨ Top ⟩v
---   ∎
-
--- mkeqvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> Vars Γ⊤ ≡ Vars Γ⊥
--- mkeqvars Γ⊤ Γ⊥ p = 
---     begin
---       Vars Γ⊤
---       ≡⟨ refl ⟩
---       Vars (Γ⊤ ⟪ Bot ⟫v)
---       ≡⟨ cong Vars p ⟩
---       Vars (Γ⊥ ⟪ Top ⟫v)
---       ≡⟨ refl ⟩
---       Vars Γ⊥
---     ∎
+Γ⊥ : VCtxTC -> VCtx onevar
+Γ⊥ Γsq = vctx (VCtxTC.Vars Γsq) (map VTC.A⊥ (VCtxTC.vty Γsq))
 
+vctxtrans : VCtxTC -> VCtx onevar
+vctxtrans Γsq = vctx (VCtxTC.Vars Γsq) (map vtrans (VCtxTC.vty Γsq))
 
--- eq-to-comp : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VctxTransComp Γ⊤ Γ⊥
--- eq-to-comp Γ⊤ Γ⊥ p = record {
---   eqvars = mkeqvars Γ⊤ Γ⊥ p;
---   eqδ = tabulate λ x⊤ → record {
---     A⊤ = lookup x⊤ (vty Γ⊤) ;
---     A⊥ = lookup (subst Fin (mkeqvars Γ⊤ Γ⊥ p)  x⊤) (vty Γ⊥) ;
---     compat =
---       begin
---         lookup x⊤ (vty Γ⊤) ⟨ Bot ⟩v
---         ≡⟨ sym (lookup-map x⊤ (λ z → z ⟨ Bot ⟩v) (vty Γ⊤)) ⟩
---         lookup x⊤ (vty (Γ⊤ ⟪ Bot ⟫v))
---         ≡⟨ cong (lookup x⊤) {!p!} ⟩
---         lookup x⊤ (subst (Vec (VType _)) _ (vty (Γ⊥ ⟪ Top ⟫v)))
---         ≡⟨ {!!} ⟩
---         lookup (subst Fin _ x⊤) (vty (Γ⊥ ⟪ Top ⟫v))
---         ≡⟨ lookup-map _ (\z -> z ⟨ Top ⟩v) (vty Γ⊥) ⟩
---         lookup (subst Fin _ x⊤) (vty Γ⊥) ⟨ Top ⟩v
---       ∎
---     }
---   }
---   record {
---   SameVar = VCtx.Vars Γ⊤ ;
---   eq⊤ = refl ;
---   eq⊥ = eq-to-compvars Γ⊤ Γ⊥ p ;
---   eqδ = λ x →
---     begin
---       VCtx.vty Γ⊤ x ⟨ Bot ⟩v
---       ≡⟨ refl ⟩
---       VCtx.vty (Γ⊤ ⟪ Bot ⟫v) x
---       ≡⟨ lem Γ⊥ Γ⊤ p x ⟩
---       VCtx.vty (Γ⊥ ⟪ Top ⟫v) (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x)
---       ≡⟨ refl ⟩
---       VCtx.vty Γ⊥ (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x) ⟨ Top ⟩v
---     ∎
---   }
+lem' : ∀ Asq -> vtrans Asq ⟨ Top ⟩v ≡ VTC.A⊤ Asq ⟨ Top ⟩v
+lem' Asq = refl
 
-vctxtrans : VCtxTC -> VCtx onevar
-vctxtrans record { Γ⊤ = Γ⊤ ; Γ⊥ = Γ⊥ ; eqvars = eqvars ; eqδ = eqδ } =
- vctx (VCtx.Vars Γ⊤) (map vtrans eqδ)
+lem : ∀ Γsq -> (vctxtrans Γsq ⟪ Top ⟫v) ≡ ((Γ⊤ Γsq) ⟪ Top ⟫v)
+lem Γsq =
+  begin
+    vctxtrans Γsq ⟪ Top ⟫v
+    ≡⟨ {!!} ⟩
+    vctxtrans Γsq ⟪ Top ⟫v
+    ≡⟨ {!!} ⟩
+    Γ⊤ Γsq ⟪ Top ⟫v
+  ∎
 
 CCtx : DCtx -> Set
 CCtx I = StCtx (CType I)
@@ -282,8 +216,8 @@ record ValTC where
   field
     ΓΓ : VCtxTC
     AA : VTC
-    V⊤ : Value (VCtxTC.Γ⊤ ΓΓ) (VTC.A⊤ AA)
-    V⊥ : Value (VCtxTC.Γ⊥ ΓΓ) (VTC.A⊥ AA)
+    V⊤ : Value (Γ⊤ ΓΓ) (VTC.A⊤ AA)
+    V⊥ : Value (Γ⊥ ΓΓ) (VTC.A⊥ AA)
 
 data Value where
   var : forall {I} (Γ : VCtx I) (x : Fin (VCtx.Vars Γ)) A -> A ≡ lookup x (VCtx.vty Γ) -> Value Γ A
@@ -312,7 +246,8 @@ vunit Γ ⟨ i ⟩vv = vunit (Γ ⟪ i ⟫v)
 vpair V V' ⟨ i ⟩vv = vpair (V ⟨ i ⟩vv) (V' ⟨ i ⟩vv)
 vdestr V Vk ⟨ i ⟩vv = vdestr (V ⟨ i ⟩vv) (Vk ⟨ i ⟩vv)
 vthunk M ⟨ i ⟩vv = vthunk (M ⟨ i ⟩cc)
-valtrans sq ⟨ Top ⟩vv = {!!}
+valtrans sq ⟨ Top ⟩vv with lem (ValTC.ΓΓ sq)
+... | q = {!!} -- subst (λ Γ⊤ → {!Value Γ⊤ ?!}) q ((ValTC.V⊤ sq) ⟨ Top ⟩vv)
 valtrans sq ⟨ Bot ⟩vv = {!!}
 
 data Term where
@@ -364,3 +299,83 @@ termrefl (app M V) = app (termrefl M) (valrefl V)
 termrefl (force V) = force (valrefl V)
 termrefl (ret V) = ret (valrefl V)
 termrefl (lett M Mk) = lett (termrefl M) ((termrefl Mk))
+
+-- eq-to-compvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥
+-- eq-to-compvars Γ⊤ Γ⊥ eq =
+--   begin VCtx.Vars Γ⊤
+--     ≡⟨ refl ⟩
+--     VCtx.Vars (Γ⊤ ⟪ Bot ⟫v)
+--     ≡⟨ cong VCtx.Vars eq ⟩
+--     VCtx.Vars (Γ⊥ ⟪ Top ⟫v)
+--     ≡⟨ refl ⟩
+--     VCtx.Vars Γ⊥
+--   ∎
+
+-- lemlem : forall {I} Vars (vty1 : Vars -> VType I) vty2 -> record { Vars = Vars ; vty = vty1 } ≡ record { Vars = Vars; vty = vty2 } -> vty1 ≡ vty2
+-- lemlem Vars vty1 vty2 refl = refl
+
+-- lem : ∀ (Γ⊥ : VCtx onevar) ->
+--         (Γ⊤ : VCtx onevar) ->
+--       (p  : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) -> 
+--       (x : VCtx.Vars Γ⊤) -> 
+--       VCtx.vty (Γ⊤ ⟪ Bot ⟫v) x ≡ VCtx.vty (Γ⊥ ⟪ Top ⟫v) (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x)
+-- lem Γ⊥ Γ⊤ p x with (eq-to-compvars Γ⊤ Γ⊥ p)
+-- lem Γ⊥ record { Vars = .(VCtx.Vars Γ⊥) ; vty = vty⊤ } p Vars⊥ | refl =
+--   begin
+--     vty⊤ Vars⊥ ⟨ Bot ⟩v
+--     ≡⟨ refl ⟩
+--     VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = λ x → vty⊤ x ⟨ Bot ⟩v }) Vars⊥
+--     ≡⟨ cong (λ x → VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = x }) Vars⊥) (lemlem (VCtx.Vars Γ⊥) (λ z → vty⊤ z ⟨ Bot ⟩v) ((λ x → VCtx.vty Γ⊥ x ⟨ Top ⟩v)) p) ⟩
+--     VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = λ x → VCtx.vty Γ⊥ x ⟨ Top ⟩v }) Vars⊥
+--     ≡⟨ refl ⟩
+--     VCtx.vty Γ⊥ Vars⊥ ⟨ Top ⟩v
+--   ∎
+
+-- mkeqvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> Vars Γ⊤ ≡ Vars Γ⊥
+-- mkeqvars Γ⊤ Γ⊥ p = 
+--     begin
+--       Vars Γ⊤
+--       ≡⟨ refl ⟩
+--       Vars (Γ⊤ ⟪ Bot ⟫v)
+--       ≡⟨ cong Vars p ⟩
+--       Vars (Γ⊥ ⟪ Top ⟫v)
+--       ≡⟨ refl ⟩
+--       Vars Γ⊥
+--     ∎
+
+
+-- eq-to-comp : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VctxTransComp Γ⊤ Γ⊥
+-- eq-to-comp Γ⊤ Γ⊥ p = record {
+--   eqvars = mkeqvars Γ⊤ Γ⊥ p;
+--   eqδ = tabulate λ x⊤ → record {
+--     A⊤ = lookup x⊤ (vty Γ⊤) ;
+--     A⊥ = lookup (subst Fin (mkeqvars Γ⊤ Γ⊥ p)  x⊤) (vty Γ⊥) ;
+--     compat =
+--       begin
+--         lookup x⊤ (vty Γ⊤) ⟨ Bot ⟩v
+--         ≡⟨ sym (lookup-map x⊤ (λ z → z ⟨ Bot ⟩v) (vty Γ⊤)) ⟩
+--         lookup x⊤ (vty (Γ⊤ ⟪ Bot ⟫v))
+--         ≡⟨ cong (lookup x⊤) {!p!} ⟩
+--         lookup x⊤ (subst (Vec (VType _)) _ (vty (Γ⊥ ⟪ Top ⟫v)))
+--         ≡⟨ {!!} ⟩
+--         lookup (subst Fin _ x⊤) (vty (Γ⊥ ⟪ Top ⟫v))
+--         ≡⟨ lookup-map _ (\z -> z ⟨ Top ⟩v) (vty Γ⊥) ⟩
+--         lookup (subst Fin _ x⊤) (vty Γ⊥) ⟨ Top ⟩v
+--       ∎
+--     }
+--   }
+--   record {
+--   SameVar = VCtx.Vars Γ⊤ ;
+--   eq⊤ = refl ;
+--   eq⊥ = eq-to-compvars Γ⊤ Γ⊥ p ;
+--   eqδ = λ x →
+--     begin
+--       VCtx.vty Γ⊤ x ⟨ Bot ⟩v
+--       ≡⟨ refl ⟩
+--       VCtx.vty (Γ⊤ ⟪ Bot ⟫v) x
+--       ≡⟨ lem Γ⊥ Γ⊤ p x ⟩
+--       VCtx.vty (Γ⊥ ⟪ Top ⟫v) (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x)
+--       ≡⟨ refl ⟩
+--       VCtx.vty Γ⊥ (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x) ⟨ Top ⟩v
+--     ∎
+--   }

gcbpv.tex

@@ -42,6 +42,7 @@
 \newcommand{\M}{\mathcal{M}}
 \newcommand{\sq}{\square}
 \newcommand{\lett}{\text{let}\,\,}
+\newcommand{\too}{\text{to}\,\,}
 \newcommand{\case}{\text{case}\,\,}
 \newcommand{\ret}{\text{ret}\,\,}
 \newcommand{\thunk}{\text{thunk}\,\,}
@@ -315,6 +316,8 @@ dynamism.
   \caption{Upcasts and Downcasts (Would be simpler with a Stoup)}
 \end{figure}
 
+\subsection{Exponentials}
+
 Next, we add the $\u F$ and $U$ types that mediate between the worlds
 of values and computations. The $\u F$ type takes a value type and
 makes the computation type of ``things that may eventually return
@@ -511,14 +514,9 @@ from a preordering.
   {x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash x_1 \ltdyn \thunk \dncast {\u B_1}{\u B_2} \force x_2 : U \u B_1}
 \end{mathpar}
   \caption{Functoriality Preserves Representability (Proofs)}
-  
 \end{figure}
 
-It seems like the easiest thing to do is have a most dynamic function
-type and product type, but I'm not sure if it's really necessary.
-%
-Explore this in the models.
-
+\subsection{Dynamic Types}
 \begin{figure}[H]
   \begin{mathpar}
     \inferrule{}{\dynv \vtype}
@@ -880,9 +878,9 @@ the domain and plug into the downcast for the result type.
       \ret (x,x_1')\\\\
 
       \upcast{U(A_1 \to \u B)}{U(A_2 \to \u B)}f_{\to} &\equidyn&
-      \thunk\lambda (x_2 : A_2). \lett x_1 = \dncast{A_1}{A_2}\ret x_2; (\force f_{\to})(x_1)\\
+      \thunk\lambda (x_2 : A_2). \lett x_1 = \dncast{\u F A_1}{\u F A_2}\ret x_2; (\force f_{\to})(x_1)\\
       \upcast{U(A \to \u B_1)}{U(A \to \u B_2)}f_{\to} &\equidyn&
-      \thunk\lambda (x : A). \force \upcast{\u B_1}{\u B_2}\thunk ((\force f_{\to})(x_1))\\\\
+      \thunk\lambda (x : A). \force \upcast{U \u B_1}{U \u B_2}\thunk ((\force f_{\to})(x_1))\\\\
 
       \dncast{\u F (A_1 \times A_1')}{\u F(A_2 \times A_1')}
       &\equidyn& \dncast{\u F (A_1 \times A_1')}{\u F(A_2 \times A_1')} \dncast{\u F (A_2 \times A_1')}{\u F(A_2 \times A_2')}\\
@@ -897,6 +895,95 @@ the domain and plug into the downcast for the result type.
   \caption{Function and Product "Expat" Directions, one side at a time}
 \end{figure}
 
+\subsection{Exponentials}
+
+To summarize what we've done so far: we show that all of the ``nice''
+connectives give an obvious uniquness principle for their ``natural''
+cast: nice value connectives give upcasts and nice computation
+connectives give downcasts.
+
+The $\u F$ and $U$ types are \emph{not nice} in that they both have a
+\emph{covariant} argument of \emph{the opposite sort}.
+%
+The reason this is troublesome is when we go to make a semantics, for
+a nice type like product if we try to design an upcast, the type
+constructor says:
+
+\begin{mathpar}
+  \inferrule
+  {A_1 \ltdyn A_1' \and A_2 \ltdyn A_2'}
+  {A_1 \times A_2 \ltdyn A_1' \times A_2'}
+\end{mathpar}
+
+and since $A \ltdyn A'$ denotes an upcast $\upcast{A}{A'}$, and
+$\times$ is covariant, we can apply the functoriality of $\times$.
+
+However, $\u F$ and $U$ are \emph{covariant} types, but if we look one
+level up we don't get a useful assumption:
+\begin{mathpar}
+  \inferrule
+  {A \ltdyn A'}
+  {\u F A \ltdyn \u F A'}
+\end{mathpar}
+
+So given an upcast $\upcast A {A'}$ we are tasked with constructing a
+downcast $\dncast{\u F A}{\u F A'}$, but since $\u F$ is covariant
+there is no way to proceed.
+%
+But to summarize the previous sections, we've shown that we can derive
+implementations for upcasts/downcasts for $\u F$ and $U$ on a
+case-by-case basis for each connective.
+
+So instead of the above we had
+\begin{mathpar}
+  \inferrule*
+  {\inferrule{A_1 \ltdyn A_1'\and A_2\ltdyn A_2'}{A_1\times A_2 \ltdyn A_1' \times A_2'}}
+  {\u F(A_1 \times A_2) \ltdyn \u F (A_1' \times A_2')}
+\end{mathpar}
+
+And at this point we have shown this is true for every connective
+\emph{except} the exponentials themselves.
+%
+So in order to produce a ``full'' implementation, we need to know what
+the casts between $U \u F A$s and $\u F U \u B$s look like
+respectively.
+%
+Fortunately, at this point there \emph{is} an obvious answer because
+now we have doubly negated: since $U$ and $\u F$ are both functors we
+can get candidates by applying their functoriality twice.
+%
+And this is correct because as we explained earlier, all functors
+preserve representability.
+
+However, here is a more direct syntactic proof.
+
+\begin{figure}
+  \inferrule
+  {A_1 \ltdyn A_2}
+  {x_1 : U \u F A_1 \vdash \upcast{U\u F A_1}{U\u F A_2}x_1 \equidyn \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1)}
+
+  \inferrule
+  {\inferrule
+  {y_2 \ltdyn \upcast{A_1}{A_2}y_1}
+  {\thunk (\lett y_1 = \force x_1; \ret y_1) \ltdyn \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1)}}
+  {x_1 : U \u F A_1 \vdash \upcast{U\u F A_1}{U\u F A_2}x_1 \ltdyn \thunk \upcast{U\u F A_1}{U\u F A_2}(\lett y_1 = \force x_1; \ret y_1) \ltdyn \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1)}
+  
+  \inferrule
+  {\inferrule
+  {x_1 \ltdyn \force\upcast{U\u F A_1}{U\u FA_2}x_1 \ltdyn x_1\and
+    y_1 \ltdyn y_2 \vdash \upcast{A_1}{A_2}y_1 \ltdyn y_2
+  }
+  {\thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1) \ltdyn \thunk (\lett y_2 = \force\upcast{U\u F A_1}{U\u F A_2} x_1; \ret y_2)}}
+  {x_1 : U \u F A_1 \vdash \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1) \ltdyn \thunk (\lett y_2 = \force\upcast{U\u F A_1}{U\u F A_2} x_1; \ret y_2) \ltdyn \upcast{U\u F A_1}{U\u F A_2}x_1}
+  \caption{Exponential Interaction}
+
+  \inferrule
+  {\u B_1 \ltdyn \u B_2}
+  {\bullet:\u F U \u B_2 \vdash \dncast{\u FU\u B_1}{\u FU\u B_2}\bullet \equidyn \lett x = \bullet; \ret \thunk \force x : \u F U \u B_1}
+\end{figure}
+
+
+
 \section{Models}
 
 To determine what sorts of dynamic type we want for different
@@ -1035,9 +1122,123 @@ Today, many years later, with the benefit of much hindsight, we can
 see Levy's proof as an application of the method of \emph{focusing}.
 
 Here we adapt that proof to get an operational semantics for
-\emph{Gradual} CBPV.
+\emph{Gradual} CBPV that will .
+%
+If we focus even more intensely we can make all upcasts between
+positive connectives implicit, but allowing positive variables rules
+out that possibility.
+
+\begin{figure}[H]
+  \mbox{Values: $\Gamma \vdash V : A$}\\
+  \begin{mathpar}
+    \inferrule
+    {\Gamma \vdash \hat V : A_1 \and A_1 \ltdyn A_2}
+    {\Gamma \vdash \upcast {A_1}{A_2} \hat V : A_2}
+  \end{mathpar}
+  \mbox{Value Constructors: $\Gamma \vdash\hat V : A$}\\
+  \begin{mathpar}
+    \inferrule
+    {x : A \in \Gamma}
+    {\Gamma \vdash x : A}
 
-TODO
+    \inferrule
+    {\Gamma \vdash V : A \and\Gamma \vdash V' : A'}
+    {\Gamma \vdash ( V,  V') : A \times A'}
+
+    \inferrule
+    {\Gamma \vdash  V : A}
+    {\Gamma \vdash \sigma_{A,A'}  V : A + A'}
+
+    \inferrule
+    {\Gamma \vdash  V' : A'}
+    {\Gamma \vdash \sigma_{A,A'}'  V' : A + A'}
+
+    \inferrule
+    {}
+    {\Gamma \vdash () : 1}
+
+    \inferrule
+    {\Gamma \vdash M : \u B}
+    {\Gamma \vdash \thunk M : U \u B}
+  \end{mathpar}
+
+  \mbox{Terms: $\Gamma \vdash M : \u B$}
+  \begin{mathpar}
+    \inferrule
+    {}
+    {\Gamma \vdash \err_{\u B} : \u B}
+
+    \inferrule
+    {\Gamma \vdash V : A}
+    {\Gamma \vdash \ret V : \u F A}
+
+    \inferrule
+    {\Gamma \vdash V : U \u B\and
+      \Gamma \pipe [ \u B ] \vdash S : \u C
+    }
+    {\Gamma \vdash \force V; S : \u B}
+
+    \inferrule
+    {\Gamma, x : A \vdash M : \u B}
+    {\Gamma \vdash \lambda x : A. M : A \to \u B}
+
+    \inferrule
+    {}
+    {\Gamma \vdash [] : \top}
+
+    \inferrule
+    {\Gamma \vdash M : \u B\and
+      \Gamma \vdash M' : \u B'}
+    {\Gamma \vdash [\pi \mapsto M \pipe \pi' \mapsto M'] : \u B \wedge \u B'}
+
+    \inferrule
+    {\Gamma \vdash  V : A \times A'\and
+      \Gamma, x : A, x': A' \vdash M : \u B}
+    {\Gamma \vdash \lett (x,x') =  V; M : \u B}
+
+    \inferrule
+    {\Gamma \vdash  V : A + A'\and
+      \Gamma , x:A \vdash M : \u B\and
+      \Gamma , x:A' \vdash M' : \u B}
+    {\Gamma \vdash \case  V \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} : \u B}
+
+    \inferrule
+    {\Gamma \vdash \hat M : \u B_2 \and \u B_1 \ltdyn \u B_2}
+    {\Gamma \vdash \dncast{\u B_1}{\u B_2} \hat M : \u B_1}
+  \end{mathpar}
+
+  \mbox{Spines $\Gamma \pipe [ \u B ] \vdash S : \u C$}
+  \begin{mathpar}
+    \inferrule
+    {\Gamma \pipe [ \u B_1] \vdash S : \u C \and \u B_1 \ltdyn \u B_2}
+    {\Gamma \pipe [\u B_2] \vdash \dncast{\u B_1}{\u B_2}; S : \u C}
+  \end{mathpar}
+
+  \mbox{Computation Destructors $\Gamma\pipe [ \u B ] \vdash \hat S : \u C$}
+  \begin{mathpar}
+    \inferrule
+    {}
+    {\Gamma \pipe [\u B ] \vdash \bullet : \u B}
+
+    \inferrule
+    {\Gamma\pipe [\u B] \vdash S : \u C \and
+      \Gamma \vdash V : A}
+    {\Gamma\pipe [ A \to \u B ] \vdash 'V; S : \u C}
+
+    \inferrule
+    {\Gamma \pipe [\u B]\vdash S : C}
+    {\Gamma \pipe [\u B \wedge \u B'] \vdash \pi; S : \u C}
+
+    \inferrule
+    {\Gamma \pipe [\u B']\vdash S : C}
+    {\Gamma \pipe [\u B \wedge \u B'] \vdash \pi'; S : \u C}
+
+    \inferrule
+    {\Gamma, x : A \vdash M : \u C}
+    {\Gamma \pipe [\u F A] \vdash \too x. M : \u C}
+  \end{mathpar}
+  \caption{Operational Gradual Call By Push Value (Sketchy)}
+\end{figure}
 
 \section{The Notes we Don't Play}