diff --git a/coq/typing_debruijn.v b/coq/typing_debruijn.v
index d1675a5..d7098d4 100644
--- a/coq/typing_debruijn.v
+++ b/coq/typing_debruijn.v
@@ -61,3 +61,72 @@ Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
     (Γ |- [{ x des τ' }] \is τ')
 
 where "Γ '|-' x '\is' τ" := (typing Γ x τ).
+
+
+
+Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f"  (at level 101).
+
+Inductive translate_typing : context -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+
+  | Expand_Var : forall Γ x τ,
+    (Γ |- [{ $x }] \is τ) ->
+    (Γ |- [[ [{ $x }] \is τ ]] = [{ $x }])
+
+  | Expand_Let : forall Γ x e e' t t' σ τ,
+    (Γ |- e \is σ) ->
+    ((x,σ)::Γ |- t \is τ) ->
+    (Γ |- [[ e \is σ ]] = e') ->
+    ((x,σ)::Γ |- [[ t \is τ ]] = t') ->
+    (Γ |- [[  [{ let e in t }] \is τ  ]] = [{ let e' in t' }])
+
+  | Expand_TypeAbs : forall Γ e e' τ,
+    (Γ |- e \is τ) ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ Λ e }] \is [< ∀ τ >] ]] = [{ Λ e' }])
+
+  | Expand_TypeApp : forall Γ e e' σ τ,
+    (Γ |- e \is [< ∀ τ >]) ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }])
+
+  | Expand_Abs : forall Γ x σ e e' τ,
+    ((x,σ)::Γ |- e \is τ) ->
+    (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
+    ((x,σ)::Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }])
+
+  | Expand_MorphAbs : forall Γ x σ e e' τ,
+    ((x,σ)::Γ |- e \is τ) ->
+    (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
+    ((x,σ)::Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }])
+
+  | Expand_App : forall Γ f f' a a' m σ τ σ',
+    (Γ |- f \is [< σ -> τ >]) ->
+    (Γ |- a \is σ') ->
+    (Γ |- σ' ~~> σ) ->
+    (Γ |- [[ f \is [< σ -> τ >] ]] = f') ->
+    (Γ |- [[ a \is σ' ]] = a') ->
+    (Γ |- [[ σ' ~~> σ ]] = m) ->
+    (Γ |- [[ [{ f a }] \is τ ]] = [{ f' (m a') }])
+
+  | Expand_MorphFun : forall Γ f f' σ τ,
+    (Γ |- f \is [< σ ->morph τ >]) ->
+    (Γ |- f \is [< σ -> τ >]) ->
+    (Γ |- [[ f \is [< σ ->morph τ >] ]] = f') ->
+    (Γ |- [[ f \is [< σ -> τ >] ]] = f')
+
+  | Expand_Ascend : forall Γ e e' τ τ',
+    (Γ |- e \is τ) ->
+    (Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ [{ e as τ' }] \is [< τ' ~ τ >] ]] = [{ e' as τ' }])
+
+  | Expand_Descend : forall Γ e e' τ τ',
+    (Γ |- e \is τ) ->
+    (τ :<= τ') ->
+    (Γ |- [{ e des τ' }] \is τ') ->
+    (Γ |- [[ e \is τ ]] = e') ->
+    (Γ |- [[ e \is τ' ]] = [{ e' des τ' }])
+
+where "Γ '|-' '[[' e '\is' τ ']]' '=' f" := (translate_typing Γ e τ f).