diff --git a/Capless/Tactics.lean b/Capless/Tactics.lean
index 3c8b95ac..3442051f 100644
--- a/Capless/Tactics.lean
+++ b/Capless/Tactics.lean
@@ -1,4 +1,5 @@
 macro "easy" : tactic => `(tactic| assumption)
+macro "sosorry" : tactic => `(tactic| all_goals sorry)
 macro "split_and" : tactic => `(tactic| repeat any_goals apply And.intro)
 macro "apply!" e:term : tactic => `(tactic| apply $e <;> easy)
 macro "apply?" e:term : tactic => `(tactic| apply $e <;> try easy)
diff --git a/Capybara.lean b/Capybara.lean
new file mode 100644
index 00000000..b7ad3ef2
--- /dev/null
+++ b/Capybara.lean
@@ -0,0 +1 @@
+import «Capybara».Syntax
diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean
new file mode 100644
index 00000000..421eac7a
--- /dev/null
+++ b/Capybara/Morphism/Core.lean
@@ -0,0 +1,286 @@
+import Mathlib.Data.Fin.Basic
+namespace Capybara
+/-!
+# Morphisms
+
+This module defines morphisms between contexts in the Capybara type system.
+
+## Main definitions
+
+- `FinFun n n'`: A function mapping finite indices from dimension `n` to dimension `n'`
+- `Renaming n m k n' m' k'`: A renaming morphism that maps between contexts with dimensions:
+  - `n` term variables to `n'` term variables
+  - `m` type variables to `m'` type variables
+  - `k` capture set variables to `k'` capture set variables
+- `CaptureRenaming n k n' k'`: A renaming morphism that maps between capture sets with only two dimensions: terms and captures.
+
+## Implementation Notes
+
+Renamings are used to implement variable substitution and weakening in a well-typed way.
+The three dimensions (term, type, and capture set variables) are handled separately but
+in parallel through the `Renaming` structure.
+
+Each dimension can be extended independently through the `ext`, `text` and `cext` operations
+which add a new variable while preserving the existing mapping.
+
+note: Sonnet wrote this documentation.
+-/
+
+/-!
+A renaming function maps indices from one dimension to another.
+-/
+def FinFun (n : Nat) (n' : Nat) : Type := Fin n -> Fin n'
+
+/-!
+Extend a renaming function by one on the term variable dimension.
+-/
+def FinFun.ext (f : FinFun n n') : FinFun (n+1) (n'+1) := by
+  intro x
+  cases x using Fin.cases
+  case zero => exact 0
+  case succ x0 => exact Fin.succ (f x0)
+
+def FinFun.id {n : Nat} : FinFun n n := fun x => x
+
+/-!
+A weaken function that shifts all indices by one.
+-/
+def FinFun.weaken {n : Nat} : FinFun n (n+1) := by
+  intro x
+  exact Fin.succ x
+
+/-!
+Open a bound variable.
+-/
+def FinFun.open {n : Nat} (x : Fin n) : FinFun (n+1) n := by
+  intro y
+  cases y using Fin.cases
+  case zero => exact x
+  case succ y0 => exact y0
+
+/-!
+A renaming function, which maps the three dimensions of a context (term, type, and capture set variables).
+-/
+structure Renaming (n m k n' m' k' : Nat) where
+  var : FinFun n n'
+  tvar : FinFun m m'
+  cvar : FinFun k k'
+
+/-!
+Capture renaming function.
+-/
+structure CaptureRenaming (n k n' k' : Nat) where
+  var : FinFun n n'
+  cvar : FinFun k k'
+
+def Renaming.asCapt (ρ : Renaming n m k n' m' k') : CaptureRenaming n k n' k' :=
+  {
+    var := ρ.var
+    cvar := ρ.cvar
+  }
+
+/-!
+Extend a renaming function by one on the term variable dimension.
+-/
+def Renaming.ext (ρ : Renaming n m k n' m' k') :
+  Renaming (n+1) m k (n'+1) m' k' :=
+  {
+    var := ρ.var.ext
+    tvar := ρ.tvar
+    cvar := ρ.cvar
+  }
+
+/-!
+Extend a renaming function by one on the type variable dimension.
+-/
+def Renaming.text (ρ : Renaming n m k n' m' k') :
+  Renaming n (m+1) k n' (m'+1) k' :=
+  {
+    var := ρ.var
+    tvar := ρ.tvar.ext
+    cvar := ρ.cvar
+  }
+
+/-!
+Extend a renaming function by one on the capture set variable dimension.
+-/
+def Renaming.cext (ρ : Renaming n m k n' m' k') :
+  Renaming n m (k+1) n' m' (k'+1) :=
+  {
+    var := ρ.var
+    tvar := ρ.tvar
+    cvar := ρ.cvar.ext
+  }
+
+/-!
+Weaken the renaming by one on the term variable dimension.
+-/
+def Renaming.weaken : Renaming n m k (n+1) m k :=
+  {
+    var := FinFun.weaken
+    tvar := FinFun.id
+    cvar := FinFun.id
+  }
+
+/-!
+Weaken the renaming by one on the type variable dimension.
+-/
+def Renaming.tweaken : Renaming n m k n (m+1) k :=
+  {
+    var := FinFun.id
+    tvar := FinFun.weaken
+    cvar := FinFun.id
+  }
+
+/-!
+Weaken the renaming by one on the capture variable dimension.
+-/
+def Renaming.cweaken : Renaming n m k n m (k+1) :=
+  {
+    var := FinFun.id
+    tvar := FinFun.id
+    cvar := FinFun.weaken
+  }
+
+def Renaming.open (x : Fin n) : Renaming (n+1) m k n m k :=
+  {
+    var := FinFun.open x
+    tvar := FinFun.id
+    cvar := FinFun.id
+  }
+
+def Renaming.topen (X : Fin m) : Renaming n (m+1) k n m k :=
+  {
+    var := FinFun.id
+    tvar := FinFun.open X
+    cvar := FinFun.id
+  }
+
+def Renaming.copen (X : Fin k) : Renaming n m (k+1) n m k :=
+  {
+    var := FinFun.id
+    tvar := FinFun.id
+    cvar := FinFun.open X
+  }
+
+def Renaming.id : Renaming n m k n m k :=
+  {
+    var := FinFun.id
+    tvar := FinFun.id
+    cvar := FinFun.id
+  }
+
+def FinFun.comp (f : FinFun n n') (g : FinFun n' n'') : FinFun n n'' :=
+  fun x => g (f x)
+
+def Renaming.comp (ρ : Renaming n m k n' m' k') (ρ' : Renaming n' m' k' n'' m'' k'') : Renaming n m k n'' m'' k'' :=
+  {
+    var := ρ.var.comp ρ'.var
+    tvar := ρ.tvar.comp ρ'.tvar
+    cvar := ρ.cvar.comp ρ'.cvar
+  }
+
+def CaptureRenaming.comp (ρ : CaptureRenaming n k n' k') (ρ' : CaptureRenaming n' k' n'' k'') : CaptureRenaming n k n'' k'' :=
+  {
+    var := ρ.var.comp ρ'.var
+    cvar := ρ.cvar.comp ρ'.cvar
+  }
+
+/-!
+Basic properties of renamings.
+-/
+theorem Renaming.ext_var_zero {ρ : Renaming n m k n' m' k'} : ρ.ext.var 0 = 0 := by
+  simp [Renaming.ext]
+  rfl
+
+theorem Renaming.ext_var_succ {ρ : Renaming n m k n' m' k'} {x : Fin n} : ρ.ext.var (Fin.succ x) = Fin.succ (ρ.var x) := by
+  simp [Renaming.ext]
+  rfl
+
+theorem FinFun.id_comp_id {n : Nat} : FinFun.comp (n:=n) FinFun.id FinFun.id = FinFun.id := by rfl
+
+theorem Renaming.id_comp_id {n m k : Nat} : Renaming.comp (n:=n) (m:=m) (k:=k) Renaming.id Renaming.id = Renaming.id := by rfl
+
+theorem FinFun.id_ext {n : Nat} : FinFun.ext (n:=n) FinFun.id = FinFun.id := by
+  funext x0
+  cases x0 using Fin.cases
+  case zero => simp [FinFun.id, FinFun.ext]
+  case succ x0 => simp [FinFun.id, FinFun.ext]
+
+theorem Renaming.id_ext {n m k : Nat} : Renaming.ext (n:=n) (m:=m) (k:=k) Renaming.id = Renaming.id := by simp [Renaming.ext, Renaming.id, FinFun.id_ext]
+
+theorem Renaming.id_text {n m k : Nat} : Renaming.text (n:=n) (m:=m) (k:=k) Renaming.id = Renaming.id := by simp [Renaming.text, Renaming.id, FinFun.id_ext]
+
+theorem Renaming.id_cext {n m k : Nat} : Renaming.cext (n:=n) (m:=m) (k:=k) Renaming.id = Renaming.id := by simp [Renaming.cext, Renaming.id, FinFun.id_ext]
+
+theorem FinFun.comp_ext {f : FinFun n n'} {g : FinFun n' n''} : (f.comp g).ext = f.ext.comp g.ext := by
+  funext x
+  cases x using Fin.cases
+  case zero => rfl
+  case succ x0 => simp [FinFun.comp, FinFun.ext]
+
+theorem Renaming.comp_ext {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} :
+  (ρ.comp ρ').ext = ρ.ext.comp ρ'.ext := by
+  simp [Renaming.ext, Renaming.comp, FinFun.comp_ext]
+
+theorem Renaming.comp_text {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} :
+  (ρ.comp ρ').text = ρ.text.comp ρ'.text := by
+  simp [Renaming.text, Renaming.comp, FinFun.comp_ext]
+
+theorem Renaming.comp_cext {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} :
+  (ρ.comp ρ').cext = ρ.cext.comp ρ'.cext := by
+  simp [Renaming.cext, Renaming.comp, FinFun.comp_ext]
+
+theorem FinFun.comp_weaken {f : FinFun n n'} :
+  f.comp FinFun.weaken = FinFun.weaken.comp (f.ext) := by
+  funext x
+  simp [FinFun.comp, FinFun.weaken, FinFun.ext]
+
+theorem FinFun.comp_id {f : FinFun n n'} : f.comp FinFun.id = f := by
+  funext x
+  simp [FinFun.comp, FinFun.id]
+
+theorem FinFun.id_comp {f : FinFun n n'} : FinFun.id.comp f = f := by
+  funext x
+  simp [FinFun.comp, FinFun.id]
+
+theorem Renaming.comp_weaken {ρ : Renaming n m k n' m' k'} :
+  ρ.comp Renaming.weaken = Renaming.weaken.comp ρ.ext := by
+  simp [Renaming.weaken, Renaming.comp, Renaming.ext]
+  simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp]
+
+theorem Renaming.comp_tweaken {ρ : Renaming n m k n' m' k'} :
+  ρ.comp Renaming.tweaken = Renaming.tweaken.comp ρ.text := by
+  simp [Renaming.tweaken, Renaming.comp, Renaming.text]
+  simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp]
+
+theorem Renaming.comp_cweaken {ρ : Renaming n m k n' m' k'} :
+  ρ.comp Renaming.cweaken = Renaming.cweaken.comp ρ.cext := by
+  simp [Renaming.cweaken, Renaming.comp, Renaming.cext]
+  simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp]
+
+theorem Renaming.comp_asCapt {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} :
+  (ρ.comp ρ').asCapt = ρ.asCapt.comp ρ'.asCapt := by
+  simp [Renaming.asCapt, CaptureRenaming.comp, Renaming.comp]
+
+theorem Renaming.weaken_transportM {n m1 m2 k : Nat} :
+  (Renaming.weaken (n:=n) (m:=m1) (k:=k)).asCapt =
+    (Renaming.weaken (n:=n) (m:=m2) (k:=k)).asCapt := by
+  simp [Renaming.weaken, Renaming.asCapt]
+
+theorem Renaming.cweaken_transportM {n m1 m2 k : Nat} :
+  (Renaming.cweaken (n:=n) (m:=m1) (k:=k)).asCapt =
+    (Renaming.cweaken (n:=n) (m:=m2) (k:=k)).asCapt := by
+  simp [Renaming.cweaken, Renaming.asCapt]
+
+@[simp]
+theorem Renaming.text_asCapt {ρ : Renaming n m k n' m' k'} :
+  ρ.text.asCapt = ρ.asCapt := by
+  simp [text, asCapt]
+
+@[simp]
+theorem Renaming.asCapt_var {ρ : Renaming n m k n' m' k'} :
+  ρ.asCapt.var = ρ.var := by
+  simp [asCapt]
+
+end Capybara
diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean
new file mode 100644
index 00000000..4690f9f9
--- /dev/null
+++ b/Capybara/Morphism/Rebinding.lean
@@ -0,0 +1,108 @@
+import Capless.Tactics
+import Capybara.Syntax
+import Capybara.Morphism.Core
+namespace Capybara
+
+/-!
+# Rebinding
+
+## Definition
+A rebinding is a morphism from a source context `Γ` to a target context `Δ` that maps each binding in `Γ` to an equivalent one in `Δ`.
+-/
+structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where
+  ρ : Renaming n m k n' m' k'
+  var : ∀ {x T}, Γ.Lookup x T -> Δ.Lookup (ρ.var x) (T.rename ρ)
+  tvar : ∀ {X S}, Γ.LookupT X S -> Δ.LookupT (ρ.tvar X) (S.rename ρ)
+  cvar : ∀ {c K}, Γ.LookupC c K -> Δ.LookupC (ρ.cvar c) (K.rename ρ.asCapt)
+
+/-!
+## Extensions
+The following methods lift rebindings to environments with more bindings.
+-/
+def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ.ρ) := by
+  constructor
+  case ρ => exact θ.ρ.ext
+  case var =>
+    intro x T hb
+    cases hb with
+    | here =>
+      simp [Renaming.ext_var_zero]
+      simp [<-CType.rename_weaken]
+      constructor
+    | there h =>
+      simp [Renaming.ext_var_succ]
+      simp [<-CType.rename_weaken]
+      constructor
+      apply θ.var; easy
+  case tvar =>
+    intro X S hb
+    cases hb
+    case there hb =>
+      simp [<-TBinding.rename_weaken]
+      constructor
+      apply θ.tvar; easy
+  case cvar =>
+    intro c B hb
+    cases hb
+    case there hb =>
+      simp [<-CBinding.rename_weaken]
+      constructor
+      apply θ.cvar; easy
+
+def Rebinding.text (θ : Rebinding Γ Δ) : Rebinding (Γ,X:B) (Δ,X:B.rename θ.ρ) := by
+  constructor
+  case ρ => exact θ.ρ.text
+  case var =>
+    intro x T hb
+    cases hb
+    case tthere hb =>
+      simp [<-CType.rename_tweaken]
+      constructor
+      apply θ.var; easy
+  case tvar =>
+    intro X B hb
+    cases hb
+    case here =>
+      simp [<-TBinding.rename_tweaken]
+      constructor
+    case tthere hb =>
+      simp [<-TBinding.rename_tweaken]
+      constructor
+      apply θ.tvar; easy
+  case cvar =>
+    intro c B hb
+    cases hb
+    case tthere hb =>
+      simp
+      constructor
+      apply θ.cvar; easy
+
+def Rebinding.cext (θ : Rebinding Γ Δ) : Rebinding (Γ,c:K) (Δ,c:K.rename θ.ρ.asCapt) := by
+  constructor
+  case ρ => exact θ.ρ.cext
+  case var =>
+    intro x T hb
+    cases hb
+    case cthere hb =>
+      simp [<-CType.rename_cweaken]
+      constructor
+      apply θ.var; easy
+  case tvar =>
+    intro X B hb
+    cases hb
+    case cthere hb =>
+      simp [<-TBinding.rename_cweaken]
+      constructor
+      apply θ.tvar; easy
+  case cvar =>
+    intro c K hb
+    cases hb
+    case here =>
+      simp [<-CBinding.rename_cweaken]
+      constructor
+    case cthere hb =>
+      simp [<-CBinding.rename_cweaken]
+      constructor
+      apply θ.cvar; easy
+
+end Capybara
diff --git a/Capybara/Rebinding/Subcapturing.lean b/Capybara/Rebinding/Subcapturing.lean
new file mode 100644
index 00000000..020d1dbe
--- /dev/null
+++ b/Capybara/Rebinding/Subcapturing.lean
@@ -0,0 +1,49 @@
+import Capybara.StaticSemantics
+import Capybara.Morphism.Rebinding
+namespace Capybara
+
+theorem Subcapturing.rebind
+  (h : Γ ⊢c C1 <: C2)
+  (θ : Rebinding Γ Δ) :
+  Δ ⊢c (C1.rename θ.ρ.asCapt) <: (C2.rename θ.ρ.asCapt) := by
+  induction h
+  case subset hs =>
+    apply Subcapturing.subset
+    apply CaptureSet.rename_subset hs
+  case trans ih1 ih2 =>
+    apply Subcapturing.trans
+    · exact ih1 θ
+    · exact ih2 θ
+  case union ih1 ih2 =>
+    apply Subcapturing.union
+    · exact ih1 θ
+    · exact ih2 θ
+  case mode h1 h2 =>
+    simp [CaptureSet.qualified_rename]
+    apply mode; easy
+  case var hb =>
+    simp [CaptureSet.rename]
+    simp [CaptureSet.qualified_rename]
+    apply var
+    have hb1 := θ.var hb
+    exact hb1
+  case rovar hb =>
+    simp [CaptureSet.rename]
+    simp [CaptureSet.qualified_rename]
+    apply rovar
+    have hb1 := θ.var hb
+    exact hb1
+  case cvar_l hb =>
+    simp [CaptureSet.rename]
+    simp [CaptureSet.qualified_rename]
+    apply cvar_l
+    have hb1 := θ.cvar hb
+    exact hb1
+  case cvar_r hb =>
+    simp [CaptureSet.rename]
+    simp [CaptureSet.qualified_rename]
+    apply cvar_r
+    have hb1 := θ.cvar hb
+    exact hb1
+
+end Capybara
diff --git a/Capybara/Rebinding/Subtyping.lean b/Capybara/Rebinding/Subtyping.lean
new file mode 100644
index 00000000..05c8c10d
--- /dev/null
+++ b/Capybara/Rebinding/Subtyping.lean
@@ -0,0 +1,116 @@
+import Capybara.StaticSemantics
+import Capybara.Rebinding.Subcapturing
+namespace Capybara
+
+private def motive_1
+  (Γ : Context n m k) (S1 S2 : SType n m k)
+  (_ : SSubtyping Γ S1 S2) : Prop :=
+  ∀ {n' m' k'} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ), SSubtyping Δ (S1.rename θ.ρ) (S2.rename θ.ρ)
+
+private def motive_2
+  (Γ : Context n m k) (T1 T2 : CType n m k)
+  (_ : CSubtyping Γ T1 T2) : Prop :=
+  ∀ {n' m' k'} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ), CSubtyping Δ (T1.rename θ.ρ) (T2.rename θ.ρ)
+
+private def motive_3
+  (Γ : Context n m k) (E1 E2 : EType n m k)
+  (_ : ESubtyping Γ E1 E2) : Prop :=
+  ∀ {n' m' k'} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ), ESubtyping Δ (E1.rename θ.ρ) (E2.rename θ.ρ)
+
+syntax "unfold_all" : tactic
+
+macro_rules
+  | `(tactic| unfold_all) => `(tactic| try unfold motive_1 at *; try unfold motive_2 at *; try unfold motive_3 at *)
+
+theorem SSubtyping.rebind
+  (h : SSubtyping Γ S1 S2)
+  (θ : Rebinding Γ Δ) :
+  SSubtyping Δ (S1.rename θ.ρ) (S2.rename θ.ρ) := by
+  apply SSubtyping.rec
+    (motive_1:=motive_1)
+    (motive_2:=motive_2)
+    (motive_3:=motive_3)
+    (t:=h)
+  all_goals (unfold_all; repeat intro)
+  case top => constructor
+  case refl => apply SSubtyping.refl
+  case trans =>
+    rename_i ih1 ih2 _ _ _ _ _
+    apply trans <;> aesop
+  case tvar =>
+    rename_i hb _ _ _ _ θ
+    apply tvar
+    have hb1 := θ.tvar hb
+    exact hb1
+  case arrow T2 T1 _ _ _ _ ih1 ih2 _ _ _ _ θ =>
+    simp [SType.rename]
+    apply arrow
+    { aesop }
+    { let θ' := θ.ext (T:=T2)
+      apply ih2 θ' }
+  case tarrow S2 S1 _ _ _ _ ih1 ih2 _ _ _ _ θ =>
+    unfold motive_3 at ih2
+    simp [SType.rename]
+    apply tarrow
+    { aesop }
+    { let θ' := θ.text (B:=tparam S2)
+      apply ih2 θ' }
+  case carrow K _ _ _ ih _ _ _ _ θ =>
+    unfold motive_3 at ih
+    simp [SType.rename]
+    apply carrow
+    { let θ' := θ.cext (K:=cparam (CKind.Sep K))
+      apply ih θ' }
+  case talias_l hb _ _ _ _ θ =>
+    simp [SType.rename]
+    apply talias_l
+    have hb1 := θ.tvar hb
+    exact hb1
+  case talias_r hb _ _ _ _ θ =>
+    simp [SType.rename]
+    apply talias_r
+    have hb1 := θ.tvar hb
+    exact hb1
+  case capt ih _ _ _ _ θ =>
+    simp [CType.rename]
+    apply CSubtyping.capt
+    { aesop }
+    { apply Subcapturing.rebind; easy }
+  case type ih _ _ _ _ θ =>
+    simp [EType.rename]
+    apply ESubtyping.type
+    { aesop }
+  case ex ih _ _ _ _ θ =>
+    unfold motive_2 at ih
+    simp [EType.rename]
+    apply ESubtyping.ex
+    let θ' := θ.cext (K:=cparam CKind.Fresh)
+    apply ih θ'
+
+theorem CSubtyping.rebind
+  (h : CSubtyping Γ T1 T2)
+  (θ : Rebinding Γ Δ) :
+  CSubtyping Δ (T1.rename θ.ρ) (T2.rename θ.ρ) := by
+  cases h
+  case capt hs hc =>
+    simp [CType.rename]
+    apply CSubtyping.capt
+    { apply SSubtyping.rebind; easy }
+    { apply Subcapturing.rebind; easy }
+
+theorem ESubtyping.rebind
+  (h : ESubtyping Γ E1 E2)
+  (θ : Rebinding Γ Δ) :
+  ESubtyping Δ (E1.rename θ.ρ) (E2.rename θ.ρ) := by
+  cases h
+  case type hc =>
+    simp [EType.rename]
+    apply ESubtyping.type
+    apply CSubtyping.rebind; easy
+  case ex hc =>
+    simp [EType.rename]
+    apply ESubtyping.ex
+    let θ' := θ.cext (K:=cparam CKind.Fresh)
+    apply CSubtyping.rebind hc θ'
+
+end Capybara
diff --git a/Capybara/Rebinding/Typing.lean b/Capybara/Rebinding/Typing.lean
new file mode 100644
index 00000000..d50430a0
--- /dev/null
+++ b/Capybara/Rebinding/Typing.lean
@@ -0,0 +1,37 @@
+import Capybara.StaticSemantics
+import Capybara.Rebinding.Subtyping
+namespace Capybara
+
+theorem Typed.rebind {Γ : Context n m k} {Δ : Context n' m' k'}
+  (h : Typed C Γ t E)
+  (θ : Rebinding Γ Δ) :
+  Typed (C.rename θ.ρ.asCapt) Δ (t.rename θ.ρ) (E.rename θ.ρ) := by
+  induction h generalizing n' m' k' Δ
+  case var =>
+    sorry
+  case pack =>
+    sorry
+  case subc =>
+    sorry
+  case abs =>
+    sorry
+  case tabs =>
+    sorry
+  case cabs =>
+    sorry
+  case fabs =>
+    sorry
+  case app =>
+    sorry
+  case tapp =>
+    sorry
+  case capp =>
+    sorry
+  case fapp =>
+    sorry
+  case letin =>
+    sorry
+  case unpack =>
+    sorry
+
+end Capybara
diff --git a/Capybara/StaticSemantics.lean b/Capybara/StaticSemantics.lean
new file mode 100644
index 00000000..b7e1f581
--- /dev/null
+++ b/Capybara/StaticSemantics.lean
@@ -0,0 +1,3 @@
+import Capybara.StaticSemantics.Subcapturing
+import Capybara.StaticSemantics.Subtyping
+import Capybara.StaticSemantics.Typing
diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean
new file mode 100644
index 00000000..9e82e05e
--- /dev/null
+++ b/Capybara/StaticSemantics/CaptureRoot.lean
@@ -0,0 +1,37 @@
+import Capybara.Syntax
+namespace Capybara
+
+structure CaptureRoot (k : Nat) : Type where
+  m : Mode
+  c : Fin k
+
+/-!
+`ReachRoot Γ C m c` means that the root `c` is reachable at access mode `m` from the capture set `C` under the context `Γ`.
+-/
+inductive ReachRoot : Context n m k -> CaptureSet n k -> CaptureRoot k -> Prop where
+| union_l :
+  ReachRoot Γ C1 ⟨m,c⟩ ->
+  ReachRoot Γ (C1 ∪ C2) ⟨m,c⟩
+| union_r :
+  ReachRoot Γ C2 ⟨m,c⟩ ->
+  ReachRoot Γ (C1 ∪ C2) ⟨m,c⟩
+| var :
+  Context.Lookup Γ x (S^[m]C) ->
+  ReachRoot Γ ((C.qualified (Mode.M m)).qualified mu) ⟨mu',c⟩ ->
+  ReachRoot Γ ({x@mu:=x}) ⟨mu',c⟩
+| cvar_alias :
+  Context.LookupC Γ c (calias C) ->
+  ReachRoot Γ (C.qualified mu) ⟨mu',c'⟩ ->
+  ReachRoot Γ ({c@mu:=c}) ⟨mu',c'⟩
+| cvar :
+  Context.LookupC Γ c (cparam K) ->
+  ReachRoot Γ ({c@mu:=c}) ⟨mu,c⟩
+
+inductive RORoot : Context n m k -> CaptureRoot k -> Prop where
+| ro :
+  RORoot Γ ⟨ro,c⟩
+| imm :
+  Context.LookupC Γ c (cparam (CKind.Sep ⟨SepMode.Imm, D⟩)) ->
+  RORoot Γ ⟨Mode.M m,c⟩
+
+end Capybara
diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean
new file mode 100644
index 00000000..b574bdf3
--- /dev/null
+++ b/Capybara/StaticSemantics/Chaining.lean
@@ -0,0 +1,17 @@
+import Capybara.StaticSemantics.CaptureRoot
+namespace Capybara
+
+/-!
+`Γ ⊢ C1 >> C2` means that the effects of `C1` and `C2` are chainable.
+
+Specifically, anything that has been dropped from `C1` cannot be mentioned by `C2` any more.
+-/
+def Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop :=
+  ∀c, ReachRoot Γ C1 ⟨drop,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False
+
+def DroppedChaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop :=
+  ∀μ c, ReachRoot Γ C1 ⟨μ,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False
+
+notation:50 Γ " ⊢ " C1 " >> " C2 => CaptureSet.Chaining Γ C1 C2
+
+end Capybara
diff --git a/Capybara/StaticSemantics/Kinding.lean b/Capybara/StaticSemantics/Kinding.lean
new file mode 100644
index 00000000..77fdef9b
--- /dev/null
+++ b/Capybara/StaticSemantics/Kinding.lean
@@ -0,0 +1,18 @@
+import Capybara.Syntax
+import Capybara.StaticSemantics.CaptureRoot
+import Capybara.StaticSemantics.Separation
+namespace Capybara
+
+inductive Kinding : Context n m k -> CaptureSet n k -> CKind n k -> Prop where
+| fresh :
+  (∀c m, ReachRoot Γ C ⟨Mode.M m,c⟩ -> Context.LookupC Γ c (cparam CKind.Fresh)) ->
+  Kinding Γ C CKind.Fresh
+| sep_mut :
+  Separation Γ C D ->
+  Kinding Γ C (CKind.Sep ⟨SepMode.Mut, D⟩)
+| sep_imm :
+  Separation Γ C D ->
+  (∀r, ReachRoot Γ C r -> RORoot Γ r) ->
+  Kinding Γ C (CKind.Sep ⟨SepMode.Imm, D⟩)
+
+end Capybara
diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean
new file mode 100644
index 00000000..1dfc03ae
--- /dev/null
+++ b/Capybara/StaticSemantics/Separation.lean
@@ -0,0 +1,32 @@
+import Capybara.StaticSemantics.CaptureRoot
+namespace Capybara
+
+/-!
+Separation checking.
+-/
+
+inductive RootSeparation : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop where
+| symm :
+  RootSeparation Γ r1 r2 ->
+  RootSeparation Γ r2 r1
+| ro :
+  RORoot Γ r1 ->
+  RORoot Γ r2 ->
+  RootSeparation Γ r1 r2
+| rw :
+  RootSeparation Γ ⟨ε,c1⟩ r2 ->
+  RootSeparation Γ ⟨ro,c1⟩ r2
+| sep :
+  Context.LookupC Γ c (cparam (CKind.Sep ⟨s,D⟩)) ->
+  ReachRoot Γ D r2 ->
+  RootSeparation Γ ⟨ε,c⟩ r2
+| fresh :
+  Context.LookupC Γ c1 (cparam CKind.Fresh) ->
+  Context.LookupC Γ c2 (cparam CKind.Fresh) ->
+  (c1 ≠ c2) ->
+  RootSeparation Γ ⟨μ1,c1⟩ ⟨μ2,c2⟩
+
+def Separation (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop :=
+  ∀r1 r2, ReachRoot Γ C1 r1 -> ReachRoot Γ C2 r2 -> RootSeparation Γ r1 r2
+
+end Capybara
diff --git a/Capybara/StaticSemantics/Subcapturing.lean b/Capybara/StaticSemantics/Subcapturing.lean
new file mode 100644
index 00000000..0ae5110e
--- /dev/null
+++ b/Capybara/StaticSemantics/Subcapturing.lean
@@ -0,0 +1,44 @@
+import Capybara.Syntax
+namespace Capybara
+
+/-!
+Subcapturing relation.
+
+There are three structural rules:
+- `subset`: if `C1 ⊆ C2`, then `C1` subcaptures `C2`.
+- `trans`: if `C1` subcaptures `C2` and `C2` subcaptures `C3`, then `C1` subcaptures `C3`.
+- `union`: if `C1` subcaptures `C` and `C2` subcaptures `C`, then `C1 ∪ C2` subcaptures `C`.
+
+Two rules for variables, one for default (mutable) captures and the other for read-only captures. Two similar rules for capture set aliases.
+-/
+inductive Subcapturing : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where
+| subset :
+  (C1 ⊆ C2) ->
+  Subcapturing Γ C1  C2
+| trans :
+  Subcapturing Γ C1 C2 ->
+  Subcapturing Γ C2 C3 ->
+  Subcapturing Γ C1 C3
+| union :
+  Subcapturing Γ C1 C ->
+  Subcapturing Γ C2 C ->
+  Subcapturing Γ (C1 ∪ C2) C
+| mode {C : CaptureSet n k} :
+  Mode.LessPermissive m1 m2 ->
+  Subcapturing Γ (C.qualified m1) (C.qualified m2)
+| var :
+  Context.Lookup Γ x (CType.capt C m S) ->
+  Subcapturing Γ ({x:=x}) (C.qualified (Mode.M m))
+| rovar :
+  Context.Lookup Γ x (CType.capt C m S) ->
+  Subcapturing Γ ({x@ro:=x}) (C.qualified ro)
+| cvar_l :
+  Context.LookupC Γ c (calias C) ->
+  Subcapturing Γ ({c@m:=c}) (C.qualified m)
+| cvar_r :
+  Context.LookupC Γ c (calias C) ->
+  Subcapturing Γ (C.qualified m) ({c@m:=c})
+
+notation:50 Γ " ⊢c " C1 "<:" C2 => Subcapturing Γ C1 C2
+
+end Capybara
diff --git a/Capybara/StaticSemantics/Subtyping.lean b/Capybara/StaticSemantics/Subtyping.lean
new file mode 100644
index 00000000..52d29efc
--- /dev/null
+++ b/Capybara/StaticSemantics/Subtyping.lean
@@ -0,0 +1,57 @@
+import Capybara.Syntax
+import Capybara.StaticSemantics.Subcapturing
+namespace Capybara
+
+mutual
+
+inductive SSubtyping : Context n m k -> SType n m k -> SType n m k -> Prop
+| top :
+  SSubtyping Γ S ⊤
+| refl :
+  SSubtyping Γ S S
+| trans :
+  SSubtyping Γ S1 S2 ->
+  SSubtyping Γ S2 S3 ->
+  SSubtyping Γ S1 S3
+| tvar :
+  Context.LookupT Γ X (tparam S) ->
+  SSubtyping Γ (SType.tvar X) S
+| arrow :
+  CSubtyping Γ T2 T1 ->
+  ESubtyping (Γ,x:T2) E1 E2 ->
+  SSubtyping Γ ((x:T1)->E1) ((x:T2)->E2)
+| tarrow :
+  SSubtyping Γ S2 S1 ->
+  ESubtyping (Γ,X:tparam S2) E1 E2 ->
+  SSubtyping Γ ([X<:S1]->E1) ([X<:S2]->E2)
+| carrow :
+  ESubtyping (Γ,c:cparam (CKind.Sep K)) E1 E2 ->
+  SSubtyping Γ ([c:K]->E1) ([c:K]->E2)
+| talias_l :
+  Context.LookupT Γ X (talias S) ->
+  SSubtyping Γ (SType.tvar X) S
+| talias_r :
+  Context.LookupT Γ X (talias S) ->
+  SSubtyping Γ S (SType.tvar X)
+
+inductive CSubtyping : Context n m k -> CType n m k -> CType n m k -> Prop
+| capt :
+  SSubtyping Γ S1 S2 ->
+  (Γ ⊢c C1 <: C2) ->
+  CSubtyping Γ (S1^[m]C1) (S2^[m]C2)
+
+inductive ESubtyping : Context n m k -> EType n m k -> EType n m k -> Prop
+| type :
+  CSubtyping Γ T1 T2 ->
+  ESubtyping Γ (EType.type T1) (EType.type T2)
+| ex :
+  CSubtyping (Γ,c:cparam CKind.Fresh) T1 T2 ->
+  ESubtyping Γ (EType.ex T1) (EType.ex T2)
+
+end
+
+notation:50 Γ " ⊢s " S1 " <: " S2 => SSubtyping Γ S1 S2
+notation:50 Γ " ⊢ " C1 " <: " C2 => CSubtyping Γ C1 C2
+notation:50 Γ " ⊢e " E1 " <: " E2 => ESubtyping Γ E1 E2
+
+end Capybara
diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean
new file mode 100644
index 00000000..73461f03
--- /dev/null
+++ b/Capybara/StaticSemantics/Typing.lean
@@ -0,0 +1,92 @@
+import Capybara.StaticSemantics.CaptureRoot
+import Capybara.StaticSemantics.Chaining
+import Capybara.StaticSemantics.Separation
+import Capybara.StaticSemantics.Subtyping
+import Capybara.StaticSemantics.Kinding
+namespace Capybara
+
+/-!
+`RootDropped Γ C D` means that any capture root in `C` is dropped in `D`.
+-/
+def RootDropped (Γ : Context n m k) (C D : CaptureSet n k) : Prop :=
+  ∀ m c, ReachRoot Γ C ⟨m,c⟩ -> (Γ ⊢c {c@drop:=c} <: D)
+
+/-!
+The typing relation.
+-/
+inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k -> Prop where
+| var :
+  Γ.Lookup x (CType.capt C m S) ->
+  Mutability.LessPermissive m' m ->
+  --------------------------------
+  Typed ({x@Mode.M m':=x}) Γ (Term.var x) (EType.type (CType.capt ({x:=x}) m' S))
+| pack :
+  Typed C' Γ (Term.var x) (EType.type (T.copen c)) ->
+  RootDropped Γ ({c:=c}) C' ->
+  Kinding Γ ({c:=c}) CKind.Fresh ->
+  -----------------------------------------------------
+  Typed C' Γ (Term.pack c x) (EType.ex T)
+| subc :
+  Typed C Γ t E ->
+  (Γ ⊢c C <: C') ->
+  -----------------------------------
+  Typed C' Γ t E
+| abs :
+  Typed (C.weaken ∪ CaptureSet.span 0) (Γ,x:T) t E ->
+  ------------------------------------------------------------
+  Typed {} Γ (Term.lam T t) (EType.type (((x:T)->E)^[ε]C))
+| tabs :
+  Typed C (Γ,X:tparam S) t E ->
+  ------------------------------------------------------------
+  Typed C Γ (Term.tlam S t) (EType.type (([X<:S]->E)^[ε]C))
+| cabs :
+  Typed C.cweaken (Γ,c:cparam (CKind.Sep D)) t E ->
+  ------------------------------------------------------------
+  Typed C Γ (Term.clam D t) (EType.type (([c:D]->E)^[ε]C))
+| fabs :
+  Typed (C.cweaken.weaken ∪ CaptureSet.span 0) ((Γ,c:cparam CKind.Fresh),x:T) t E ->
+  ------------------------------------------------------------
+  Typed C Γ (Term.flam T t) (EType.type (([c:Fresh](x:T)->E)^[ε]C))
+| app :
+  Typed C' Γ (Term.var x) (EType.type (((x:T)->E)^[ε]Cf)) ->
+  Typed C' Γ (Term.var y) (EType.type T0) ->
+  (Γ ⊢ T0 <: T) ->
+  Chaining Γ ({x:=x}) ({x:=y}) ->
+  Chaining Γ ({x:=y}) ({x:=x}) ->
+  ------------------------------------------------------------
+  Typed C' Γ (Term.app x y) (E.open y)
+| tapp :
+  Typed C' Γ (Term.var x) (EType.type (([X<:S]->E)^[ε]Cf)) ->
+  (Γ ⊢s (SType.tvar X) <: S) ->
+  ------------------------------------------------------------
+  Typed C' Γ (Term.tapp x X) (E.topen X)
+| capp :
+  Typed C' Γ (Term.var x) (EType.type (([c:D]->E)^[ε]Cf)) ->
+  Kinding Γ ({c:=c}) (CKind.Sep D) ->
+  ------------------------------------------------------------
+  Typed C' Γ (Term.capp x c) (E.copen c)
+| fapp :
+  Typed C' Γ (Term.var x) (EType.type (([c:Fresh](x:T)->E)^[ε]Cf)) ->
+  Typed C' Γ (Term.var y) (EType.type T0) ->
+  (Γ ⊢ T0 <: (T.copen c)) ->
+  RootDropped Γ ({c:=c}) C' ->
+  Kinding Γ ({c:=c}) CKind.Fresh ->
+  DroppedChaining Γ ({c:=c}) ({x:=x}) ->
+  ------------------------------------------------------------
+  Typed C' Γ (Term.fapp x c y) ((E.copen c).open y)
+| letin :
+  Typed C1 Γ t (EType.type T) ->
+  Typed C2.weaken (Γ,x:T) u E0 ->
+  ((Γ,x:T) ⊢e E0 <: E.weaken) ->
+  Chaining Γ C1 C2 ->
+  ------------------------------------------------------------
+  Typed (C1 ∪ C2) Γ (Term.letin t u) E
+| unpack :
+  Typed C1 Γ t (EType.ex T) ->
+  Typed (C2.cweaken.weaken ∪ CaptureSet.span 0) ((Γ,c:cparam CKind.Fresh),x:T) u E0 ->
+  (((Γ,c:cparam CKind.Fresh),x:T) ⊢e E0 <: E.cweaken.weaken) ->
+  Chaining Γ C1 C2 ->
+  ------------------------------------------------------------
+  Typed (C1 ∪ C2) Γ (Term.unpack t u) E
+
+end Capybara
diff --git a/Capybara/Syntax.lean b/Capybara/Syntax.lean
new file mode 100644
index 00000000..d234b8b0
--- /dev/null
+++ b/Capybara/Syntax.lean
@@ -0,0 +1,5 @@
+import Capybara.Syntax.Mode
+import Capybara.Syntax.CaptureSet
+import Capybara.Syntax.Type
+import Capybara.Syntax.Term
+import Capybara.Syntax.Context
diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean
new file mode 100644
index 00000000..8dedb7ca
--- /dev/null
+++ b/Capybara/Syntax/CaptureSet.lean
@@ -0,0 +1,2 @@
+import Capybara.Syntax.CaptureSet.Core
+import Capybara.Syntax.CaptureSet.Properties
diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean
new file mode 100644
index 00000000..c367787a
--- /dev/null
+++ b/Capybara/Syntax/CaptureSet/Core.lean
@@ -0,0 +1,113 @@
+import Capybara.Syntax.Mode
+import Capybara.Morphism.Core
+namespace Capybara
+
+/-!
+Capture set definitions.
+-/
+inductive CaptureSet : Nat -> Nat -> Type where
+| empty : CaptureSet n k
+| union : CaptureSet n k -> CaptureSet n k -> CaptureSet n k
+| singleton : Fin n -> Mode -> CaptureSet n k
+| csingleton : Fin k -> Mode -> CaptureSet n k
+
+/-!
+Instance definitions for capture sets.
+-/
+@[simp]
+instance : EmptyCollection (CaptureSet n k) where
+  emptyCollection := CaptureSet.empty
+
+@[simp]
+instance : Union (CaptureSet n k) where
+  union := CaptureSet.union
+
+/-!
+Notation for capture sets.
+-/
+notation:40 "{x@" m ":=" x "}" => CaptureSet.singleton x m
+notation:40 "{x:=" x "}" => {x@ε:=x}
+notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m
+notation:40 "{c:=" x "}" => {c@ε:=x}
+
+/-!
+Renaming functions for capture sets.
+-/
+def CaptureSet.rename
+  (C : CaptureSet n k)
+  (ρ : CaptureRenaming n k n' k') :
+  CaptureSet n' k' :=
+  match C with
+  | empty => {}
+  | union C1 C2 => (C1.rename ρ) ∪ (C2.rename ρ)
+  | singleton x m => {x@m:=ρ.var x}
+  | csingleton x m => {c@m:=ρ.cvar x}
+
+/-!
+Mode qualification.
+-/
+def CaptureSet.qualified
+  (C : CaptureSet n k)
+  (m : Mode) :
+  CaptureSet n k :=
+  match C, m with
+  | empty, _ => {}
+  | union C1 C2, m => (C1.qualified m) ∪ (C2.qualified m)
+  | singleton x m0, ε => singleton x m0
+  | singleton x _, m => singleton x m
+  | csingleton x m0, ε => csingleton x m0
+  | csingleton x _, m => csingleton x m
+
+def CaptureSet.ro (C : CaptureSet n k) : CaptureSet n k :=
+  C.qualified ro
+
+/-!
+Weakening functions for capture sets.
+-/
+def CaptureSet.weaken : CaptureSet n k -> CaptureSet (n+1) k :=
+  fun C => C.rename (Renaming.weaken (m:=0)).asCapt
+def CaptureSet.cweaken : CaptureSet n k -> CaptureSet n (k+1) :=
+  fun C => C.rename (Renaming.cweaken (m:=0)).asCapt
+
+/-!
+Basic theorems.
+-/
+theorem CaptureSet.empty_def :
+  ({} : CaptureSet n k) = CaptureSet.empty := rfl
+
+theorem CaptureSet.union_def (C1 C2 : CaptureSet n k) :
+  (C1 ∪ C2) = CaptureSet.union C1 C2 := rfl
+
+@[simp]
+theorem CaptureSet.qualified_default {C : CaptureSet n k} :
+  C.qualified ε = C := by
+  induction C <;> simp [CaptureSet.qualified, CaptureSet.empty_def]
+  case union ih1 ih2 => simp [CaptureSet.union_def, ih1, ih2]
+
+/-!
+Subset relation for capture sets. It is defined inductively.
+-/
+inductive CaptureSet.Subset : CaptureSet n k -> CaptureSet n k -> Prop where
+| empty : CaptureSet.Subset {} C
+| refl : CaptureSet.Subset C C
+| union_l :
+  CaptureSet.Subset C1 C ->
+  CaptureSet.Subset C2 C ->
+  CaptureSet.Subset (C1 ∪ C2) C
+| union_rl :
+  CaptureSet.Subset C C1 ->
+  CaptureSet.Subset C (C1 ∪ C2)
+| union_rr :
+  CaptureSet.Subset C C2 ->
+  CaptureSet.Subset C (C1 ∪ C2)
+
+instance : HasSubset (CaptureSet n k) where
+  Subset := CaptureSet.Subset
+
+/-!
+Spanning a capture set over a variable.
+-/
+def CaptureSet.span (x : Fin n) : CaptureSet n k :=
+  ({x:=x}) ∪ ({x@ro:=x}) ∪ ({x@drop:=x})
+
+end Capybara
diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean
new file mode 100644
index 00000000..4998ed09
--- /dev/null
+++ b/Capybara/Syntax/CaptureSet/Properties.lean
@@ -0,0 +1,66 @@
+import Capybara.Syntax.CaptureSet.Core
+namespace Capybara
+
+/-!
+# Properties of capture sets
+
+## Renaming identity
+We can show that renaming by the identity renaming yields the same capture set.
+-/
+@[simp]
+theorem CaptureSet.rename_id {C : CaptureSet n k} : C.rename (Renaming.id (m:=m).asCapt) = C := by
+  induction C <;> simp [CaptureSet.rename]
+  case union ih1 ih2 => simp [ih1, ih2]
+  case singleton => simp [Renaming.id, Renaming.asCapt, FinFun.id]
+  case csingleton => simp [Renaming.id, Renaming.asCapt, FinFun.id]
+
+/-!
+## Composition of renamings
+In the following, we show that renaming composes.
+-/
+theorem CaptureSet.rename_comp {ρ : CaptureRenaming n k n' k'} {ρ' : CaptureRenaming n' k' n'' k''} {C : CaptureSet n k} :
+  (C.rename ρ).rename ρ' = C.rename (ρ.comp ρ') := by
+  induction C <;> simp [CaptureSet.rename]
+  case union ih1 ih2 => simp [ih1, ih2]
+  case singleton => simp [CaptureRenaming.comp, FinFun.comp]
+  case csingleton => simp [CaptureRenaming.comp, FinFun.comp]
+
+theorem CaptureSet.rename_weaken {C : CaptureSet n k} {ρ : Renaming n m k n' m' k'} :
+  (C.rename ρ.asCapt).weaken = C.weaken.rename ρ.ext.asCapt := by
+  simp [CaptureSet.weaken]
+  simp [CaptureSet.rename_comp]
+  rw [Renaming.weaken_transportM (m1:=0) (m2:=m')]
+  rw [<-Renaming.comp_asCapt]
+  rw [Renaming.weaken_transportM (m1:=0) (m2:=m)]
+  rw [<-Renaming.comp_asCapt]
+  simp [Renaming.comp_weaken]
+
+theorem CaptureSet.rename_cweaken {C : CaptureSet n k} {ρ : Renaming n m k n' m' k'} :
+  (C.rename ρ.asCapt).cweaken = C.cweaken.rename ρ.cext.asCapt := by
+  simp [CaptureSet.cweaken, CaptureSet.rename_comp]
+  rw [Renaming.cweaken_transportM (m1:=0) (m2:=m')]
+  rw [<-Renaming.comp_asCapt]
+  rw [Renaming.cweaken_transportM (m1:=0) (m2:=m)]
+  rw [<-Renaming.comp_asCapt]
+  simp [Renaming.comp_cweaken]
+
+theorem CaptureSet.rename_subset {C1 C2 : CaptureSet n k} {ρ : CaptureRenaming n k n' k'} (hs : C1 ⊆ C2) :
+  (C1.rename ρ) ⊆ (C2.rename ρ) := by
+  induction hs <;> try simp [CaptureSet.rename] <;> try (solve | constructor)
+  case refl => apply Subset.refl
+  case union_l ih1 ih2 => constructor <;> aesop
+  case union_rl => apply Subset.union_rl; aesop
+  case union_rr => apply Subset.union_rr; aesop
+
+theorem CaptureSet.qualified_rename {C : CaptureSet n k} :
+  (C.qualified m).rename ρ = (C.rename ρ).qualified m := by
+  induction C <;> simp [CaptureSet.qualified, CaptureSet.rename]
+  case union ih1 ih2 => simp [ih1, ih2]
+  case singleton =>
+    cases m <;> try simp [CaptureSet.qualified, CaptureSet.rename]
+    case M mu => cases mu <;> simp [CaptureSet.qualified, CaptureSet.rename]
+  case csingleton =>
+    cases m <;> try simp [CaptureSet.qualified, CaptureSet.rename]
+    case M mu => cases mu <;> simp [CaptureSet.qualified, CaptureSet.rename]
+
+end Capybara
diff --git a/Capybara/Syntax/Context.lean b/Capybara/Syntax/Context.lean
new file mode 100644
index 00000000..085eccf9
--- /dev/null
+++ b/Capybara/Syntax/Context.lean
@@ -0,0 +1,2 @@
+import Capybara.Syntax.Context.Core
+import Capybara.Syntax.Context.Properties
diff --git a/Capybara/Syntax/Context/Core.lean b/Capybara/Syntax/Context/Core.lean
new file mode 100644
index 00000000..e3d3c488
--- /dev/null
+++ b/Capybara/Syntax/Context/Core.lean
@@ -0,0 +1,123 @@
+import Mathlib.Data.Fin.Basic
+import Capybara.Syntax.Type
+namespace Capybara
+
+/-!
+Kind of a capture set parameter.
+-/
+inductive CKind : Nat -> Nat -> Type where
+| Sep : SepDegree n k -> CKind n k
+| Fresh : CKind n k
+
+/-!
+Type binding and capture set binding.
+
+Type binding can be either a type parameter (abstract) or
+a concrete type alias. Similarly, capture set binding can be
+a capture set parameter (abstract) or a concrete capture set alias.
+-/
+inductive TBinding : Nat -> Nat -> Nat -> Type where
+| param : SType n m k -> TBinding n m k
+| typealias : SType n m k -> TBinding n m k
+
+inductive CBinding : Nat -> Nat -> Type where
+| param : CKind n k -> CBinding n k
+| capturealias : CaptureSet n k -> CBinding n k
+
+notation:max "tparam" S => TBinding.param S
+notation:max "talias" S => TBinding.typealias S
+notation:max "cparam" k => CBinding.param k
+notation:max "calias" C => CBinding.capturealias C
+
+/-!
+Renaming functions for type and capture set binding.
+-/
+def CKind.rename : CKind n k -> CaptureRenaming n k n' k' -> CKind n' k'
+| CKind.Sep D, ρ => CKind.Sep (D.rename ρ)
+| CKind.Fresh, _ => CKind.Fresh
+def TBinding.rename : TBinding n m k -> Renaming n m k n' m' k' -> TBinding n' m' k'
+| TBinding.param T, ρ => TBinding.param (T.rename ρ)
+| TBinding.typealias T, ρ => TBinding.typealias (T.rename ρ)
+def CBinding.rename : CBinding n k -> CaptureRenaming n k n' k' -> CBinding n' k'
+| CBinding.param k, ρ => CBinding.param (k.rename ρ)
+| CBinding.capturealias C, ρ => CBinding.capturealias (C.rename ρ)
+
+/-!
+Weakening functions for type and capture set binding.
+-/
+def TBinding.weaken (B : TBinding n m k) : TBinding (n+1) m k :=
+  B.rename (Renaming.weaken)
+def CKind.weaken (K : CKind n k) : CKind (n+1) k :=
+  K.rename (Renaming.weaken (m:=0)).asCapt
+def CBinding.weaken (B : CBinding n k) : CBinding (n+1) k :=
+  B.rename (Renaming.weaken (m:=0)).asCapt
+def TBinding.tweaken (B : TBinding n m k) : TBinding n (m+1) k :=
+  B.rename (Renaming.tweaken)
+def TBinding.cweaken (B : TBinding n m k) : TBinding n m (k+1) :=
+  B.rename (Renaming.cweaken)
+def CKind.cweaken (K : CKind n k) : CKind n (k+1) :=
+  K.rename (Renaming.cweaken (m:=0)).asCapt
+def CBinding.cweaken (B : CBinding n k) : CBinding n (k+1) :=
+  B.rename (Renaming.cweaken (m:=0)).asCapt
+
+/-!
+An indexed context. A `Context n m k` contains `n` term variables,
+`m` type variables, and `k` capture set variables.
+!-/
+inductive Context : Nat -> Nat -> Nat -> Type where
+| empty : Context 0 0 0
+| cons : Context n m k -> CType n m k -> Context (n+1) m k
+| tcons : Context n m k -> TBinding n m k -> Context n (m+1) k
+| ccons : Context n m k -> CBinding n k -> Context n m (k+1)
+
+instance : EmptyCollection (Context 0 0 0) :=
+  ⟨Context.empty⟩
+
+theorem Context.empty_def :
+  ({} : Context 0 0 0) = Context.empty := rfl
+
+notation:20 Γ ",x:" T => Context.cons Γ T
+notation:20 Γ ",X:" T => Context.tcons Γ T
+notation:20 Γ ",c:" C => Context.ccons Γ C
+
+/-!
+Context lookup.
+
+`Context.Lookup`, `Context.LookupT`, and `Context.LookupC` look up the three dimensions of a context,
+respectively.
+-/
+inductive Context.Lookup : Context n m k -> Fin n -> CType n m k -> Prop where
+| here : Context.Lookup (Γ,x:T) 0 T.weaken
+| there :
+  Context.Lookup Γ x T ->
+  Context.Lookup (Γ,x:T) (x.succ) T.weaken
+| tthere :
+  Context.Lookup Γ x T ->
+  Context.Lookup (Γ,X:B) x (T.tweaken)
+| cthere :
+  Context.Lookup Γ x T ->
+  Context.Lookup (Γ,c:B) x (T.cweaken)
+inductive Context.LookupT : Context n m k -> Fin m -> TBinding n m k -> Prop where
+| here : Context.LookupT (Γ,X:T) 0 T.tweaken
+| there :
+  Context.LookupT Γ X S ->
+  Context.LookupT (Γ,x:T) X S.weaken
+| tthere :
+  Context.LookupT Γ X T ->
+  Context.LookupT (Γ,X:B) (X.succ) T.tweaken
+| cthere :
+  Context.LookupT Γ X T ->
+  Context.LookupT (Γ,c:B) X T.cweaken
+inductive Context.LookupC : Context n m k -> Fin k -> CBinding n k -> Prop where
+| here : Context.LookupC (Γ,c:C) 0 C.cweaken
+| there :
+  Context.LookupC Γ c C ->
+  Context.LookupC (Γ,x:T) c C.weaken
+| tthere :
+  Context.LookupC Γ c C ->
+  Context.LookupC (Γ,X:B) c C
+| cthere :
+  Context.LookupC Γ c C ->
+  Context.LookupC (Γ,c:B) (c.succ) C.cweaken
+
+end Capybara
diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean
new file mode 100644
index 00000000..d25094dd
--- /dev/null
+++ b/Capybara/Syntax/Context/Properties.lean
@@ -0,0 +1,74 @@
+import Capybara.Syntax.Context.Core
+namespace Capybara
+
+theorem TBinding.rename_id {B : TBinding n m k} : B.rename Renaming.id = B := by
+  cases B
+  case param => simp [TBinding.rename, SType.rename_id]
+  case typealias => simp [TBinding.rename, SType.rename_id]
+
+theorem TBinding.rename_weaken {B : TBinding n m k} :
+  (B.rename ρ).weaken = B.weaken.rename ρ.ext := by
+  cases B
+  case param =>
+    simp [TBinding.weaken, TBinding.rename]
+    apply SType.rename_weaken
+  case typealias =>
+    simp [TBinding.weaken, TBinding.rename]
+    apply SType.rename_weaken
+
+theorem TBinding.rename_tweaken {B : TBinding n m k} :
+  (B.rename ρ).tweaken = B.tweaken.rename ρ.text := by
+  cases B
+  case param =>
+    simp [TBinding.tweaken, TBinding.rename]
+    apply SType.rename_tweaken
+  case typealias =>
+    simp [TBinding.tweaken, TBinding.rename]
+    apply SType.rename_tweaken
+
+theorem TBinding.rename_cweaken {B : TBinding n m k} :
+  (B.rename ρ).cweaken = B.cweaken.rename ρ.cext := by
+  cases B
+  case param =>
+    simp [TBinding.cweaken, TBinding.rename]
+    apply SType.rename_cweaken
+  case typealias =>
+    simp [TBinding.cweaken, TBinding.rename]
+    apply SType.rename_cweaken
+
+theorem CBinding.rename_weaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} :
+  (B.rename ρ.asCapt).weaken = B.weaken.rename ρ.ext.asCapt := by
+  cases B
+  case param K =>
+    simp [CBinding.weaken, CBinding.rename]
+    cases K
+    case Sep D =>
+      cases D; simp [CKind.rename]; simp [SepDegree.rename]
+      apply CaptureSet.rename_weaken
+    case Fresh =>
+      simp [CKind.rename]
+  case capturealias C =>
+    simp [CBinding.weaken, CBinding.rename]
+    simp [CaptureSet.rename_comp]
+    rw [Renaming.weaken_transportM (m1:=0) (m2:=m')]
+    rw [<-Renaming.comp_asCapt]
+    rw [Renaming.weaken_transportM (m1:=0) (m2:=m)]
+    rw [<-Renaming.comp_asCapt]
+    simp [Renaming.comp_weaken]
+
+theorem CBinding.rename_cweaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} :
+  (B.rename ρ.asCapt).cweaken = B.cweaken.rename ρ.cext.asCapt := by
+  cases B
+  case param K =>
+    simp [CBinding.cweaken, CBinding.rename]
+    cases K
+    case Sep D =>
+      cases D; simp [CKind.rename]; simp [SepDegree.rename]
+      apply CaptureSet.rename_cweaken
+    case Fresh =>
+      simp [CKind.rename]
+  case capturealias C =>
+    simp [CBinding.cweaken]; simp [CBinding.rename]
+    apply CaptureSet.rename_cweaken
+
+end Capybara
diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean
new file mode 100644
index 00000000..60006ab8
--- /dev/null
+++ b/Capybara/Syntax/Mode.lean
@@ -0,0 +1,28 @@
+namespace Capybara
+
+inductive Mutability : Type where
+| readonly : Mutability
+| default : Mutability
+
+inductive Mode : Type where
+| M : Mutability -> Mode
+| drop : Mode
+
+notation "ro" => Mode.M Mutability.readonly
+notation "ε" => Mode.M Mutability.default
+notation "ε" => Mutability.default
+notation "drop" => Mode.drop
+
+/-!
+Given `m1` and `m2`, `LessPermissive m1 m2` means that `m1` is less permissive than `m2`.
+-/
+inductive Mutability.LessPermissive : Mutability -> Mutability -> Prop where
+| readonly : LessPermissive Mutability.readonly Mutability.default
+| refl : LessPermissive m m
+
+inductive Mode.LessPermissive : Mode -> Mode -> Prop where
+| M : Mutability.LessPermissive m1 m2 -> LessPermissive (Mode.M m1) (Mode.M m2)
+| drop : LessPermissive m Mode.drop
+| refl : LessPermissive m m
+
+end Capybara
diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean
new file mode 100644
index 00000000..df20f325
--- /dev/null
+++ b/Capybara/Syntax/Term.lean
@@ -0,0 +1,78 @@
+import Capybara.Syntax.Type
+namespace Capybara
+/-!
+# Term Syntax
+
+This module defines the syntax of terms in the Capybara language.
+
+## Main Definitions
+
+- `Term n m k`: Terms with `n` term variables, `m` type variables, and `k` capture set variables
+- `Term.rename`: Renaming operation for terms
+
+## Term Constructors
+
+- Variables: `var`
+- Functions: `lam` (term abstraction), `tlam` (type abstraction), `clam` (capture abstraction), `flam` (fresh capture abstraction)
+- Applications: `app` (term application), `tapp` (type application), `capp` (capture set application)
+- Capture set operations: `pack` (capture set creation), `unpack` (capture set elimination)
+- Let bindings: `letin` (term binding)
+- Aliases: `calias` (capture set alias), `talias` (type alias)
+
+The indices `n`, `m`, and `k` track the number of term variables, type variables, and capture set variables
+in scope, respectively. This ensures well-scopedness of terms through the type system.
+-/
+
+/-!
+Term definitions.
+-/
+inductive Term : Nat -> Nat -> Nat -> Type where
+| var : Fin n -> Term n m k
+| lam : CType n m k -> Term (n+1) m k -> Term n m k
+| tlam : SType n m k -> Term n (m+1) k -> Term n m k
+| clam : SepDegree n k -> Term n m (k+1) -> Term n m k
+| flam : CType n m (k+1) -> Term (n+1) m (k+1) -> Term n m k
+| pack : Fin k -> Fin n -> Term n m k
+| app : Fin n -> Fin n -> Term n m k
+| tapp : Fin n -> Fin m -> Term n m k
+| capp : Fin n -> Fin k -> Term n m k
+| fapp : Fin n -> Fin k -> Fin n -> Term n m k
+| letin : Term n m k -> Term (n+1) m k -> Term n m k
+| unpack : Term n m k -> Term (n+1) m (k+1) -> Term n m k
+| calias : CaptureSet n k -> Term n m (k+1) -> Term n m k
+| talias : SType n m k -> Term n (m+1) k -> Term n m k
+
+/-!
+Renaming operation for terms.
+-/
+def Term.rename
+  (t : Term n m k)
+  (ρ : Renaming n m k n' m' k') :
+  Term n' m' k' :=
+  match t with
+  | var x => var (ρ.var x)
+  | lam t1 t2 => lam (t1.rename ρ) (t2.rename ρ.ext)
+  | tlam t1 t2 => tlam (t1.rename ρ) (t2.rename ρ.text)
+  | clam D t => clam (D.rename ρ.asCapt) (t.rename ρ.cext)
+  | flam T t => flam (T.rename ρ.cext) (t.rename ρ.cext.ext)
+  | pack x y => pack (ρ.cvar x) (ρ.var y)
+  | app x y => app (ρ.var x) (ρ.var y)
+  | tapp x X => tapp (ρ.var x) (ρ.tvar X)
+  | capp x c => capp (ρ.var x) (ρ.cvar c)
+  | fapp x c y => fapp (ρ.var x) (ρ.cvar c) (ρ.var y)
+  | letin t1 t2 => letin (t1.rename ρ) (t2.rename ρ.ext)
+  | unpack t1 t2 => unpack (t1.rename ρ) (t2.rename ρ.cext.ext)
+  | calias C t => calias (C.rename ρ.asCapt) (t.rename ρ.cext)
+  | talias T t => talias (T.rename ρ) (t.rename ρ.text)
+
+/-!
+Weakening operation for terms.
+-/
+def Term.weaken : Term n m k -> Term (n+1) m k :=
+  fun t => t.rename Renaming.weaken
+def Term.tweaken : Term n m k -> Term n (m+1) k :=
+  fun t => t.rename Renaming.tweaken
+def Term.cweaken : Term n m k -> Term n m (k+1) :=
+  fun t => t.rename Renaming.cweaken
+
+end Capybara
diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean
new file mode 100644
index 00000000..3383628f
--- /dev/null
+++ b/Capybara/Syntax/Type.lean
@@ -0,0 +1,5 @@
+import Capybara.Syntax.Type.Core
+import Capybara.Syntax.Type.Renaming
+import Capybara.Syntax.Type.Weakening
+import Capybara.Syntax.Type.Opening
+import Capybara.Syntax.Type.Properties
diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean
new file mode 100644
index 00000000..aad5b764
--- /dev/null
+++ b/Capybara/Syntax/Type/Core.lean
@@ -0,0 +1,45 @@
+import Capybara.Syntax.CaptureSet.Core
+namespace Capybara
+
+inductive SepMode : Type where
+| Mut : SepMode
+| Imm : SepMode
+
+/-!
+Separation degree.
+-/
+structure SepDegree (n k : Nat) : Type where
+  mode : SepMode
+  degree : CaptureSet n k
+
+mutual
+
+inductive EType : Nat -> Nat -> Nat -> Type where
+| type : CType n m k -> EType n m k
+| ex   : CType n m (k+1) -> EType n m k
+
+inductive CType : Nat -> Nat -> Nat -> Type where
+| capt : CaptureSet n k -> Mutability -> SType n m k -> CType n m k
+
+inductive SType : Nat -> Nat -> Nat -> Type where
+| top : SType n m k
+| tvar : Fin m -> SType n m k
+| tarrow : SType n m k -> EType n (m+1) k -> SType n m k
+| arrow : CType n m k -> EType (n+1) m k -> SType n m k
+| carrow : SepDegree n k -> EType n m (k+1) -> SType n m k
+| farrow : CType n m (k+1) -> EType (n+1) m (k+1) -> SType n m k
+
+end
+
+/-!
+Notation for types.
+-/
+notation:max "⊤" => SType.top
+notation:40 "[X<:" S "]->" T => SType.tarrow S T
+notation:40 "(x:" S ")->" T => SType.arrow S T
+notation:40 "[c:" D "]->" T => SType.carrow D T
+notation:40 "[c:Fresh](x:" T ")->" E => SType.farrow T E
+notation:50 S "^[" m "]" C => CType.capt C m S
+notation:50 S "^" C => CType.capt C ε S
+
+end Capybara
diff --git a/Capybara/Syntax/Type/Opening.lean b/Capybara/Syntax/Type/Opening.lean
new file mode 100644
index 00000000..77707ebe
--- /dev/null
+++ b/Capybara/Syntax/Type/Opening.lean
@@ -0,0 +1,16 @@
+import Capybara.Syntax.Type.Renaming
+namespace Capybara
+
+def CType.copen (T : CType n m (k+1)) (c : Fin k) : CType n m k :=
+  T.rename (Renaming.copen c)
+
+def EType.open (T : EType (n+1) m k) (x : Fin n) : EType n m k :=
+  T.rename (Renaming.open x)
+
+def EType.topen (T : EType n (m+1) k) (X : Fin m) : EType n m k :=
+  T.rename (Renaming.topen X)
+
+def EType.copen (T : EType n m (k+1)) (c : Fin k) : EType n m k :=
+  T.rename (Renaming.copen c)
+
+end Capybara
diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean
new file mode 100644
index 00000000..656c5c15
--- /dev/null
+++ b/Capybara/Syntax/Type/Properties.lean
@@ -0,0 +1,137 @@
+import Capybara.Syntax.CaptureSet
+import Capybara.Syntax.Type.Renaming
+import Capybara.Syntax.Type.Weakening
+namespace Capybara
+
+
+/-!
+# Basic properties of type renamings
+
+## Renaming identity
+First, we show that renaming by the identity renaming yields the separation degree.
+-/
+theorem SepDegree.rename_id {D : SepDegree n k} : D.rename (Renaming.id (m:=m)).asCapt = D := by
+  cases D; simp [SepDegree.rename]
+
+/-!
+Then, we show that renaming by the identity renaming yields the type.
+-/
+mutual
+
+theorem EType.rename_id {E : EType n m k} : E.rename Renaming.id = E :=
+  match E with
+  | .ex T => by
+    simp [EType.rename]
+    simp [Renaming.id_cext]
+    simp [CType.rename_id]
+  | .type T => by
+    simp [EType.rename]
+    simp [CType.rename_id]
+
+theorem CType.rename_id {C : CType n m k} : C.rename Renaming.id = C :=
+  match C with
+  | .capt C' m S => by
+    simp [CType.rename]
+    simp [SType.rename_id]
+
+theorem SType.rename_id {S : SType n m k} : S.rename Renaming.id = S :=
+  match S with
+  | .top => rfl
+  | .tvar i => by
+    simp [SType.rename, Renaming.id]
+    rfl
+  | .tarrow S' T => by
+    simp [SType.rename]
+    simp [Renaming.id_text]
+    simp [SType.rename_id, EType.rename_id]
+  | .arrow C T => by
+    simp [SType.rename]
+    simp [Renaming.id_ext]
+    simp [CType.rename_id, EType.rename_id]
+  | .carrow D T => by
+    simp [SType.rename]
+    simp [Renaming.id_cext]
+    simp [EType.rename_id, SepDegree.rename_id]
+  | .farrow C T => by
+    simp [SType.rename]
+    simp [Renaming.id_cext, Renaming.id_ext]
+    simp [CType.rename_id, EType.rename_id]
+
+end
+
+/-!
+## Renaming composition
+-/
+theorem SepDegree.rename_comp {D : SepDegree n k} :
+  (D.rename ρ).rename ρ' = D.rename (ρ.comp ρ') := by
+  cases D; simp [SepDegree.rename, CaptureSet.rename_comp]
+
+mutual
+
+theorem EType.rename_comp {E : EType n m k} :
+  (E.rename ρ).rename ρ' = E.rename (ρ.comp ρ') :=
+  match E with
+  | .type T => by
+    simp [EType.rename]
+    simp [CType.rename_comp]
+  | .ex T => by
+    simp [EType.rename]
+    simp [CType.rename_comp, Renaming.comp_cext]
+
+theorem CType.rename_comp {C : CType n m k} :
+  (C.rename ρ).rename ρ' = C.rename (ρ.comp ρ') :=
+  match C with
+  | .capt m' C' S => by
+    simp [CType.rename, SType.rename_comp]
+    simp [CaptureSet.rename_comp, Renaming.comp_asCapt]
+
+theorem SType.rename_comp {S : SType n m k} :
+  (S.rename ρ).rename ρ' = S.rename (ρ.comp ρ') :=
+  match S with
+  | .top => by
+    simp [SType.rename]
+  | .tvar i => by
+    simp [SType.rename, Renaming.comp, FinFun.comp]
+  | .tarrow S' T => by
+    simp [SType.rename]
+    simp [SType.rename_comp, EType.rename_comp, Renaming.comp_text]
+  | .arrow C T => by
+    simp [SType.rename]
+    simp [CType.rename_comp, EType.rename_comp, Renaming.comp_ext]
+  | .carrow D T => by
+    simp [SType.rename]
+    simp [EType.rename_comp, SepDegree.rename_comp, Renaming.comp_cext, Renaming.comp_asCapt]
+  | .farrow C T => by
+    simp [SType.rename]
+    simp [CType.rename_comp, EType.rename_comp, Renaming.comp_cext, Renaming.comp_ext]
+
+end
+
+/-!
+## Corollaries of renaming composition
+-/
+theorem CType.rename_weaken {T : CType n m k} :
+  (T.rename ρ).weaken = T.weaken.rename ρ.ext := by
+  simp [CType.weaken, CType.rename_comp, Renaming.comp_weaken]
+
+theorem CType.rename_tweaken {T : CType n m k} :
+  (T.rename ρ).tweaken = T.tweaken.rename ρ.text := by
+  simp [CType.tweaken, CType.rename_comp, Renaming.comp_tweaken]
+
+theorem CType.rename_cweaken {T : CType n m k} :
+  (T.rename ρ).cweaken = T.cweaken.rename ρ.cext := by
+  simp [CType.cweaken, CType.rename_comp, Renaming.comp_cweaken]
+
+theorem SType.rename_weaken {S : SType n m k} :
+  (S.rename ρ).weaken = S.weaken.rename ρ.ext := by
+  simp [SType.weaken, SType.rename_comp, Renaming.comp_weaken]
+
+theorem SType.rename_tweaken {S : SType n m k} :
+  (S.rename ρ).tweaken = S.tweaken.rename ρ.text := by
+  simp [SType.tweaken, SType.rename_comp, Renaming.comp_tweaken]
+
+theorem SType.rename_cweaken {S : SType n m k} :
+  (S.rename ρ).cweaken = S.cweaken.rename ρ.cext := by
+  simp [SType.cweaken, SType.rename_comp, Renaming.comp_cweaken]
+
+end Capybara
diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean
new file mode 100644
index 00000000..08d5bf98
--- /dev/null
+++ b/Capybara/Syntax/Type/Renaming.lean
@@ -0,0 +1,39 @@
+import Capybara.Syntax.Type.Core
+namespace Capybara
+
+def SepDegree.rename
+  (D : SepDegree n k)
+  (ρ : CaptureRenaming n k n' k') :
+  SepDegree n' k' :=
+  match D with
+  | ⟨s, C⟩ => ⟨s, C.rename ρ⟩
+
+mutual
+
+def EType.rename
+  (E : EType n m k)
+  (ρ : Renaming n m k n' m' k') :
+  EType n' m' k' :=
+  match E with
+  | EType.type T => EType.type (T.rename ρ)
+  | EType.ex T => EType.ex (T.rename ρ.cext)
+
+def CType.rename
+  (T : CType n m k)
+  (ρ : Renaming n m k n' m' k') :
+  CType n' m' k' :=
+  match T with
+  | CType.capt C m S => CType.capt (C.rename ρ.asCapt) m (S.rename ρ)
+
+def SType.rename (S : SType n m k) (ρ : Renaming n m k n' m' k') : SType n' m' k' :=
+  match S with
+  | SType.top => SType.top
+  | SType.tvar x => SType.tvar (ρ.tvar x)
+  | SType.arrow T E => (x:T.rename ρ)->(E.rename ρ.ext)
+  | SType.carrow D E => [c:D.rename ρ.asCapt]->(E.rename ρ.cext)
+  | SType.farrow T E => [c:Fresh](x:T.rename ρ.cext)->(E.rename ρ.cext.ext)
+  | SType.tarrow S T => [X<:S.rename ρ]->(T.rename ρ.text)
+
+end
+
+end Capybara
diff --git a/Capybara/Syntax/Type/Weakening.lean b/Capybara/Syntax/Type/Weakening.lean
new file mode 100644
index 00000000..9967f9cb
--- /dev/null
+++ b/Capybara/Syntax/Type/Weakening.lean
@@ -0,0 +1,38 @@
+import Capybara.Syntax.Type.Renaming
+namespace Capybara
+
+/-!
+Term weakening functions.
+-/
+def EType.weaken : EType n m k -> EType (n+1) m k :=
+  fun E => E.rename Renaming.weaken
+def CType.weaken : CType n m k -> CType (n+1) m k :=
+  fun T => T.rename Renaming.weaken
+def SType.weaken : SType n m k -> SType (n+1) m k :=
+  fun S => S.rename Renaming.weaken
+def SepDegree.weaken : SepDegree n k -> SepDegree (n+1) k
+| ⟨sm, C⟩ => ⟨sm, C.weaken⟩
+
+/-!
+Type weakening functions.
+-/
+def EType.tweaken : EType n m k -> EType n (m+1) k :=
+  fun E => E.rename Renaming.tweaken
+def CType.tweaken : CType n m k -> CType n (m+1) k :=
+  fun T => T.rename Renaming.tweaken
+def SType.tweaken : SType n m k -> SType n (m+1) k :=
+  fun S => S.rename Renaming.tweaken
+
+/-!
+Capture set weakening functions.
+-/
+def EType.cweaken : EType n m k -> EType n m (k+1) :=
+  fun E => E.rename Renaming.cweaken
+def CType.cweaken : CType n m k -> CType n m (k+1) :=
+  fun T => T.rename Renaming.cweaken
+def SType.cweaken : SType n m k -> SType n m (k+1) :=
+  fun S => S.rename Renaming.cweaken
+def SepDegree.cweaken : SepDegree n k -> SepDegree n (k+1)
+| ⟨sm, C⟩ => ⟨sm, C.cweaken⟩
+
+end Capybara
diff --git a/lakefile.lean b/lakefile.lean
index a307e98d..1aedd2aa 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 «Capybara» where