diff --git a/Capless/CaptureSet.lean b/Capless/CaptureSet.lean
index 327647f3..d674eeb9 100644
--- a/Capless/CaptureSet.lean
+++ b/Capless/CaptureSet.lean
@@ -28,6 +28,7 @@ notation:max "{c=" c "}" => CaptureSet.csingleton c
 instance : Union (CaptureSet n k) where
   union := CaptureSet.union
 
+@[aesop unsafe [50% constructors]]
 inductive CaptureSet.Subset : CaptureSet n k → CaptureSet n k → Prop where
 | empty : Subset {} C
 | rfl : Subset C C
diff --git a/Capless/Subcapturing/Basic.lean b/Capless/Subcapturing/Basic.lean
index 5d170ea5..54c06ba6 100644
--- a/Capless/Subcapturing/Basic.lean
+++ b/Capless/Subcapturing/Basic.lean
@@ -6,4 +6,28 @@ theorem Subcapt.refl :
   apply subset
   apply CaptureSet.subset_refl
 
+theorem Subcapt.union_l
+  (h : Subcapt Γ C C2) :
+  Subcapt Γ C (C1 ∪ C2) := by
+  apply Subcapt.trans
+  { exact h }
+  { apply Subcapt.subset
+    aesop }
+
+theorem Subcapt.union_r
+  (h : Subcapt Γ C C1) :
+  Subcapt Γ C (C1 ∪ C2) := by
+  apply Subcapt.trans
+  { exact h }
+  { apply Subcapt.subset
+    aesop }
+
+theorem Subcapt.join
+  (h1 : Subcapt Γ C1 D1)
+  (h2 : Subcapt Γ C2 D2) :
+  Subcapt Γ (C1 ∪ C2) (D1 ∪ D2) := by
+  apply Subcapt.union
+  { apply Subcapt.union_r; assumption }
+  { apply Subcapt.union_l; assumption }
+
 end Capless
diff --git a/Capless/Type/Core.lean b/Capless/Type/Core.lean
index 1e649fb7..f21d5d1c 100644
--- a/Capless/Type/Core.lean
+++ b/Capless/Type/Core.lean
@@ -30,4 +30,7 @@ notation:40 "∃c." T => EType.ex T
 instance : Coe (CType n m k) (EType n m k) where
   coe T := EType.type T
 
+instance : Coe (SType n m k) (CType n m k) where
+  coe T := CType.capt {} T
+
 end Capless
diff --git a/Capless/playground.lean b/Capless/playground.lean
deleted file mode 100644
index b366fe2b..00000000
--- a/Capless/playground.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-inductive MemKind: Type -- classifies names/members
-| field -- names of term members
-| type  -- names of type members
-
-inductive Ty: Nat -> Type -- for simplicity, just one case
-| bot: Ty n
-
-inductive ComponentSig: Nat -> MemKind -> Type -- classifies the dependent second component of a pair _type_
-| field : Ty n -> ComponentSig n field         -- field member of type T
-| type  : Ty n -> Ty n -> ComponentSig n type  -- type member with interval S .. T
-
-def ComponentSig.interval' (sig : ComponentSig n K) : Ty n × Ty n := by
-  cases sig
-  case field => sorry
-  case type => sorry
diff --git a/Cappy.lean b/Cappy.lean
new file mode 100644
index 00000000..cd8ce275
--- /dev/null
+++ b/Cappy.lean
@@ -0,0 +1,2 @@
+import Cappy.Syntax
+import Cappy.TypeSystem
diff --git a/Cappy/Renaming.lean b/Cappy/Renaming.lean
new file mode 100644
index 00000000..3be59edd
--- /dev/null
+++ b/Cappy/Renaming.lean
@@ -0,0 +1,42 @@
+import Capless.Tactics
+import Capless.Basic
+namespace Cappy
+
+structure RenameFun (n m n' m' : Nat) where
+  map : Capless.FinFun n n'
+  tmap : Capless.FinFun m m'
+
+def RenameFun.ext (f : RenameFun n m n' m') : RenameFun (n+1) m (n'+1) m' :=
+  { map := f.map.ext, tmap := f.tmap }
+
+def RenameFun.text (f : RenameFun n m n' m') : RenameFun n (m+1) n' (m'+1) :=
+  { map := f.map, tmap := f.tmap.ext }
+
+def RenameFun.weaken : RenameFun n m (n+1) m :=
+  { map := Capless.FinFun.weaken, tmap := Capless.FinFun.id }
+
+def RenameFun.tweaken : RenameFun n m n (m+1) :=
+  { map := Capless.FinFun.id, tmap := Capless.FinFun.weaken }
+
+def RenameFun.id : RenameFun n m n m :=
+  { map := Capless.FinFun.id, tmap := Capless.FinFun.id }
+
+def RenameFun.comp (g : RenameFun n' m' n'' m'') (f : RenameFun n m n' m') : RenameFun n m n'' m'' :=
+  { map := g.map ∘ f.map, tmap := g.tmap ∘ f.tmap }
+
+theorem RenameFun.comp_ext {g : RenameFun n' m' n'' m''} {f : RenameFun n m n' m'} :
+  (g.comp f).ext = g.ext.comp f.ext := by
+  simp [RenameFun.comp, RenameFun.ext]
+  simp [Capless.FinFun.ext_comp_ext]
+
+theorem RenameFun.comp_text {g : RenameFun n' m' n'' m''} {f : RenameFun n m n' m'} :
+  (g.comp f).text = g.text.comp f.text := by
+  simp [RenameFun.comp, RenameFun.text]
+  simp [Capless.FinFun.ext_comp_ext]
+
+theorem RenameFun.weaken_tweaken :
+  tweaken.comp (weaken : RenameFun n m (n+1) m) = weaken.comp tweaken := by
+  simp [tweaken, weaken, comp]
+  aesop
+
+end Cappy
diff --git a/Cappy/Syntax.lean b/Cappy/Syntax.lean
new file mode 100644
index 00000000..39e28f7c
--- /dev/null
+++ b/Cappy/Syntax.lean
@@ -0,0 +1,4 @@
+import Cappy.Syntax.CaptureSet
+import Cappy.Syntax.Type
+import Cappy.Syntax.Term
+import Cappy.Syntax.Context
diff --git a/Cappy/Syntax/CaptureSet.lean b/Cappy/Syntax/CaptureSet.lean
new file mode 100644
index 00000000..4d6b3a16
--- /dev/null
+++ b/Cappy/Syntax/CaptureSet.lean
@@ -0,0 +1,87 @@
+import Capless.Tactics
+import Capless.Basic
+import Mathlib.Data.Fin.Basic
+namespace Cappy
+
+inductive CaptureSet : Nat -> Type where
+| empty : CaptureSet n
+| union : CaptureSet n -> CaptureSet n -> CaptureSet n
+| singleton : Fin n -> CaptureSet n
+| reach : Fin n -> CaptureSet n
+| universal : CaptureSet n
+
+@[simp]
+instance : EmptyCollection (CaptureSet n) where
+  emptyCollection := CaptureSet.empty
+
+notation:max "{x=" x "}" => CaptureSet.singleton x
+notation:max "{x*=" c "}" => CaptureSet.reach c
+notation:max "{cap}" => CaptureSet.universal
+
+@[simp]
+instance : Union (CaptureSet n) where
+  union := CaptureSet.union
+
+@[aesop unsafe [50% constructors]]
+inductive CaptureSet.Subset : CaptureSet n -> CaptureSet n -> Prop where
+| empty : Subset {} C
+| rfl : Subset C C
+| union_l :
+  Subset C1 C ->
+  Subset C2 C ->
+  Subset (C1 ∪ C2) C
+| union_rl :
+  Subset C C1 ->
+  Subset C (C1 ∪ C2)
+| union_rr :
+  Subset C C2 ->
+  Subset C (C1 ∪ C2)
+
+@[simp]
+instance : HasSubset (CaptureSet n) where
+  Subset := CaptureSet.Subset
+
+def CaptureSet.rename (C : CaptureSet n) (f : Capless.FinFun n n') : CaptureSet n' :=
+  match C with
+  | empty => {}
+  | union C1 C2 => (C1.rename f) ∪ (C2.rename f)
+  | singleton x => {x=(f x)}
+  | reach x => {x*=(f x)}
+  | universal => {cap}
+
+def CaptureSet.weaken (C : CaptureSet n) : CaptureSet (n+1) :=
+  C.rename Capless.FinFun.weaken
+
+structure CapSubst (n n' : Nat) where
+  map : Fin n -> CaptureSet n'
+  rmap : Fin n -> CaptureSet n'
+  capmap : CaptureSet n'
+
+def CaptureSet.subst : CaptureSet n -> CapSubst n n' -> CaptureSet n'
+| empty, _ => {}
+| union C1 C2, σ => (C1.subst σ) ∪ (C2.subst σ)
+| singleton x, σ => (σ.map x)
+| reach x, σ => (σ.rmap x)
+| universal, σ => σ.capmap
+
+def CapSubst.open_cap (D : CaptureSet n) : CapSubst n n :=
+  { map := λ x => {x=x}, rmap := λ x => {x*=x}, capmap := D }
+
+def CaptureSet.open_cap (C : CaptureSet n) (D : CaptureSet n) : CaptureSet n :=
+  C.subst (CapSubst.open_cap D)
+
+theorem CaptureSet.rename_comp {C : CaptureSet n} :
+  (C.rename f).rename g = C.rename (g.comp f) := by
+  induction C generalizing f g <;> try (solve | simp [rename])
+  case union ih1 ih2 =>
+    simp [rename]
+    aesop
+
+theorem CaptureSet.rename_id {C : CaptureSet n} :
+  C.rename Capless.FinFun.id = C := by
+  induction C <;> try (solve | simp [rename, Capless.FinFun.id])
+  case union ih1 ih2 =>
+    simp [rename]
+    aesop
+
+end Cappy
diff --git a/Cappy/Syntax/Context.lean b/Cappy/Syntax/Context.lean
new file mode 100644
index 00000000..ec3052da
--- /dev/null
+++ b/Cappy/Syntax/Context.lean
@@ -0,0 +1,2 @@
+import Cappy.Syntax.Context.Core
+import Cappy.Syntax.Context.Properties
diff --git a/Cappy/Syntax/Context/Core.lean b/Cappy/Syntax/Context/Core.lean
new file mode 100644
index 00000000..8258b9ae
--- /dev/null
+++ b/Cappy/Syntax/Context/Core.lean
@@ -0,0 +1,29 @@
+import Cappy.Syntax.Type
+namespace Cappy
+
+inductive Context : Nat -> Nat -> Type where
+| empty : Context 0 0
+| var : Context n m -> CType n m -> Context (n+1) m
+| tvar : Context n m -> SType n m -> Context n (m+1)
+
+inductive Context.Bound : Context n m -> Fin n -> CType n m -> Prop where
+| here :
+  Context.Bound (Context.var Γ T) 0 T.weaken
+| there_var :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.var Γ T') x.succ T.weaken
+| there_tvar :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.tvar Γ S) x T.tweaken
+
+inductive Context.TBound : Context n m -> Fin m -> SType n m -> Prop where
+| here :
+  Context.TBound (Context.tvar Γ S) 0 S.tweaken
+| there_var :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.var Γ T) x S.weaken
+| there_tvar :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.tvar Γ S') x.succ S.tweaken
+
+end Cappy
diff --git a/Cappy/Syntax/Context/Properties.lean b/Cappy/Syntax/Context/Properties.lean
new file mode 100644
index 00000000..760198bf
--- /dev/null
+++ b/Cappy/Syntax/Context/Properties.lean
@@ -0,0 +1,65 @@
+import Cappy.Syntax.Context.Core
+import Cappy.Syntax.Type.Properties
+namespace Cappy
+
+theorem Context.var_bound_succ'
+  (he1 : Γ0 = Γ.var P) (he2 : x0 = x.succ)
+  (hb : Context.Bound Γ0 x0 T) :
+  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken := by
+  cases hb <;> try (solve | cases he1 | cases he2)
+  cases he1
+  rw [Fin.succ_inj] at he2
+  aesop
+
+theorem Context.var_bound_succ
+  (hb : Context.Bound (Context.var Γ P) x.succ T) :
+  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken :=
+  Context.var_bound_succ' rfl rfl hb
+
+theorem Context.bound_inj
+  (hb1 : Context.Bound Γ x T1)
+  (hb2 : Context.Bound Γ x T2) :
+  T1 = T2 := by
+  induction hb1
+  case here => cases hb2; rfl
+  case there_var ih =>
+    have ⟨T0, hb2, heq⟩ := Context.var_bound_succ hb2
+    have ih := ih hb2
+    aesop
+  case there_tvar ih =>
+    cases hb2; rename_i hb2
+    have ih := ih hb2
+    aesop
+
+theorem Context.bound_exists {x : Fin n} {Γ : Context n m} :
+  ∃ T, Context.Bound Γ x T := by
+  induction Γ
+  case empty => apply Fin.elim0 x
+  case var ih =>
+    cases x using Fin.cases
+    case zero => constructor; constructor
+    case succ x0 =>
+      have ⟨T0, ih⟩ := ih (x := x0)
+      constructor; constructor
+      assumption
+  case tvar ih =>
+    have ⟨T0, ih⟩ := ih (x := x)
+    constructor; constructor
+    assumption
+
+inductive CType.Weakened : CType n m -> Prop where
+| mk :
+  CType.Weakened (CType.weaken T)
+
+theorem Context.bound_weaken
+  (hb : Context.Bound Γ x T) :
+  T.Weakened := by
+  induction hb
+  case here => constructor
+  case there_var => constructor
+  case there_tvar ih =>
+    cases ih
+    simp [CType.tweaken_weaken]
+    constructor
+
+end Cappy
diff --git a/Cappy/Syntax/Term.lean b/Cappy/Syntax/Term.lean
new file mode 100644
index 00000000..3f44be93
--- /dev/null
+++ b/Cappy/Syntax/Term.lean
@@ -0,0 +1,14 @@
+import Cappy.Syntax.Type
+namespace Cappy
+
+inductive Term : Nat -> Nat -> Type where
+| var : Fin n -> Term n m
+| abs : Annot -> CType n m -> Term (n+1) m -> Term n m
+| app : Fin n -> Fin n -> Term n m
+| tabs : SType n m -> Term n (m+1) -> Term n m
+| tapp : Fin m -> SType n m -> Term n m
+| box : Fin n -> Term n m
+| unbox : CaptureSet n -> Fin n -> Term n m
+| letin : Term n m -> Term (n+1) m -> Term n m
+
+end Cappy
diff --git a/Cappy/Syntax/Type.lean b/Cappy/Syntax/Type.lean
new file mode 100644
index 00000000..fb18a5d7
--- /dev/null
+++ b/Cappy/Syntax/Type.lean
@@ -0,0 +1,2 @@
+import Cappy.Syntax.Type.Core
+import Cappy.Syntax.Type.Properties
diff --git a/Cappy/Syntax/Type/Core.lean b/Cappy/Syntax/Type/Core.lean
new file mode 100644
index 00000000..711d0698
--- /dev/null
+++ b/Cappy/Syntax/Type/Core.lean
@@ -0,0 +1,55 @@
+import Cappy.Syntax.CaptureSet
+import Cappy.Renaming
+
+namespace Cappy
+
+inductive Annot : Type where
+| eps : Annot
+| use : Annot
+
+mutual
+
+inductive CType : Nat -> Nat -> Type where
+| capt : CaptureSet n -> SType n m -> CType n m
+
+inductive SType : Nat -> Nat -> Type where
+| top : SType n m
+| tvar : Fin m -> SType n m
+| arrow : Annot -> CType n m -> CType (n+1) m -> SType n m
+| tarrow : SType n m -> CType n (m+1) -> SType n m
+| boxed : CType n m -> SType n m
+
+end
+
+notation:max S "^" C => CType.capt C S
+notation:50 "∀(x:" T ")" U => SType.arrow Annot.eps T U
+notation:50 "∀(use x:" T ")" U => SType.arrow Annot.use T U
+notation:50 "∀[X<:" S "]" T => SType.tarrow S T
+
+mutual
+
+def CType.rename : CType n m -> RenameFun n m n' m' -> CType n' m'
+| CType.capt C S, f => (S.rename f)^(C.rename f.map)
+
+def SType.rename : SType n m -> RenameFun n m n' m' -> SType n' m'
+| SType.top, _ => SType.top
+| SType.tvar x, f => SType.tvar (f.tmap x)
+| SType.arrow a T U, f => SType.arrow a (T.rename f) (U.rename f.ext)
+| SType.tarrow S T, f => SType.tarrow (S.rename f) (T.rename f.text)
+| SType.boxed C, f => SType.boxed (C.rename f)
+
+end
+
+def CType.weaken (T : CType n m) : CType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def SType.weaken (T : SType n m) : SType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def CType.tweaken (T : CType n m) : CType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+def SType.tweaken (T : SType n m) : SType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+end Cappy
diff --git a/Cappy/Syntax/Type/Properties.lean b/Cappy/Syntax/Type/Properties.lean
new file mode 100644
index 00000000..f3e13988
--- /dev/null
+++ b/Cappy/Syntax/Type/Properties.lean
@@ -0,0 +1,44 @@
+import Cappy.Syntax.Type.Core
+namespace Cappy
+
+mutual
+
+theorem CType.rename_comp {T : CType n m} :
+  (T.rename f).rename g = T.rename (g.comp f) :=
+  match T with
+  | CType.capt C S => by
+    simp [CType.rename]
+    apply And.intro
+    { apply CaptureSet.rename_comp }
+    { apply SType.rename_comp }
+
+theorem SType.rename_comp {S : SType n m} :
+  (S.rename f).rename g = S.rename (g.comp f) :=
+  match S with
+  | SType.top => by simp [SType.rename]
+  | SType.tvar X => by simp [SType.rename, RenameFun.comp]
+  | SType.arrow a T U => by
+    simp [SType.rename]
+    apply And.intro
+    { apply CType.rename_comp }
+    { simp [RenameFun.comp_ext]
+      apply CType.rename_comp }
+  | SType.tarrow S T => by
+    simp [SType.rename]
+    apply And.intro
+    { apply SType.rename_comp }
+    { simp [RenameFun.comp_text]
+      apply CType.rename_comp }
+  | SType.boxed T => by
+    simp [SType.rename]
+    apply CType.rename_comp
+
+end
+
+theorem CType.tweaken_weaken {T : CType n m} :
+  T.weaken.tweaken = T.tweaken.weaken := by
+  simp [CType.weaken, CType.tweaken]
+  simp [CType.rename_comp]
+  simp [RenameFun.weaken_tweaken]
+
+end Cappy
diff --git a/Cappy/Translation/Encoding/CaptureSet.lean b/Cappy/Translation/Encoding/CaptureSet.lean
new file mode 100644
index 00000000..e1a4825f
--- /dev/null
+++ b/Cappy/Translation/Encoding/CaptureSet.lean
@@ -0,0 +1,2 @@
+import Cappy.Translation.Encoding.CaptureSet.Core
+import Cappy.Translation.Encoding.CaptureSet.Properties
diff --git a/Cappy/Translation/Encoding/CaptureSet/Core.lean b/Cappy/Translation/Encoding/CaptureSet/Core.lean
new file mode 100644
index 00000000..7106dd3b
--- /dev/null
+++ b/Cappy/Translation/Encoding/CaptureSet/Core.lean
@@ -0,0 +1,35 @@
+import Cappy.Syntax
+import Capless.CaptureSet
+import Cappy.Translation.TContext
+namespace Cappy
+
+/-!
+# Encoding of Capture Sets
+
+The `CaptureSet.Interp` derivation defines the encoding of capture sets from Cappy to Capless. It is a 5-place judgement:
+1. The mapping from reach capabilities to capture variables
+2. The type context in Cappy
+3. The input capture set
+4. The interpretation
+5. The output capture set
+!-/
+
+inductive CaptureSet.Interp : TMap n m k -> Context n m -> CaptureSet n -> Capless.CaptureSet n k -> Capless.CaptureSet n k -> Prop where
+| i_empty :
+  CaptureSet.Interp ρ Γ {} D {}
+| i_union :
+  CaptureSet.Interp ρ Γ C1 D D1 ->
+  CaptureSet.Interp ρ Γ C2 D D2 ->
+  CaptureSet.Interp ρ Γ (C1 ∪ C2) D (D1 ∪ D2)
+| i_singleton :
+  Context.Bound Γ x (S^C) ->
+  CaptureSet.Interp ρ Γ C {c=ρ.reach x} C' ->
+  CaptureSet.Interp ρ Γ {x=x} D C'
+| i_reach :
+  CaptureSet.Interp ρ Γ {x*=x} D {c=ρ.reach x}
+| i_cap :
+  CaptureSet.Interp ρ Γ {cap} D D
+
+notation:20 "⟦" C1 "⟧^" D " ↝c[" ρ " | " Γ "] " C2 => CaptureSet.Interp ρ Γ C1 D C2
+
+end Cappy
diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
new file mode 100644
index 00000000..04263d5a
--- /dev/null
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -0,0 +1,218 @@
+import Cappy.Translation.Encoding.CaptureSet.Core
+namespace Cappy
+
+theorem CaptureSet.interp_inj
+  (hi1 : CaptureSet.Interp ρ Γ C D I1)
+  (hi2 : CaptureSet.Interp ρ Γ C D I2) :
+  I1 = I2 := by
+  induction hi1 generalizing I2 <;> try (solve | cases hi2; trivial)
+  case i_union ih1 ih2 =>
+    cases hi2
+    aesop
+  case i_singleton hb1 _ ih =>
+    cases hi2; rename_i hb2 _
+    have h := Context.bound_inj hb1 hb2
+    aesop
+
+theorem CaptureSet.weaken_union {C1 C2 : CaptureSet n} :
+  (C1 ∪ C2).weaken = C1.weaken ∪ C2.weaken := by
+  simp [CaptureSet.weaken, CaptureSet.rename]
+
+theorem CType.weaken_capt :
+  (S^C : CType n m).weaken = S.weaken^C.weaken := by
+  simp [CType.weaken, CType.rename, CaptureSet.weaken, SType.weaken, RenameFun.weaken]
+
+theorem CType.tweaken_capt :
+  (S^C : CType n m).tweaken = S.tweaken^C := by
+  simp [CType.tweaken, CType.rename, SType.tweaken, RenameFun.tweaken]
+  simp [CaptureSet.rename_id]
+
+theorem Capless.CaptureSet.weaken_union {C1 C2 : Capless.CaptureSet n k} :
+  (C1 ∪ C2).weaken = C1.weaken ∪ C2.weaken := by
+  simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
+
+theorem Capless.CaptureSet.cweaken_union {C1 C2 : Capless.CaptureSet n k} :
+  (C1 ∪ C2).cweaken = C1.cweaken ∪ C2.cweaken := by
+  simp [Capless.CaptureSet.cweaken, Capless.CaptureSet.crename]
+
+theorem Capless.CaptureSet.weaken_csingleton :
+  ({c=x} : Capless.CaptureSet n k).weaken = {c=x} := by
+  simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
+
+theorem TMap.ext_reach_succ {ρ : TMap n m k} :
+  ρ.ext.reach x.succ = (ρ.reach x).succ := by
+  simp [TMap.ext, Capless.FinFun.ext]
+
+inductive CaptureSet.Lift : CaptureSet n -> CaptureSet n' -> Prop where
+| refl : CaptureSet.Lift C C
+| step :
+  CaptureSet.Lift C C' ->
+  CaptureSet.Lift C C'.weaken
+
+theorem CaptureSet.lift_empty'
+  (he : C0 = {})
+  (hl : CaptureSet.Lift C0 C) : C = {} := by
+  induction hl
+  case refl => assumption
+  case step hl => aesop
+
+theorem CaptureSet.lift_empty
+  (hl : CaptureSet.Lift ({} : CaptureSet n) C) : C = {} :=
+  CaptureSet.lift_empty' rfl hl
+
+theorem CaptureSet.lift_union'
+  (he : C0 = C1 ∪ C2)
+  (hl : CaptureSet.Lift C0 D) :
+  ∃ D1 D2, CaptureSet.Lift C1 D1 ∧ CaptureSet.Lift C2 D2 ∧ D = D1 ∪ D2 := by
+  induction hl
+  case refl =>
+    constructor; constructor
+    constructor; constructor
+    constructor; constructor
+    assumption
+  case step hl ih =>
+    have ih := ih he
+    have ⟨D1, D2, ih1, ih2, he⟩ := ih
+    apply Exists.intro D1.weaken
+    apply Exists.intro D2.weaken
+    constructor
+    constructor; assumption
+    constructor
+    constructor; assumption
+    rw [he, CaptureSet.weaken_union]
+
+theorem CaptureSet.lift_union
+  (hl : CaptureSet.Lift (C1 ∪ C2) D) :
+  ∃ D1 D2, CaptureSet.Lift C1 D1 ∧ CaptureSet.Lift C2 D2 ∧ D = D1 ∪ D2 := by
+  apply CaptureSet.lift_union' rfl hl
+
+theorem CaptureSet.lift_cap'
+  (he : C0 = {cap})
+  (hl : CaptureSet.Lift C0 D) :
+  D = {cap} := by
+  induction hl
+  case refl => aesop
+  case step ih =>
+    have ih := ih he
+    rw [ih]
+    simp [CaptureSet.weaken, CaptureSet.rename]
+
+theorem CaptureSet.lift_cap
+  (hl : CaptureSet.Lift ({cap} : CaptureSet n) D) :
+  D = {cap} :=
+  CaptureSet.lift_cap' rfl hl
+
+theorem CaptureSet.lift_reach'
+  (he : C0 = {x*=x})
+  (hl : CaptureSet.Lift C0 D) :
+  ∃ y, D = {x*=y} := by
+  induction hl
+  case refl => aesop
+  case step ih =>
+    have ⟨y0, ih⟩ := ih he
+    rw [ih]
+    simp [CaptureSet.weaken, CaptureSet.rename]
+
+theorem CaptureSet.lift_reach
+  (hl : CaptureSet.Lift {x*=xC0} D) :
+  ∃ y, D = {x*=y} :=
+  CaptureSet.lift_reach' rfl hl
+
+def CaptureSet.InterpComplete (Γ : Context n m) :=
+  ∀ {k} (ρ : TMap n m k) C D, ∃ I, CaptureSet.Interp ρ Γ C D I
+
+theorem CaptureSet.interp_weaken
+  (hi : CaptureSet.Interp ρ Γ C D I) :
+  ∃ I', CaptureSet.Interp ρ' (Γ.var P) C.weaken D' I' := by
+  induction hi generalizing ρ' D'
+  case i_empty =>
+    simp [weaken, rename]
+    constructor; constructor
+  case i_union ih1 ih2 =>
+    have ⟨I1, ih1⟩ := ih1 (ρ' := ρ') (D' := D')
+    have ⟨I2, ih2⟩ := ih2 (ρ' := ρ') (D' := D')
+    rw [CaptureSet.weaken_union]
+    constructor; constructor <;> assumption
+  case i_singleton x0 _ _ _ _ _ hb _ ih =>
+    have hb1 := Context.Bound.there_var (T' := P) hb
+    simp [CType.weaken_capt] at hb1
+    simp [weaken, rename, Capless.FinFun.weaken]
+    have ⟨I, ih⟩ := ih (ρ' := ρ') (D' := {c=ρ'.reach x0.succ})
+    constructor; constructor
+    { exact hb1 }
+    { exact ih }
+  case i_reach =>
+    simp [weaken, rename, Capless.FinFun.weaken]
+    constructor; constructor
+  case i_cap =>
+    simp [weaken, rename]
+    constructor; constructor
+
+theorem CaptureSet.interp_tweaken
+  (hi : CaptureSet.Interp ρ Γ C D I) :
+  ∃ I', CaptureSet.Interp ρ' (Γ.tvar S) C D' I' := by
+  induction hi generalizing ρ' D'
+  case i_empty => constructor; constructor
+  case i_union ih1 ih2 =>
+    have ⟨I1, ih1⟩ := ih1 (ρ' := ρ') (D' := D')
+    have ⟨I2, ih2⟩ := ih2 (ρ' := ρ') (D' := D')
+    constructor; constructor <;> assumption
+  case i_singleton x0 _ _ _ _ _ hb0 _ ih =>
+    have ⟨I0, hi0⟩ := ih (ρ' := ρ') (D' := {c=ρ'.reach x0})
+    have hb := Context.Bound.there_tvar (S := S) hb0
+    simp [CType.tweaken_capt] at hb
+    constructor; constructor
+    { exact hb }
+    { exact hi0 }
+  case i_reach => constructor; constructor
+  case i_cap => constructor; constructor
+
+theorem CaptureSet.interp_complete' :
+  InterpComplete Γ := by
+  induction Γ <;> (unfold InterpComplete; intro k ρ C D)
+  case empty =>
+    induction C
+    case empty => constructor; constructor
+    case union ih1 ih2 =>
+      have ⟨I1, ih1⟩ := ih1
+      have ⟨I2, ih2⟩ := ih2
+      constructor; constructor <;> assumption
+    case singleton x0 => apply Fin.elim0 x0
+    case reach x0 => apply Fin.elim0 x0
+    case universal => constructor; constructor
+  case var Γ0 P0 ih =>
+    induction C
+    case empty => constructor; constructor
+    case union ih1 ih2 =>
+      have ⟨I1, ih1⟩ := ih1
+      have ⟨I2, ih2⟩ := ih2
+      constructor; constructor <;> assumption
+    case singleton x0 =>
+      cases P0; rename_i C0 S0
+      have ⟨T0, hb0⟩ := Context.bound_exists (Γ:=Γ0.var (S0^C0)) (x:=x0)
+      cases hb0
+      case here =>
+        have hb0 := Context.Bound.here (Γ := Γ0) (T := (S0^C0))
+        simp [CType.weaken_capt] at hb0
+        have ⟨I0, ih0⟩ := ih (ρ := ρ.strip) (C := C0) (D := {})
+        have ⟨I1, ih1⟩ := CaptureSet.interp_weaken (ρ':=ρ) (D':={c=ρ.reach 0}) (P:=(S0^C0)) ih0
+        constructor
+        constructor
+        { exact hb0 }
+        { exact ih1 }
+      case there_var x0 T0 hb0 =>
+        have ⟨I0, ih0⟩ := ih (ρ := ρ.strip) (C:={x=x0}) (D:={})
+        have ih1 := CaptureSet.interp_weaken (ρ':=ρ) (D':=D) (P:=(S0^C0)) ih0
+        exact ih1
+    case reach => constructor; constructor
+    case universal => constructor; constructor
+  case tvar Γ0 S0 ih =>
+    have ⟨I0, h0⟩ := ih (ρ:=ρ.tstrip) (C:=C) (D:=D)
+    have h1 := CaptureSet.interp_tweaken (ρ':=ρ) (D':=D) (S:=S0) h0
+    exact h1
+
+theorem CaptureSet.interp_complete :
+  ∃ I, CaptureSet.Interp ρ Γ C D I :=
+  CaptureSet.interp_complete' ρ C D
+
+end Cappy
diff --git a/Cappy/Translation/Encoding/Context.lean b/Cappy/Translation/Encoding/Context.lean
new file mode 100644
index 00000000..1b974909
--- /dev/null
+++ b/Cappy/Translation/Encoding/Context.lean
@@ -0,0 +1,17 @@
+import Cappy.Translation.Encoding.Type
+import Cappy.Translation.TContext
+namespace Cappy
+
+inductive Context.Interp : Context n m -> TContext n m k -> Prop where
+| empty :
+  Context.Interp empty TContext.empty
+| var {Γ : Context n m} {Δ : TContext n m k} :
+  Context.Interp Γ Δ ->
+  CType.Interp (Δ.map.cweaken) Γ T {c=0} T' ->
+  Context.Interp (Γ.var T) (Δ.var T')
+| tvar {Γ : Context n m} {Δ : TContext n m k} :
+  Context.Interp Γ Δ ->
+  CType.Interp (Δ.map.cweaken) Γ (S^{}) {c=0} (S'^{}) ->
+  Context.Interp (Γ.tvar S) (Δ.tvar S')
+
+end Cappy
diff --git a/Cappy/Translation/Encoding/Type.lean b/Cappy/Translation/Encoding/Type.lean
new file mode 100644
index 00000000..7e2a8a90
--- /dev/null
+++ b/Cappy/Translation/Encoding/Type.lean
@@ -0,0 +1,49 @@
+import Cappy.Translation.Encoding.CaptureSet
+import Capless.Type
+namespace Cappy
+
+/-!
+# Encoding of Types
+!-/
+
+inductive CType.Interp : TMap n m k -> Context n m -> CType n m -> Capless.CaptureSet n k -> Capless.CType n m k -> Prop where
+| i_top :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ Γ (SType.top^C) D (⊤^C')
+| i_tvar :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ Γ ((SType.tvar X)^C) D ((Capless.SType.tvar X)^C')
+| i_boxed :
+  CType.Interp ρ Γ T D T' ->
+  CType.Interp ρ Γ
+     ((SType.boxed T)^{})
+     D
+     ((∀(x:⊤^{})((∀(x:⊤^{})(Capless.EType.type T'.weaken.weaken))^Capless.CaptureSet.empty))^Capless.CaptureSet.empty)
+| i_arrow :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ.cweaken Γ T ({c=0}) T' ->
+  CaptureSet.Interp ρ.ext (Γ.var T) ({x*=0}∪{x=0}) {} D1 ->
+  CType.Interp ρ.ext (Γ.var T) U (D.weaken.cweaken ∪ D1) U' ->
+  CType.Interp ρ Γ
+    ((∀(x:T)U)^C)
+    D
+    ((∀[c](Capless.EType.type (∀(x:T')U')^(C'.cweaken)))^({}))
+| i_uarrow :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ.cweaken Γ T ({c=0}) T' ->
+  CaptureSet.Interp ρ.ext (Γ.var T) ({x*=0}∪{x=0}) {} D1 ->
+  CType.Interp ρ.ext (Γ.var T) U (D.weaken.cweaken ∪ D1) U' ->
+  CType.Interp ρ Γ
+    ((∀(use x:T)U)^C)
+    D
+    ((∀[c](Capless.EType.type (∀(x:T')U')^(C'.cweaken ∪ {c=0})))^({}))
+| i_tarrow :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ.cweaken Γ (S^{}) ({c=0}) (S'^{}) ->
+  CType.Interp ρ.text (Γ.tvar S) T (D.cweaken ∪ {c=0}) T' ->
+  CType.Interp ρ Γ
+    ((∀[X<:S]T)^C)
+    D
+    ((∀[c](Capless.EType.type (∀[X<:S']T')^(C'.cweaken)))^({}))
+
+end Cappy
diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
new file mode 100644
index 00000000..dd162917
--- /dev/null
+++ b/Cappy/Translation/Subcapturing.lean
@@ -0,0 +1,98 @@
+import Cappy.Translation.Encoding.Context
+import Cappy.TypeSystem.Subcapturing
+import Capless.Subcapturing
+import Capless.Subcapturing.Basic
+namespace Cappy
+
+theorem CaptureSet.interp_monotonic_subcapt
+  (h : Δ ⊢ D1 <:c D2)
+  (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
+  (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
+  (Δ ⊢ I1 <:c I2) := by
+  induction C generalizing I1 I2
+  case empty =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case union C1 C2 ih1 ih2 =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.join
+    { aesop }
+    { aesop }
+  case singleton =>
+    cases hi1; cases hi2
+    rename_i hb1 hi1 _ _ hb2 hi2
+    have h := Context.bound_inj hb1 hb2
+    cases h
+    have h := CaptureSet.interp_inj hi1 hi2
+    cases h
+    apply Capless.Subcapt.refl
+  case reach =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case universal =>
+    cases hi1; cases hi2
+    assumption
+
+theorem CaptureSet.interp_monotonic_subset
+  (hi1 : CaptureSet.Interp ρ Γ C1 D I1)
+  (hi2 : CaptureSet.Interp ρ Γ C2 D I2)
+  (hsub : C1 ⊆ C2) :
+  I1 ⊆ I2 := by
+  induction hsub generalizing I1 I2
+  case empty => cases hi1; aesop
+  case rfl =>
+    have h := CaptureSet.interp_inj hi1 hi2
+    aesop
+  case union_l =>
+    cases hi1
+    aesop
+  case union_rl => cases hi2; aesop
+  case union_rr => cases hi2; aesop
+
+theorem CaptureSet.interp_meet
+  (h1 : CaptureSet.Interp ρ Γ C D1 I1)
+  (h2 : CaptureSet.Interp ρ Γ C D2 I2) :
+  ∃ D3 I3,
+    CaptureSet.Interp ρ Γ C D3 I3 ∧
+    (Δ ⊢ I1 <:c I3) ∧ (Δ ⊢ I2 <:c I3) := by
+  have ⟨I3, h3⟩ := CaptureSet.interp_complete (ρ := ρ) (Γ := Γ) (C := C) (D := D1 ∪ D2)
+  apply Exists.intro (D1 ∪ D2)
+  apply Exists.intro I3
+  constructor; assumption
+  constructor
+  { apply CaptureSet.interp_monotonic_subcapt (hi1 := h1) (hi2 := h3)
+    apply Capless.Subcapt.subset; aesop }
+  { apply CaptureSet.interp_monotonic_subcapt (hi1 := h2) (hi2 := h3)
+    apply Capless.Subcapt.subset; aesop }
+
+theorem CaptureSet.interp_monotonic_alt
+  (hsc : Subcapt Γ C1 C2)
+  (hi1 : CaptureSet.Interp ρ Γ C1 D1 I1) :
+  ∃ D2 I2, CaptureSet.Interp ρ Γ C2 D2 I2 ∧ Δ ⊢ I1 <:c I2 := by
+  induction hsc generalizing D1 I1
+  case sc_trans ih1 ih2 =>
+    have ⟨D2, I2, hi2, hsc2⟩ := ih1 hi1
+    have ⟨D3, I3, hi3, hsc3⟩ := ih2 hi2
+    have hsc0 := Capless.Subcapt.trans hsc2 hsc3
+    aesop
+  case sc_var hb1 =>
+    cases hi1; rename_i hb2 hi1
+    have h := Context.bound_inj hb1 hb2
+    cases h
+    have hsc0 := Capless.Subcapt.refl (Γ := Δ) (C := I1)
+    aesop
+  case sc_elem C1 C2 hs =>
+    have ⟨I2, hi2⟩ := CaptureSet.interp_complete (ρ:=ρ) (Γ:=Γ) (C:=C2) (D:=D1)
+    have h := CaptureSet.interp_monotonic_subset hi1 hi2 hs
+    have h := Capless.Subcapt.subset (Γ:=Δ) h
+    aesop
+  case sc_set C1 C2 C _ _ ih1 ih2 =>
+    cases hi1; rename_i I11 I12 hi11 hi12
+    have ⟨D21, I21, h21, hs21⟩ := ih1 hi11
+    have ⟨D22, I22, h22, hs22⟩ := ih2 hi12
+    have ⟨D3, I3, hi3, hs1, hs2⟩ := CaptureSet.interp_meet (Δ:=Δ) h21 h22
+    apply Exists.intro D3; apply Exists.intro I3
+    constructor; assumption
+    apply Capless.Subcapt.union <;> (apply Capless.Subcapt.trans <;> assumption)
+
+end Cappy
diff --git a/Cappy/Translation/Subtyping.lean b/Cappy/Translation/Subtyping.lean
new file mode 100644
index 00000000..641d1db6
--- /dev/null
+++ b/Cappy/Translation/Subtyping.lean
@@ -0,0 +1,59 @@
+import Cappy.Translation.Subcapturing
+import Cappy.TypeSystem
+import Capless.Subtyping
+namespace Cappy
+
+theorem CType.interp_monotonic_cs
+  (hi : CType.Interp ρ Γ (S^C1) D1 Q1)
+  (hs : Subcapt Γ C1 C2) :
+  ∃ D2 Q2,
+    CType.Interp ρ Γ (S^C2) D2 Q2 ∧
+    Capless.CSubtyp Δ Q1 Q2 := sorry
+
+def CType.interp_monotonic.motive_1
+  (Γ : Context n m)
+  (T1 T2 : CType n m)
+  (_ : CSubtyp Γ T1 T2) : Prop :=
+  ∀ {k} {Δ : Capless.Context n m k} {ρ} (_ : Context.Interp Γ ⟨Δ, ρ⟩)
+    {D1 Q1} (_ : CType.Interp ρ Γ T1 D1 Q1),
+  ∃ D2 Q2,
+    CType.Interp ρ Γ T2 D2 Q2 ∧
+    (Δ ⊢ Q1 <: Q2)
+
+def CType.interp_monotonic.motive_2
+  (Γ : Context n m)
+  (S1 S2 : SType n m)
+  (_ : SSubtyp Γ S1 S2) : Prop :=
+  ∀ {k} {Δ : Capless.Context n m k} {ρ} (_ : Context.Interp Γ ⟨Δ, ρ⟩)
+    {C D1 Q1} (_ : CType.Interp ρ Γ (S1^C) D1 Q1),
+  ∃ D2 Q2,
+    CType.Interp ρ Γ (S2^C) D2 Q2 ∧
+    (Δ ⊢ Q1 <: Q2)
+
+theorem CType.interp_monotonic
+  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+  (hsub : CSubtyp Γ T1 T2)
+  (hi : CType.Interp ρ Γ T1 D1 Q1) :
+  ∃ D2 Q2,
+    CType.Interp ρ Γ T2 D2 Q2 ∧
+    (Δ ⊢ Q1 <: Q2) := by
+  apply CSubtyp.rec
+    (motive_1 := CType.interp_monotonic.motive_1)
+    (motive_2 := CType.interp_monotonic.motive_2)
+    (t := hsub)
+    (D1 := D1)
+  all_goals try assumption
+  case capt =>
+    repeat intro
+    rename_i hsc hs ih _ Δ ρ hg D1 Q1 hi1
+    unfold interp_monotonic.motive_2 at ih
+    sorry
+  case top => sorry
+  case refl => sorry
+  case trans => sorry
+  case tvar => sorry
+  case boxed => sorry
+  case arrow => sorry
+  case tarrow => sorry
+
+end Cappy
diff --git a/Cappy/Translation/TContext.lean b/Cappy/Translation/TContext.lean
new file mode 100644
index 00000000..280e9ae2
--- /dev/null
+++ b/Cappy/Translation/TContext.lean
@@ -0,0 +1,25 @@
+import Capless.Context
+import Capless.Basic
+import Cappy.Translation.TMap
+namespace Cappy
+
+structure TContext (n m k : Nat) where
+  ctx : Capless.Context n m k
+  map : TMap n m k
+
+def TContext.empty : TContext 0 0 0 :=
+  ⟨Capless.Context.empty, TMap.empty⟩
+
+def TContext.var
+  (Γ : TContext n m k)
+  (T : Capless.CType n m (k+1)) :
+  TContext (n+1) m (k+1) :=
+  ⟨((Γ.ctx,c:CapSet),x:T), Γ.map.ext⟩
+
+def TContext.tvar
+  (Γ : TContext n m k)
+  (S : Capless.SType n m (k+1)) :
+  TContext n (m+1) (k+1) :=
+  ⟨((Γ.ctx,c:CapSet),X<:S), Γ.map.text⟩
+
+end Cappy
diff --git a/Cappy/Translation/TMap.lean b/Cappy/Translation/TMap.lean
new file mode 100644
index 00000000..8d77a296
--- /dev/null
+++ b/Cappy/Translation/TMap.lean
@@ -0,0 +1,69 @@
+import Aesop
+import Mathlib.Data.Fin.Basic
+import Capless.Basic
+namespace Cappy
+
+structure TMap (n m k : Nat) where
+  reach : Fin n -> Fin k
+  treach : Fin m -> Fin k
+
+def TMap.empty : TMap 0 0 0 := ⟨id, id⟩
+
+def TMap.ext (ρ : TMap n m k) : TMap (n+1) m (k+1) := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    apply Capless.FinFun.ext
+    aesop
+  case treach =>
+    have h := ρ.treach
+    intro x
+    apply Fin.succ
+    aesop
+
+def TMap.text (ρ : TMap n m k) : TMap n (m+1) (k+1) := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    intro x
+    apply Fin.succ
+    aesop
+  case treach =>
+    have h := ρ.treach
+    apply Capless.FinFun.ext
+    aesop
+
+def TMap.cweaken (ρ : TMap n m k) : TMap n m (k+1) := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    intro x
+    apply Fin.succ
+    aesop
+  case treach =>
+    have h := ρ.treach
+    intro x
+    apply Fin.succ
+    aesop
+
+def TMap.strip (ρ : TMap (n+1) m k) : TMap n m k := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    intro n
+    exact h (n.succ)
+  case treach =>
+    have h := ρ.treach
+    aesop
+
+def TMap.tstrip (ρ : TMap n (m+1) k) : TMap n m k := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    aesop
+  case treach =>
+    have h := ρ.treach
+    intro m
+    exact h (m.succ)
+
+end Cappy
diff --git a/Cappy/TypeSystem.lean b/Cappy/TypeSystem.lean
new file mode 100644
index 00000000..627f761b
--- /dev/null
+++ b/Cappy/TypeSystem.lean
@@ -0,0 +1,3 @@
+import Cappy.TypeSystem.Subcapturing
+import Cappy.TypeSystem.Subtyping
+import Cappy.TypeSystem.Typing
diff --git a/Cappy/TypeSystem/Subcapturing.lean b/Cappy/TypeSystem/Subcapturing.lean
new file mode 100644
index 00000000..d387c117
--- /dev/null
+++ b/Cappy/TypeSystem/Subcapturing.lean
@@ -0,0 +1,21 @@
+import Cappy.Syntax.Context
+namespace Cappy
+
+inductive Subcapt : Context n m -> CaptureSet n -> CaptureSet n -> Prop where
+| sc_trans :
+  Subcapt Γ C1 C2 ->
+  Subcapt Γ C2 C3 ->
+  Subcapt Γ C1 C3
+| sc_var :
+  Context.Bound Γ x (S^C) ->
+  Subcapt Γ {x=x} C
+| sc_elem {C1 C2 : CaptureSet n} :
+  C1 ⊆ C2 ->
+  Subcapt Γ C1 C2
+| sc_set :
+  Subcapt Γ C1 C ->
+  Subcapt Γ C2 C ->
+  Subcapt Γ (C1 ∪ C2) C
+
+
+end Cappy
diff --git a/Cappy/TypeSystem/Subtyping.lean b/Cappy/TypeSystem/Subtyping.lean
new file mode 100644
index 00000000..3e32e618
--- /dev/null
+++ b/Cappy/TypeSystem/Subtyping.lean
@@ -0,0 +1,44 @@
+import Cappy.TypeSystem.Subcapturing
+namespace Cappy
+
+inductive SubAnnot : Annot -> Annot -> Prop where
+| refl :
+  SubAnnot a a
+| use :
+  SubAnnot Annot.eps Annot.use
+
+mutual
+
+inductive CSubtyp : Context n m -> CType n m -> CType n m -> Prop where
+| capt :
+  Subcapt Γ C1 C2 ->
+  SSubtyp Γ S1 S2 ->
+  CSubtyp Γ (S1^C1) (S2^C2)
+
+inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
+| top :
+  SSubtyp Γ S SType.top
+| refl :
+  SSubtyp Γ S S
+| trans :
+  SSubtyp Γ S1 S2 ->
+  SSubtyp Γ S2 S3 ->
+  SSubtyp Γ S1 S3
+| tvar :
+  Context.TBound Γ X S ->
+  SSubtyp Γ (SType.tvar X) S
+| boxed :
+  CSubtyp Γ T1 T2 ->
+  SSubtyp Γ (SType.boxed T1) (SType.boxed T2)
+| arrow :
+  SubAnnot a1 a2 ->
+  CSubtyp (Γ.var T) U1 U2 ->
+  SSubtyp Γ (SType.arrow a1 T U1) (SType.arrow a2 T U2)
+| tarrow :
+  CSubtyp (Γ.tvar S) T1 T2 ->
+  SSubtyp Γ (∀[X<:S]T1) (∀[X<:S]T2)
+
+end
+
+
+end Cappy
diff --git a/Cappy/TypeSystem/Typing.lean b/Cappy/TypeSystem/Typing.lean
new file mode 100644
index 00000000..03bc595a
--- /dev/null
+++ b/Cappy/TypeSystem/Typing.lean
@@ -0,0 +1,59 @@
+import Cappy.TypeSystem.Subtyping
+import Cappy.Syntax.Term
+namespace Cappy
+
+mutual
+
+inductive CType.CapRefine : CaptureSet n -> CType n m -> CType n m -> Prop where
+| r_capt :
+  SType.CapRefine D S S' ->
+  CType.CapRefine D (S^C) (S'^(C.open_cap D))
+
+inductive SType.CapRefine : CaptureSet n -> SType n m -> SType n m -> Prop where
+| r_top :
+  SType.CapRefine D top top
+| r_tvar :
+  SType.CapRefine D (SType.tvar X) (SType.tvar X)
+| r_fun :
+  CType.CapRefine (D.weaken ∪ {x=0} ∪ {x*=0}) U U' ->
+  SType.CapRefine D (SType.arrow a T U) (SType.arrow a T U')
+| r_tfun :
+  CType.CapRefine D T T' ->
+  SType.CapRefine D (SType.tarrow S T) (SType.tarrow S T')
+| r_boxed :
+  CType.CapRefine D T T' ->
+  SType.CapRefine D (SType.boxed T) (SType.boxed T')
+
+end
+
+inductive Typed : CaptureSet n -> Context n m -> Term n m -> CType n m -> Prop where
+| var :
+  Γ.Bound x (S^C) ->
+  S.CapRefine {x*=x} S' ->
+  Typed {x=x} Γ (Term.var x) (S'^{x=x})
+| sub :
+  Typed C Γ t T ->
+  Subcapt Γ C C' ->
+  CSubtyp Γ T T' ->
+  Typed C' Γ t T'
+| abs {C : CaptureSet n} :
+  Typed (C.weaken ∪ {x=0} ∪ {x*=0}) (Γ.var T) t U ->
+  Typed {} Γ (Term.abs Annot.eps T t) ((∀(x:T)U)^C)
+| uabs {C : CaptureSet n} :
+  Typed (C.weaken ∪ {x=0}) (Γ.var T) t U ->
+  Typed {} Γ (Term.abs Annot.use T t) ((∀(use x:T)U)^C)
+| tabs {C : CaptureSet n} :
+  Typed C (Γ.tvar S) t T ->
+  Typed {} Γ (Term.tabs S t) ((∀[X<:S]T)^C)
+| box {C : CaptureSet n} :
+  Typed C Γ (Term.var x) T ->
+  Typed {} Γ (Term.box x) ((SType.boxed T)^{})
+| unbox {C : CaptureSet n} :
+  Typed C Γ (Term.var x) ((SType.boxed (S^C))^{}) ->
+  Typed C Γ (Term.unbox C x) (S^C)
+| letin {C : CaptureSet n} {U : CType n m} :
+  Typed C Γ t T ->
+  Typed C.weaken (Γ.var T) u U.weaken ->
+  Typed C Γ (Term.letin t u) U
+
+end Cappy
diff --git a/lakefile.lean b/lakefile.lean
index a307e98d..b128391f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -14,3 +14,5 @@ require mathlib from git
 @[default_target]
 lean_lib «Capless» where
   -- add any library configuration options here
+
+lean_lib «Cappy» where