Define syntax and equivalence.

8 files changed, 741 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..a485625
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/_build
diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..03e3ccd
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,7 @@
+module Everything where
+
+import CBPV.Axiom
+import CBPV.Equality
+import CBPV.Family
+import CBPV.Term
+import CBPV.Type
diff --git a/cbpv.agda-lib b/cbpv.agda-lib
new file mode 100644
index 0000000..204d880
--- /dev/null
+++ b/cbpv.agda-lib
@@ -0,0 +1,4 @@
+name: cbpv
+depend: standard-library
+include: src
+flags: --without-K
diff --git a/src/CBPV/Axiom.agda b/src/CBPV/Axiom.agda
new file mode 100644
index 0000000..503b61d
--- /dev/null
+++ b/src/CBPV/Axiom.agda
@@ -0,0 +1,167 @@
+{-# OPTIONS --safe #-}
+
+module CBPV.Axiom where
+
+open import Data.List using (List; []; _∷_; [_]; map)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties using (∈-map⁺)
+open import Data.List.Relation.Unary.Any using () renaming (here to ↓_; there to ↑_)
+open import Data.List.Relation.Unary.All using (_∷_; tabulate) renaming ([] to •⟩)
+open import Data.Product using () renaming (_,_ to _⊩_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import CBPV.Family
+open import CBPV.Term
+open import CBPV.Type
+
+pattern _∶_ a b = a ∷ b
+
+pattern x₀ = var (↓ refl)
+pattern x₁ = var (↑ ↓ refl)
+pattern x₂ = var (↑ ↑ ↓ refl)
+pattern x₃ = var (↑ ↑ ↑ ↓ refl)
+pattern x₄ = var (↑ ↑ ↑ ↑ ↓ refl)
+pattern x₅ = var (↑ ↑ ↑ ↑ ↑ ↓ refl)
+
+pattern 𝔞⟨_ ε = mvar (↓ refl) ε
+pattern 𝔟⟨_ ε = mvar (↑ ↓ refl) ε
+pattern 𝔠⟨_ ε = mvar (↑ ↑ ↓ refl) ε
+pattern 𝔡⟨_ ε = mvar (↑ ↑ ↑ ↓ refl) ε
+
+pattern ◌ᵃ⟨_ ε = 𝔞⟨ ε
+pattern ◌ᵇ⟨_ ε = 𝔟⟨ ε
+pattern ◌ᶜ⟨_ ε = 𝔠⟨ ε
+pattern ◌ᵈ⟨_ ε = 𝔡⟨ ε
+
+infix 19 _⟩
+infix 18 𝔞⟨_ 𝔟⟨_ 𝔠⟨_ 𝔡⟨_ ◌ᵃ⟨_ ◌ᵇ⟨_ ◌ᶜ⟨_ ◌ᵈ⟨_
+infixr 18 ⟨_ _∶_
+
+pattern 𝔞 = 𝔞⟨ •⟩
+pattern 𝔟 = 𝔟⟨ •⟩
+pattern 𝔠 = 𝔠⟨ •⟩
+pattern 𝔡 = 𝔡⟨ •⟩
+pattern ◌ᵃ = ◌ᵃ⟨ •⟩
+pattern ◌ᵇ = ◌ᵇ⟨ •⟩
+pattern ◌ᶜ = ◌ᶜ⟨ •⟩
+pattern ◌ᵈ = ◌ᵈ⟨ •⟩
+
+pattern _⟩ a = a ∶ •⟩
+pattern ⟨_ as = as
+
+pattern []⊩_ C = [] ⊩ C
+pattern [_]⊩_ A C = (A ∷ []) ⊩ C
+pattern [_•_]⊩_ A A′ C = (A ∷ A′ ∷ []) ⊩ C
+
+private
+  variable
+    A A′ A′′ : ValType
+    B B′ : CompType
+
+infix 0 _⨾_▹⊢ᵛ_≋_ _⨾_▹⊢ᶜ_≋_
+
+data _⨾_▹⊢ᵛ_≋_ : ∀ Vs Cs {A} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᵛ A) 0ℓ
+data _⨾_▹⊢ᶜ_≋_ : ∀ Vs Cs {B} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᶜ B) 0ℓ
+
+data _⨾_▹⊢ᵛ_≋_ where
+  -- Structural
+  have : ([]⊩ A) ∷ ([ A ]⊩ A′) ∷ [] ⨾ [] ▹⊢ᵛ have 𝔞 be 𝔟⟨ x₀ ⟩ ≋ 𝔟⟨ 𝔞 ⟩
+  -- Beta
+  𝟙β : [ []⊩ A ] ⨾ [] ▹⊢ᵛ unpoint tt 𝔞 ≋ 𝔞
+  +β₁ :
+    ([]⊩ A) ∷ ([ A ]⊩ A′′) ∷ ([ A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
+      untag (inl 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩)
+    ≋
+      𝔟⟨ 𝔞 ⟩
+  +β₂ :
+    ([]⊩ A′) ∷ ([ A ]⊩ A′′) ∷ ([ A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
+      untag (inr 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩)
+    ≋
+      𝔠⟨ 𝔞 ⟩
+  ×β :
+    ([]⊩ A) ∷ ([]⊩ A′) ∷ ([ A • A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
+      unpair (𝔞 , 𝔟) (𝔠⟨ x₀ ∶ x₁ ⟩)
+    ≋
+      𝔠⟨ 𝔞 ∶ 𝔟 ⟩
+  ⟶β : ([]⊩ A) ∷ ([ A ]⊩ A′) ∷ [] ⨾ [] ▹⊢ᵛ 𝔞 ‵ ƛ 𝔟⟨ x₀ ⟩ ≋ 𝔟⟨ 𝔞 ⟩
+  -- Eta
+  Uη : [ []⊩ (U B) ] ⨾ [] ▹⊢ᵛ thunk (force 𝔞) ≋ 𝔞
+  𝟘η : ([]⊩ 𝟘) ∷ ([ 𝟘 ]⊩ A) ∷ [] ⨾ [] ▹⊢ᵛ absurd 𝔞 ≋ 𝔟⟨ 𝔞 ⟩
+  𝟙η : ([]⊩ 𝟙) ∷ ([ 𝟙 ]⊩ A) ∷ [] ⨾ [] ▹⊢ᵛ unpoint 𝔞 (𝔟⟨ tt ⟩) ≋ 𝔟⟨ 𝔞 ⟩
+  +η :
+    ([]⊩ (A + A′)) ∷ ([ A + A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
+      untag 𝔞 (𝔟⟨ inl x₀ ⟩) (𝔟⟨ inr x₀ ⟩)
+    ≋
+      𝔟⟨ 𝔞 ⟩
+  ×η :
+    ([]⊩ (A × A′)) ∷ ([ A × A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
+      unpair 𝔞 (𝔟⟨ (x₀ , x₁) ⟩)
+    ≋
+      𝔟⟨ 𝔞 ⟩
+  ⟶η : [ []⊩ (A ⟶ A′) ] ⨾ [] ▹⊢ᵛ ƛ (x₀ ‵ 𝔞) ≋ 𝔞
+
+data _⨾_▹⊢ᶜ_≋_ where
+  -- Structural
+  have : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ have 𝔞 be 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
+  -- Beta
+  Uβ : [] ⨾ [ []⊩ B ] ▹⊢ᶜ force (thunk 𝔞) ≋ 𝔞
+  𝟙β : [] ⨾ [ []⊩ B ] ▹⊢ᶜ unpoint tt 𝔞 ≋ 𝔞
+  +β₁ :
+    [ []⊩ A ] ⨾ ([ A ]⊩ B) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
+      untag (inl 𝔞) (𝔞⟨ x₀ ⟩) (𝔟⟨ x₀ ⟩)
+    ≋
+      𝔞⟨ 𝔞 ⟩
+  +β₂ :
+    [ []⊩ A′ ] ⨾ ([ A ]⊩ B) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
+      untag (inr 𝔞) (𝔞⟨ x₀ ⟩) (𝔟⟨ x₀ ⟩)
+    ≋
+      𝔟⟨ 𝔞 ⟩
+  ×β :
+    ([]⊩ A) ∷ ([]⊩ A′) ∷ [] ⨾ [ [ A • A′ ]⊩ B ] ▹⊢ᶜ
+      unpair (𝔞 , 𝔟) (𝔞⟨ x₀ ∶ x₁ ⟩)
+    ≋
+      𝔞⟨ 𝔞 ∶ 𝔟 ⟩
+  Fβ : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ return 𝔞 to 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
+  ×ᶜβ₁ : [] ⨾ ([]⊩ B) ∷ ([]⊩ B′) ∷ [] ▹⊢ᶜ π₁ (𝔞 , 𝔟) ≋ 𝔞
+  ×ᶜβ₂ : [] ⨾ ([]⊩ B) ∷ ([]⊩ B′) ∷ [] ▹⊢ᶜ π₂ (𝔞 , 𝔟) ≋ 𝔟
+  ⟶β : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ 𝔞 ‵ ƛ 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
+  -- Eta
+  𝟘η : [ []⊩ 𝟘 ] ⨾ [ [ 𝟘 ]⊩ B ] ▹⊢ᶜ absurd 𝔞 ≋ 𝔞⟨ 𝔞 ⟩
+  𝟙η : [ []⊩ 𝟙 ] ⨾ [ [ 𝟙 ]⊩ B ] ▹⊢ᶜ unpoint 𝔞 (𝔞⟨ tt ⟩) ≋ 𝔞⟨ 𝔞 ⟩
+  +η :
+    [ []⊩ (A + A′) ] ⨾ [ [ A + A′ ]⊩ B ] ▹⊢ᶜ
+      untag 𝔞 (𝔞⟨ inl x₀ ⟩) (𝔞⟨ inr x₀ ⟩)
+    ≋
+      𝔞⟨ 𝔞 ⟩
+  ×η :
+    [ []⊩ (A × A′) ] ⨾ [ [ A × A′ ]⊩ B ] ▹⊢ᶜ
+      unpair 𝔞 (𝔞⟨ (x₀ , x₁) ⟩)
+    ≋
+      𝔞⟨ 𝔞 ⟩
+  Fη : [] ⨾ [ []⊩ (F A) ] ▹⊢ᶜ 𝔞 to return x₀ ≋ 𝔞
+  𝟙ᶜη : [] ⨾ [ []⊩ 𝟙 ] ▹⊢ᶜ tt ≋ 𝔞
+  ×ᶜη : [] ⨾ [ []⊩ (B × B′) ] ▹⊢ᶜ π₁ 𝔞 , π₂ 𝔞 ≋ 𝔞
+  ⟶η : [] ⨾ [ []⊩ (A ⟶ B) ] ▹⊢ᶜ ƛ (x₀ ‵ 𝔞) ≋ 𝔞
+  -- Sequencing
+  to-to :
+    [] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (F A′)) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
+      (𝔞 to 𝔟⟨ x₀ ⟩) to 𝔠⟨ x₀ ⟩
+    ≋
+      𝔞 to (𝔟⟨ x₀ ⟩ to 𝔠⟨ x₀ ⟩)
+  to-π₁ :
+    [] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (B × B′)) ∷ [] ▹⊢ᶜ
+      π₁ (𝔞 to 𝔟⟨ x₀ ⟩)
+    ≋
+      𝔞 to π₁ (𝔟⟨ x₀ ⟩)
+  to-π₂ :
+    [] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (B × B′)) ∷ [] ▹⊢ᶜ
+      π₂ (𝔞 to 𝔟⟨ x₀ ⟩)
+    ≋
+      𝔞 to π₂ (𝔟⟨ x₀ ⟩)
+  to-‵ :
+    [ []⊩ A ] ⨾ ([]⊩ (F A′)) ∷ ([ A′ ]⊩ (A ⟶ B)) ∷ [] ▹⊢ᶜ
+      𝔞 ‵ (𝔞 to 𝔟⟨ x₀ ⟩)
+    ≋
+      𝔞 to 𝔞 ‵ 𝔟⟨ x₀ ⟩
diff --git a/src/CBPV/Equality.agda b/src/CBPV/Equality.agda
new file mode 100644
index 0000000..f6f58c8
--- /dev/null
+++ b/src/CBPV/Equality.agda
@@ -0,0 +1,174 @@
+{-# OPTIONS --safe #-}
+
+module CBPV.Equality where
+
+open import Data.List using (List; []; _∷_; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Unary.All using (All; _∷_; []; lookup)
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.Product using () renaming (_×_ to _×′_; _,_ to _,′_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; _⇒_; _=[_]⇒_; Reflexive; Symmetric; Transitive; Setoid)
+open import Relation.Binary.PropositionalEquality using (refl)
+import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+
+open import CBPV.Axiom
+open import CBPV.Family
+open import CBPV.Term
+open import CBPV.Type
+
+private
+  variable
+    Vs Vs′ : List (Context ×′ ValType)
+    Cs Cs′ : List (Context ×′ CompType)
+    Γ Δ : Context
+    A A′ : ValType
+    B B′ : CompType
+
+infix 0 _⨾_▹_⊢ᵛ_≈_ _⨾_▹_⊢ᶜ_≈_
+
+data _⨾_▹_⊢ᵛ_≈_ : ∀ Vs Cs Γ {A} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A) 0ℓ
+data _⨾_▹_⊢ᶜ_≈_ : ∀ Vs Cs Γ {B} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B) 0ℓ
+
+data _⨾_▹_⊢ᵛ_≈_ where
+  refl  : Reflexive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
+  sym   : Symmetric {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
+  trans : Transitive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
+  axiom : (_⨾_▹⊢ᵛ_≋_ Vs Cs {A}) ⇒ (Vs ⨾ Cs ▹ [] ⊢ᵛ_≈_)
+  ren   : (ρ : Γ ~[ I ]↝ᵛ Δ) → (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_) =[ renᵛ {A = A} ρ ]⇒ (Vs ⨾ Cs ▹ Δ ⊢ᵛ_≈_)
+  msub  :
+    {val₁ val₂ : ⌞ Vs ⌟ᵛ ⇒ᵛ δᵛ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᵛ_)}
+    {comp₁ comp₂ : ⌞ Cs ⌟ᶜ ⇒ᶜ δᶜ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᶜ_)}
+    {t u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} →
+    (∀ {A Δ} → (m : (Δ ,′ A) ∈ Vs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᵛ val₁ m ≈ val₂ m) →
+    (∀ {B Δ} → (m : (Δ ,′ B) ∈ Cs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᶜ comp₁ m ≈ comp₂ m) →
+    Vs ⨾ Cs ▹ Γ ⊢ᵛ t ≈ u →
+    Vs′ ⨾ Cs′ ▹ Γ ⊢ᵛ msubᵛ val₁ comp₁ t ≈ msubᵛ val₂ comp₂ u
+
+data _⨾_▹_⊢ᶜ_≈_ where
+  refl  : Reflexive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
+  sym   : Symmetric {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
+  trans : Transitive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
+  axiom : (_⨾_▹⊢ᶜ_≋_ Vs Cs {B}) ⇒ (Vs ⨾ Cs ▹ [] ⊢ᶜ_≈_)
+  ren   : (ρ : Γ ~[ I ]↝ᵛ Δ) → (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_) =[ renᶜ {B = B} ρ ]⇒ (Vs ⨾ Cs ▹ Δ ⊢ᶜ_≈_)
+  msub  :
+    {val₁ val₂ : ⌞ Vs ⌟ᵛ ⇒ᵛ δᵛ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᵛ_)}
+    {comp₁ comp₂ : ⌞ Cs ⌟ᶜ ⇒ᶜ δᶜ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᶜ_)}
+    {t u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} →
+    (∀ {A Δ} → (m : (Δ ,′ A) ∈ Vs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᵛ val₁ m ≈ val₂ m) →
+    (∀ {B Δ} → (m : (Δ ,′ B) ∈ Cs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᶜ comp₁ m ≈ comp₂ m) →
+    Vs ⨾ Cs ▹ Γ ⊢ᶜ t ≈ u →
+    Vs′ ⨾ Cs′ ▹ Γ ⊢ᶜ msubᶜ val₁ comp₁ t ≈ msubᶜ val₂ comp₂ u
+
+≈ᵛ-setoid :
+  (Vs : List (Context ×′ ValType)) (Cs : List (Context ×′ CompType)) (Γ : Context) (A : ValType) →
+  Setoid 0ℓ 0ℓ
+≈ᵛ-setoid Vs Cs Γ A = record
+  { Carrier = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A
+  ; _≈_ = Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_
+  ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
+  }
+
+≈ᶜ-setoid :
+  (Vs : List (Context ×′ ValType)) (Cs : List (Context ×′ CompType)) (Γ : Context) (B : CompType) →
+  Setoid 0ℓ 0ℓ
+≈ᶜ-setoid Vs Cs Γ B = record
+  { Carrier = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B
+  ; _≈_ = Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_
+  ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
+  }
+
+module ValReasoning {Vs} {Cs} {Γ} {A} = SetoidReasoning (≈ᵛ-setoid Vs Cs Γ A)
+module CompReasoning {Vs} {Cs} {Γ} {B} = SetoidReasoning (≈ᶜ-setoid Vs Cs Γ B)
+
+-- Congruence
+
+val-congᵛ :
+  (t : ⌞ (Δ ,′ A′) ∷ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A)
+  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A′} →
+  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᵛ s ≈ u →
+  Vs ⨾ Cs ▹ Γ ⊢ᵛ val-instᵛ s t ≈ val-instᵛ u t
+val-congᵛ t s≈u =
+  msub {t = t}
+    (λ
+      { (here refl) → s≈u
+      ; (there m)   → refl
+      })
+    (λ m → refl)
+    refl
+
+val-congᶜ :
+  (t : ⌞ (Δ ,′ A) ∷ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B)
+  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A} →
+  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᵛ s ≈ u →
+  Vs ⨾ Cs ▹ Γ ⊢ᶜ val-instᶜ s t ≈ val-instᶜ u t
+val-congᶜ t s≈u =
+  msub {t = t}
+    (λ
+      { (here refl) → s≈u
+      ; (there m)   → refl
+      })
+    (λ m → refl)
+    refl
+
+comp-congᵛ :
+  (t : ⌞ Vs ⌟ᵛ ⨾ ⌞ (Δ ,′ B) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A)
+  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B} →
+  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᶜ s ≈ u →
+  Vs ⨾ Cs ▹ Γ ⊢ᵛ comp-instᵛ s t ≈ comp-instᵛ u t
+comp-congᵛ t s≈u =
+  msub {t = t}
+    (λ m → refl)
+    (λ
+      { (here refl) → s≈u
+      ; (there m)   → refl
+      })
+    refl
+
+comp-congᶜ :
+  (t : ⌞ Vs ⌟ᵛ ⨾ ⌞ (Δ ,′ B′) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B)
+  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B′} →
+  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᶜ s ≈ u →
+  Vs ⨾ Cs ▹ Γ ⊢ᶜ comp-instᶜ s t ≈ comp-instᶜ u t
+comp-congᶜ t s≈u =
+  msub {t = t}
+    (λ m → refl)
+    (λ
+      { (here refl) → s≈u
+      ; (there m)   → refl
+      })
+    refl
+
+thmᵛ≈ :
+  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A}
+  (thm : Vs ⨾ Cs ▹ Γ ⊢ᵛ t ≈ s)
+  (ρ : All (I Δ) Γ)
+  (ζ : All (λ (Θ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᵛ A) Vs)
+  (ξ : All (λ (Θ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᶜ B) Cs) →
+  Vs′ ⨾ Cs′ ▹ Δ ⊢ᵛ msub′ᵛ ζ ξ (ren′ᵛ ρ t) ≈ msub′ᵛ ζ ξ (ren′ᵛ ρ s)
+thmᵛ≈ thm ρ ζ ξ = msub (λ _ → refl) (λ _ → refl) (ren (lookup ρ) thm)
+
+thmᶜ≈ :
+  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B}
+  (thm : Vs ⨾ Cs ▹ Γ ⊢ᶜ t ≈ s)
+  (ρ : All (I Δ) Γ)
+  (ζ : All (λ (Θ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᵛ A) Vs)
+  (ξ : All (λ (Θ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᶜ B) Cs) →
+  Vs′ ⨾ Cs′ ▹ Δ ⊢ᶜ msub′ᶜ ζ ξ (ren′ᶜ ρ t) ≈ msub′ᶜ ζ ξ (ren′ᶜ ρ s)
+thmᶜ≈ thm ρ ζ ξ = msub (λ _ → refl) (λ _ → refl) (ren (lookup ρ) thm)
+
+axᵛ≈ :
+  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᵛ A}
+  (ax : Vs ⨾ Cs ▹⊢ᵛ t ≋ s)
+  (ζ : All (λ (Δ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A) Vs)
+  (ξ : All (λ (Δ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B) Cs) →
+  Vs′ ⨾ Cs′ ▹ Γ ⊢ᵛ msub′ᵛ ζ ξ (ren′ᵛ [] t) ≈ msub′ᵛ ζ ξ (ren′ᵛ [] s)
+axᵛ≈ ax = thmᵛ≈ (axiom ax) []
+
+axᶜ≈ :
+  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᶜ B}
+  (ax : Vs ⨾ Cs ▹⊢ᶜ t ≋ s)
+  (ζ : All (λ (Δ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A) Vs)
+  (ξ : All (λ (Δ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B) Cs) →
+  Vs′ ⨾ Cs′ ▹ Γ ⊢ᶜ msub′ᶜ ζ ξ (ren′ᶜ [] t) ≈ msub′ᶜ ζ ξ (ren′ᶜ [] s)
+axᶜ≈ ax = thmᶜ≈ (axiom ax) []
diff --git a/src/CBPV/Family.agda b/src/CBPV/Family.agda
new file mode 100644
index 0000000..94fee5c
--- /dev/null
+++ b/src/CBPV/Family.agda
@@ -0,0 +1,52 @@
+{-# OPTIONS --safe #-}
+
+module CBPV.Family where
+
+open import Data.List using (List; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Product using (_,_) renaming (_×_ to _×′_)
+open import Level using (Level; suc; _⊔_)
+
+open import CBPV.Type
+
+private
+  variable
+    ℓ ℓ′ : Level
+
+Context : Set
+Context = List ValType
+
+ValFamily : (ℓ : Level) → Set (suc ℓ)
+ValFamily ℓ = Context → ValType → Set ℓ
+
+CompFamily : (ℓ : Level) → Set (suc ℓ)
+CompFamily ℓ = Context → CompType → Set ℓ
+
+δᵛ : Context → ValFamily ℓ → ValFamily ℓ
+δᵛ Δ V Γ A = V (Γ ++ Δ) A
+
+δᶜ : Context → CompFamily ℓ → CompFamily ℓ
+δᶜ Δ C Γ B = C (Γ ++ Δ) B
+
+infix 0 _⇒ᵛ_ _⇒ᶜ_ _~[_]↝ᵛ_ _~[_]↝ᶜ_
+
+_⇒ᵛ_ : ValFamily ℓ → ValFamily ℓ′ → Set (ℓ ⊔ ℓ′)
+V ⇒ᵛ V′ = ∀ {Γ A} → V Γ A → V′ Γ A
+
+_⇒ᶜ_ : CompFamily ℓ → CompFamily ℓ′ → Set (ℓ ⊔ ℓ′)
+C ⇒ᶜ C′ = ∀ {Γ B} → C Γ B → C′ Γ B
+
+_~[_]↝ᵛ_ : List ValType → ValFamily ℓ → Context → Set ℓ
+As ~[ V ]↝ᵛ Γ = ∀ {A} → A ∈ As → V Γ A
+
+_~[_]↝ᶜ_ : List CompType → CompFamily ℓ → Context → Set ℓ
+Bs ~[ C ]↝ᶜ Γ = ∀ {B} → B ∈ Bs → C Γ B
+
+I : ValFamily _
+I Γ A = A ∈ Γ
+
+⌞_⌟ᵛ : List (Context ×′ ValType) → ValFamily _
+⌞ Vs ⌟ᵛ Γ A = (Γ , A) ∈ Vs
+
+⌞_⌟ᶜ : List (Context ×′ CompType) → CompFamily _
+⌞ Cs ⌟ᶜ Γ B = (Γ , B) ∈ Cs
diff --git a/src/CBPV/Term.agda b/src/CBPV/Term.agda
new file mode 100644
index 0000000..ec05de4
--- /dev/null
+++ b/src/CBPV/Term.agda
@@ -0,0 +1,309 @@
+{-# OPTIONS --safe #-}
+
+module CBPV.Term where
+
+open import Data.List using (List; []; _∷_; [_]; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties using (∈-++⁻; ∈-++⁺ˡ; ∈-++⁺ʳ)
+open import Data.List.Relation.Unary.All using (All; []; _∷_; lookup; tabulate)
+open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to _++⁺_)
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.Product using () renaming (_×_ to _×′_; _,_ to _,′_)
+open import Data.Sum using ([_,_]′)
+open import Function.Base using (id; _∘_; _∘′_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import CBPV.Family
+open import CBPV.Type
+
+private
+  variable
+    Γ Δ : Context
+    A A′ A′′ : ValType
+    B B′ : CompType
+    As : List ValType
+
+infix 0 _⨾_▹_⊢ᵛ_ _⨾_▹_⊢ᶜ_
+infix 9 ƛ_
+infixr 8 _‵_
+infixr 2 _,_
+infixr 1 have_be_ _to_
+
+data _⨾_▹_⊢ᵛ_ {v c} (V : ValFamily v) (C : CompFamily c) (Γ : Context) : ValType → Set (v ⊔ c)
+data _⨾_▹_⊢ᶜ_ {v c} (V : ValFamily v) (C : CompFamily c) (Γ : Context) : CompType → Set (v ⊔ c)
+
+data _⨾_▹_⊢ᵛ_ V C Γ where
+  -- Initiality
+  mvar : V Δ A → All (V ⨾ C ▹ Γ ⊢ᵛ_) Δ → V ⨾ C ▹ Γ ⊢ᵛ A
+  var  : A ∈ Γ → V ⨾ C ▹ Γ ⊢ᵛ A
+  -- Structural
+  have_be_ : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ A ∷ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A′
+  -- Introductors
+  thunk : V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᵛ U B
+  tt    : V ⨾ C ▹ Γ ⊢ᵛ 𝟙
+  inl   : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A + A′
+  inr   : V ⨾ C ▹ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A + A′
+  _,_   : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A × A′
+  ƛ_    : V ⨾ C ▹ A ∷ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A ⟶ A′
+  -- Eliminators
+  absurd  : V ⨾ C ▹ Γ ⊢ᵛ 𝟘 → V ⨾ C ▹ Γ ⊢ᵛ A
+  unpoint : V ⨾ C ▹ Γ ⊢ᵛ 𝟙 → V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
+  untag   : V ⨾ C ▹ Γ ⊢ᵛ A + A′ → V ⨾ C ▹ A ∷ Γ ⊢ᵛ A′′ → V ⨾ C ▹ A′ ∷ Γ ⊢ᵛ A′′ → V ⨾ C ▹ Γ ⊢ᵛ A′′
+  unpair  : V ⨾ C ▹ Γ ⊢ᵛ A × A′ → V ⨾ C ▹ A ∷ A′ ∷ Γ ⊢ᵛ A′′ → V ⨾ C ▹ Γ ⊢ᵛ A′′
+  _‵_     : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A ⟶ A′ → V ⨾ C ▹ Γ ⊢ᵛ A′
+
+data _⨾_▹_⊢ᶜ_ V C Γ where
+  -- Initiality
+  mvar : C Δ B → All (V ⨾ C ▹ Γ ⊢ᵛ_) Δ → V ⨾ C ▹ Γ ⊢ᶜ B
+  -- Structural
+  have_be_ : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+  -- Introductors
+  return : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᶜ F A
+  tt     : V ⨾ C ▹ Γ ⊢ᶜ 𝟙
+  _,_    : V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B′ → V ⨾ C ▹ Γ ⊢ᶜ B × B′
+  ƛ_     : V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ A ⟶ B
+  -- Eliminators
+  force   : V ⨾ C ▹ Γ ⊢ᵛ U B → V ⨾ C ▹ Γ ⊢ᶜ B
+  absurd  : V ⨾ C ▹ Γ ⊢ᵛ 𝟘 → V ⨾ C ▹ Γ ⊢ᶜ B
+  unpoint : V ⨾ C ▹ Γ ⊢ᵛ 𝟙 → V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+  untag   : V ⨾ C ▹ Γ ⊢ᵛ A + A′ → V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ A′ ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+  unpair  : V ⨾ C ▹ Γ ⊢ᵛ A × A′ → V ⨾ C ▹ A ∷ A′ ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+  _to_    : V ⨾ C ▹ Γ ⊢ᶜ F A → V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+  π₁      : V ⨾ C ▹ Γ ⊢ᶜ B × B′ → V ⨾ C ▹ Γ ⊢ᶜ B
+  π₂      : V ⨾ C ▹ Γ ⊢ᶜ B × B′ → V ⨾ C ▹ Γ ⊢ᶜ B′
+  _‵_     : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᶜ A ⟶ B → V ⨾ C ▹ Γ ⊢ᶜ B
+
+private
+  variable
+    ℓ : Level
+    V V′ : ValFamily ℓ
+    C C′ : CompFamily ℓ
+    Vs : List (Context ×′ ValType)
+    Cs : List (Context ×′ CompType)
+
+lift :
+  (V : ValFamily ℓ) →
+  (∀ {A Γ Δ} → Γ ~[ I ]↝ᵛ Δ → V Γ A → V Δ A) →
+  I ⇒ᵛ V →
+  (Θ : Context) →
+  Γ ~[ V ]↝ᵛ Δ →
+  Θ ++ Γ ~[ V ]↝ᵛ Θ ++ Δ
+lift V ren new Θ σ = [ new ∘′ ∈-++⁺ˡ , ren (∈-++⁺ʳ Θ) ∘′ σ ]′ ∘′ ∈-++⁻ Θ
+
+liftI : (Θ : Context) → Γ ~[ I ]↝ᵛ Δ → Θ ++ Γ ~[ I ]↝ᵛ Θ ++ Δ
+liftI = lift I (λ f → f) id
+
+-- Renaming --------------------------------------------------------------------
+
+renᵛ : Δ ~[ I ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
+renᶜ : Δ ~[ I ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+renᵛ⋆ : Δ ~[ I ]↝ᵛ Γ → All (V ⨾ C ▹ Δ ⊢ᵛ_) As → All (V ⨾ C ▹ Γ ⊢ᵛ_) As
+
+renᵛ ρ (mvar m ts)  = mvar m (renᵛ⋆ ρ ts)
+renᵛ ρ (var i)      = var (ρ i)
+
+renᵛ ρ (have t be s) = have renᵛ ρ t be renᵛ (liftI [ _ ] ρ) s
+
+renᵛ ρ (thunk t) = thunk (renᶜ ρ t)
+renᵛ ρ tt        = tt
+renᵛ ρ (inl t)   = inl (renᵛ ρ t)
+renᵛ ρ (inr t)   = inr (renᵛ ρ t)
+renᵛ ρ (t , s)   = renᵛ ρ t , renᵛ ρ s
+renᵛ ρ (ƛ t)     = ƛ renᵛ (liftI [ _ ] ρ) t
+
+renᵛ ρ (absurd t)    = absurd (renᵛ ρ t)
+renᵛ ρ (unpoint t s) = unpoint (renᵛ ρ t) (renᵛ ρ s)
+renᵛ ρ (untag t s u) = untag (renᵛ ρ t) (renᵛ (liftI [ _ ] ρ) s) (renᵛ (liftI [ _ ] ρ) u)
+renᵛ ρ (unpair t s)  = unpair (renᵛ ρ t) (renᵛ (liftI (_ ∷ _ ∷ []) ρ) s)
+renᵛ ρ (t ‵ s)       = renᵛ ρ t ‵ renᵛ ρ s
+
+renᶜ ρ (mvar m ts) = mvar m (renᵛ⋆ ρ ts)
+
+renᶜ ρ (have t be s) = have renᵛ ρ t be renᶜ (liftI [ _ ] ρ) s
+
+renᶜ ρ (return t) = return (renᵛ ρ t)
+renᶜ ρ tt         = tt
+renᶜ ρ (t , s)    = renᶜ ρ t , renᶜ ρ s
+renᶜ ρ (ƛ t)      = ƛ renᶜ (liftI [ _ ] ρ) t
+
+renᶜ ρ (force t)     = force (renᵛ ρ t)
+renᶜ ρ (absurd t)    = absurd (renᵛ ρ t)
+renᶜ ρ (unpoint t s) = unpoint (renᵛ ρ t) (renᶜ ρ s)
+renᶜ ρ (untag t s u) = untag (renᵛ ρ t) (renᶜ (liftI [ _ ] ρ) s) (renᶜ (liftI [ _ ] ρ) u)
+renᶜ ρ (unpair t s)  = unpair (renᵛ ρ t) (renᶜ (liftI (_ ∷ _ ∷ []) ρ) s)
+renᶜ ρ (t to s)      = renᶜ ρ t to renᶜ (liftI [ _ ] ρ) s
+renᶜ ρ (π₁ t)        = π₁ (renᶜ ρ t)
+renᶜ ρ (π₂ t)        = π₂ (renᶜ ρ t)
+renᶜ ρ (t ‵ s)       = renᵛ ρ t ‵ renᶜ ρ s
+
+renᵛ⋆ ρ []       = []
+renᵛ⋆ ρ (t ∷ ts) = renᵛ ρ t ∷ renᵛ⋆ ρ ts
+
+-- Shorthand
+
+ren′ᵛ : All (I Δ) Γ → V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Δ ⊢ᵛ A
+ren′ᵛ ρ = renᵛ (lookup ρ)
+
+ren′ᶜ : All (I Δ) Γ → V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Δ ⊢ᶜ B
+ren′ᶜ ρ = renᶜ (lookup ρ)
+
+liftV : (Θ : Context) → Γ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Δ → Θ ++ Γ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Θ ++ Δ
+liftV = lift (_ ⨾ _ ▹_⊢ᵛ_) renᵛ var
+
+-- Substitution ----------------------------------------------------------------
+
+subᵛ : Δ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
+subᶜ : Δ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+subᵛ⋆ : Δ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Γ → All (V ⨾ C ▹ Δ ⊢ᵛ_) As → All (V ⨾ C ▹ Γ ⊢ᵛ_) As
+
+subᵛ σ (mvar m ts)  = mvar m (subᵛ⋆ σ ts)
+subᵛ σ (var i)      = σ i
+
+subᵛ σ (have t be s) = have subᵛ σ t be subᵛ (liftV [ _ ] σ) s
+
+subᵛ σ (thunk t) = thunk (subᶜ σ t)
+subᵛ σ tt        = tt
+subᵛ σ (inl t)   = inl (subᵛ σ t)
+subᵛ σ (inr t)   = inr (subᵛ σ t)
+subᵛ σ (t , s)   = subᵛ σ t , subᵛ σ s
+subᵛ σ (ƛ t)     = ƛ subᵛ (liftV [ _ ] σ) t
+
+subᵛ σ (absurd t)    = absurd (subᵛ σ t)
+subᵛ σ (unpoint t s) = unpoint (subᵛ σ t) (subᵛ σ s)
+subᵛ σ (untag t s u) = untag (subᵛ σ t) (subᵛ (liftV [ _ ] σ) s) (subᵛ (liftV [ _ ] σ) u)
+subᵛ σ (unpair t s)  = unpair (subᵛ σ t) (subᵛ (liftV (_ ∷ _ ∷ []) σ) s)
+subᵛ σ (t ‵ s)       = subᵛ σ t ‵ subᵛ σ s
+
+subᶜ σ (mvar m ts) = mvar m (subᵛ⋆ σ ts)
+
+subᶜ σ (have t be s) = have subᵛ σ t be subᶜ (liftV [ _ ] σ) s
+
+subᶜ σ (return t) = return (subᵛ σ t)
+subᶜ σ tt         = tt
+subᶜ σ (t , s)    = subᶜ σ t , subᶜ σ s
+subᶜ σ (ƛ t)      = ƛ subᶜ (liftV [ _ ] σ) t
+
+subᶜ σ (force t)     = force (subᵛ σ t)
+subᶜ σ (absurd t)    = absurd (subᵛ σ t)
+subᶜ σ (unpoint t s) = unpoint (subᵛ σ t) (subᶜ σ s)
+subᶜ σ (untag t s u) = untag (subᵛ σ t) (subᶜ (liftV [ _ ] σ) s) (subᶜ (liftV [ _ ] σ) u)
+subᶜ σ (unpair t s)  = unpair (subᵛ σ t) (subᶜ (liftV (_ ∷ _ ∷ []) σ) s)
+subᶜ σ (t to s)      = subᶜ σ t to subᶜ (liftV [ _ ] σ) s
+subᶜ σ (π₁ t)        = π₁ (subᶜ σ t)
+subᶜ σ (π₂ t)        = π₂ (subᶜ σ t)
+subᶜ σ (t ‵ s)       = subᵛ σ t ‵ subᶜ σ s
+
+subᵛ⋆ σ []       = []
+subᵛ⋆ σ (t ∷ ts) = subᵛ σ t ∷ subᵛ⋆ σ ts
+
+-- Shorthand
+
+sub′ᵛ : All (V ⨾ C ▹ Δ ⊢ᵛ_) Γ → V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Δ ⊢ᵛ A
+sub′ᵛ ρ = subᵛ (lookup ρ)
+
+sub′ᶜ : All (V ⨾ C ▹ Δ ⊢ᵛ_) Γ → V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Δ ⊢ᶜ B
+sub′ᶜ ρ = subᶜ (lookup ρ)
+
+-- Syntactic Substitution ------------------------------------------------------
+
+wknᵛ : (Θ : Context) → δᵛ Δ (V ⨾ C ▹_⊢ᵛ_) ⇒ᵛ δᵛ (Θ ++ Δ) (V ⨾ C ▹_⊢ᵛ_)
+wknᵛ {Δ} Θ {Γ} = renᵛ (liftI Γ (∈-++⁺ʳ Θ))
+
+wknᶜ : (Θ : Context) → δᶜ Δ (V ⨾ C ▹_⊢ᶜ_) ⇒ᶜ δᶜ (Θ ++ Δ) (V ⨾ C ▹_⊢ᶜ_)
+wknᶜ {Δ} Θ {Γ} = renᶜ (liftI Γ (∈-++⁺ʳ Θ))
+
+msubᵛ : V ⇒ᵛ δᵛ Γ (V′ ⨾ C′ ▹_⊢ᵛ_) → C ⇒ᶜ δᶜ Γ (V′ ⨾ C′ ▹_⊢ᶜ_) → V ⨾ C ▹ Γ ⊢ᵛ A → V′ ⨾ C′ ▹ Γ ⊢ᵛ A
+msubᶜ : V ⇒ᵛ δᵛ Γ (V′ ⨾ C′ ▹_⊢ᵛ_) → C ⇒ᶜ δᶜ Γ (V′ ⨾ C′ ▹_⊢ᶜ_) → V ⨾ C ▹ Γ ⊢ᶜ B → V′ ⨾ C′ ▹ Γ ⊢ᶜ B
+msubᵛ⋆ : V ⇒ᵛ δᵛ Γ (V′ ⨾ C′ ▹_⊢ᵛ_) → C ⇒ᶜ δᶜ Γ (V′ ⨾ C′ ▹_⊢ᶜ_) → All (V ⨾ C ▹ Γ ⊢ᵛ_) As → All (V′ ⨾ C′ ▹ Γ ⊢ᵛ_) As
+
+msubᵛ val comp (mvar m ts) = subᵛ (lookup (msubᵛ⋆ val comp ts ++⁺ tabulate var)) (val m)
+msubᵛ val comp (var i)     = var i
+
+msubᵛ val comp (have t be s) = have msubᵛ val comp t be msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s
+
+msubᵛ val comp (thunk t) = thunk (msubᶜ val comp t)
+msubᵛ val comp tt        = tt
+msubᵛ val comp (inl t)   = inl (msubᵛ val comp t)
+msubᵛ val comp (inr t)   = inr (msubᵛ val comp t)
+msubᵛ val comp (t , s)   = msubᵛ val comp t , msubᵛ val comp s
+msubᵛ val comp (ƛ t)     = ƛ msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) t
+
+msubᵛ val comp (absurd t)    = absurd (msubᵛ val comp t)
+msubᵛ val comp (unpoint t s) = unpoint (msubᵛ val comp t) (msubᵛ val comp s)
+msubᵛ val comp (untag t s u) = untag (msubᵛ val comp t) (msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s) (msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) u)
+msubᵛ val comp (unpair t s)  = unpair (msubᵛ val comp t) (msubᵛ (wknᵛ (_ ∷ _ ∷ []) ∘′ val) (wknᶜ (_ ∷ _ ∷ []) ∘′ comp) s)
+msubᵛ val comp (t ‵ s)       = msubᵛ val comp t ‵ msubᵛ val comp s
+
+msubᶜ val comp (mvar m ts) = subᶜ (lookup (msubᵛ⋆ val comp ts ++⁺ tabulate var)) (comp m)
+
+msubᶜ val comp (have t be s) = have msubᵛ val comp t be msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s
+
+msubᶜ val comp (return t) = return (msubᵛ val comp t)
+msubᶜ val comp tt         = tt
+msubᶜ val comp (t , s)    = msubᶜ val comp t , msubᶜ val comp s
+msubᶜ val comp (ƛ t)      = ƛ msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) t
+
+msubᶜ val comp (force t)     = force (msubᵛ val comp t)
+msubᶜ val comp (absurd t)    = absurd (msubᵛ val comp t)
+msubᶜ val comp (unpoint t s) = unpoint (msubᵛ val comp t) (msubᶜ val comp s)
+msubᶜ val comp (untag t s u) = untag (msubᵛ val comp t) (msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s) (msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) u)
+msubᶜ val comp (unpair t s)  = unpair (msubᵛ val comp t) (msubᶜ (wknᵛ (_ ∷ _ ∷ []) ∘′ val) (wknᶜ (_ ∷ _ ∷ []) ∘′ comp) s)
+msubᶜ val comp (t to s)      = msubᶜ val comp t to msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s
+msubᶜ val comp (π₁ t)        = π₁ (msubᶜ val comp t)
+msubᶜ val comp (π₂ t)        = π₂ (msubᶜ val comp t)
+msubᶜ val comp (t ‵ s)       = msubᵛ val comp t ‵ msubᶜ val comp s
+
+msubᵛ⋆ val comp []       = []
+msubᵛ⋆ val comp (t ∷ ts) = msubᵛ val comp t ∷ msubᵛ⋆ val comp ts
+
+-- Shorthand
+
+msub′ᵛ :
+  All (λ (Δ ,′ A) → V ⨾ C ▹ Δ ++ Γ ⊢ᵛ A) Vs →
+  All (λ (Δ ,′ B) → V ⨾ C ▹ Δ ++ Γ ⊢ᶜ B) Cs →
+  ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
+msub′ᵛ ζ ξ = msubᵛ (lookup ζ) (lookup ξ)
+
+msub′ᶜ :
+  All (λ (Δ ,′ A) → V ⨾ C ▹ Δ ++ Γ ⊢ᵛ A) Vs →
+  All (λ (Δ ,′ B) → V ⨾ C ▹ Δ ++ Γ ⊢ᶜ B) Cs →
+  ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
+msub′ᶜ ζ ξ = msubᶜ (lookup ζ) (lookup ξ)
+
+val-instᵛ : ⌞ Vs ⌟ᵛ ⨾ C ▹ Δ ++ Γ ⊢ᵛ A′ → ⌞ (Δ ,′ A′) ∷ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᵛ A → ⌞ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᵛ A
+val-instᵛ t =
+  msubᵛ
+    (λ
+      { (here refl) → t
+      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
+      })
+    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))
+
+val-instᶜ : ⌞ Vs ⌟ᵛ ⨾ C ▹ Δ ++ Γ ⊢ᵛ A → ⌞ (Δ ,′ A) ∷ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᶜ B → ⌞ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᶜ B
+val-instᶜ t =
+  msubᶜ
+    (λ
+      { (here refl) → t
+      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
+      })
+    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))
+
+
+comp-instᵛ : V ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B → V ⨾ ⌞ (Δ ,′ B) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A → V ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A
+comp-instᵛ t =
+  msubᵛ
+    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))
+    (λ
+      { (here refl) → t
+      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
+      })
+
+comp-instᶜ : V ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B′ → V ⨾ ⌞ (Δ ,′ B′) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B → V ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B
+comp-instᶜ t =
+  msubᶜ
+    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))
+    (λ
+      { (here refl) → t
+      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
+      })
diff --git a/src/CBPV/Type.agda b/src/CBPV/Type.agda
new file mode 100644
index 0000000..3d27e4e
--- /dev/null
+++ b/src/CBPV/Type.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --safe #-}
+
+module CBPV.Type where
+
+open import Data.List using (List)
+
+data ValType : Set
+data CompType : Set
+
+infix 8 U_ F_
+infixr 7 _×_
+infixr 6 _+_
+infixr 5 _⟶_
+
+data ValType where
+  U_  : CompType → ValType
+  𝟘   : ValType
+  𝟙   : ValType
+  _+_ : ValType → ValType → ValType
+  _×_ : ValType → ValType → ValType
+  _⟶_ : ValType → ValType → ValType
+
+data CompType where
+  F_  : ValType → CompType
+  𝟙   : CompType
+  _×_ : CompType → CompType → CompType
+  _⟶_ : ValType → CompType → CompType