WIP: concrete families

9 files changed, 1366 insertions, 699 deletions

diff --git a/Everything.agda b/Everything.agda
index 03e3ccd..7fcdb94 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -1,7 +1,7 @@
 module Everything where
 
-import CBPV.Axiom
-import CBPV.Equality
+import CBPV.Context
 import CBPV.Family
-import CBPV.Term
+import CBPV.Frex.Comp
+import CBPV.Structure
 import CBPV.Type
diff --git a/src/CBPV/Axiom.agda b/src/CBPV/Axiom.agda
deleted file mode 100644
index 503b61d..0000000
--- a/src/CBPV/Axiom.agda
+++ /dev/null
@@ -1,167 +0,0 @@
-{-# 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/Context.agda b/src/CBPV/Context.agda
new file mode 100644
index 0000000..d1aafc4
--- /dev/null
+++ b/src/CBPV/Context.agda
@@ -0,0 +1,37 @@
+module CBPV.Context where
+
+open import Data.Bool using (Bool)
+open import Data.String using (String)
+import Data.String.Properties as String
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+open import CBPV.Type
+
+abstract
+  Name : Set
+  Name = String
+
+  𝔪 : Name
+  𝔪 = "𝔪"
+
+record Named : Set where
+  constructor _:-_
+  field
+    name   : Name
+    ofType : ValType
+
+open Named public
+
+infixl 5 _:<_ _++_
+
+data Context : Set where
+  [<]  : Context
+  _:<_ : Context → (ex : Named) → Context
+
+pattern [<_:-_] x A = [<] :< (x :- A)
+pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
+
+_++_ : Context → Context → Context
+Γ ++ [<] = Γ
+Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
diff --git a/src/CBPV/Equality.agda b/src/CBPV/Equality.agda
deleted file mode 100644
index f6f58c8..0000000
--- a/src/CBPV/Equality.agda
+++ /dev/null
@@ -1,174 +0,0 @@
-{-# 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
index 94fee5c..4a64726 100644
--- a/src/CBPV/Family.agda
+++ b/src/CBPV/Family.agda
@@ -1,52 +1,362 @@
-{-# 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 Data.List as List using (List; []; _∷_; map)
+open import Data.Unit using (⊤)
+open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_return_of_)
+open import Reflection hiding (name; Name; _≟_)
+open import Reflection.Argument using (_⟨∷⟩_)
+open import Reflection.Term as Term using (_⋯⟅∷⟆_)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (yes; no)
 
+open import CBPV.Context
 open import CBPV.Type
 
+-- Families and Morphisms -----------------------------------------------------
+
+infix 4 _⇾_ _⇾ᵛ_ _⇾ᶜ_
+
+Family : Set₁
+Family = Context → Set
+
+ValFamily : Set₁
+ValFamily = ValType → Family
+
+CompFamily : Set₁
+CompFamily = CompType → Family
+
+_⇾_ : Family → Family → Set
+X ⇾ Y = {Γ : Context} → X Γ → Y Γ
+
+_⇾ᵛ_ : ValFamily → ValFamily → Set
+V ⇾ᵛ W = {A : ValType} → V A ⇾ W A
+
+_⇾ᶜ_ : CompFamily → CompFamily → Set
+C ⇾ᶜ D = {B : CompType} → C B ⇾ D B
+
+-- Variables -------------------------------------------------------------------
+
 private
   variable
-    ℓ ℓ′ : Level
+    Γ Δ Θ Π : Context
+    A A′ : ValType
+    x y : Name
+    V W X : ValFamily
+
+data VarPos (x : Name) (A : ValType) : Context → Set where
+  Here  : VarPos x A (Γ :< (x :- A))
+  There : VarPos x A Γ → VarPos x A (Γ :< (y :- A′))
+
+weaklPos : (Δ : Context) → VarPos x A Γ → VarPos x A (Γ ++ Δ)
+weaklPos [<] i = i
+weaklPos (Δ :< (x :- A)) i = There (weaklPos Δ i)
+
+-- Reflection
+
+wknTerm : Term → Term
+wknTerm t = quote There ⟨ con ⟩ 5 ⋯⟅∷⟆ t ⟨∷⟩ []
+
+weaklTerm : Term → Term → Term
+weaklTerm Δ t = quote weaklPos ⟨ def ⟩ 3 ⋯⟅∷⟆ Δ ⟨∷⟩ t ⟨∷⟩ []
+
+searchCtx :
+  (wkn : Term → Term) →
+  (hole : Term) →
+  (name : Term) →
+  (Γ : Term) →
+  TC ⊤
+searchCtx wkn hole name (meta m _) = blockOnMeta m
+searchCtx wkn hole name (con (quote [<]) []) =
+  typeError (termErr name ∷ strErr " not in context." ∷ [])
+searchCtx wkn hole name (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (meta x _ ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) =
+  blockOnMeta x
+searchCtx wkn hole name (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (x ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) =
+  catchTC
+    (do
+      debugPrint "squid" 10 (strErr "checking name " ∷ termErr x ∷ strErr "..." ∷ [])
+      unify name x
+      let soln = wkn (quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ [])
+      debugPrint "squid" 10 (strErr "testing solution " ∷ termErr soln ∷ strErr "..." ∷ [])
+      unify soln hole
+      debugPrint "squid" 10 (strErr "success!" ∷ []))
+    (searchCtx (wkn ∘ wknTerm) hole name Γ)
+searchCtx wkn hole name (def (quote _++_) (Γ ⟨∷⟩ Δ ⟨∷⟩ [])) =
+  catchTC
+    (searchCtx wkn hole name Δ)
+    (searchCtx (wkn ∘ weaklTerm Δ) hole name Γ)
+searchCtx wkn hole name Γ =
+  typeError (termErr name ∷ strErr " not in context " ∷ termErr Γ ∷ [])
+-- searchCtx (con (quote [<]) []) y = return []
+-- searchCtx (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (x ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) y =
+-- --   with x Term.≟ y
+-- -- ... | yes _ =
+--   do
+--     let head = quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ []
+--     tail ← searchCtx Γ y
+--     return (head ∷ map wknTerm tail)
+-- -- ... | no  _ =
+-- --   do
+-- --     tail ← searchCtx Γ y
+-- --     return (map wknTerm tail)
+-- searchCtx (def (quote _++_) (Γ ⟨∷⟩ Δ ⟨∷⟩ [])) y =
+--   do
+--     right ← searchCtx Δ y
+--     left ← searchCtx Γ y
+--     return (right List.++ map (weaklTerm Δ) left)
+
+-- searchCtx (meta m _) y = blockOnMeta m
+-- searchCtx Γ y =
+--   do
+--     debugPrint "squid" 10 (strErr "stuck matching term " ∷ termErr Γ ∷ [])
+--     return []
+
+-- tryEach : List Term → Term → TC ⊤
+-- tryEach [] hole = typeError (strErr "not in context" ∷ [])
+-- tryEach (t ∷ []) hole =
+--   do
+--     debugPrint "squid" 10 (strErr "trying term " ∷ termErr t ∷ [])
+--     unify t hole
+--     debugPrint "squid" 10 (strErr "success!" ∷ [])
+-- tryEach (t ∷ ts@(_ ∷ _)) hole =
+--   do
+--     debugPrint "squid" 10 (strErr "trying term " ∷ termErr t ∷ [])
+--     catchTC
+--       (do
+--         unify t hole
+--         debugPrint "squid" 10 (strErr "success!" ∷ []))
+--       (tryEach ts hole)
+
+searchVarPos : Context → Name → Term → TC ⊤
+searchVarPos Γ x hole =
+  do
+    Γ ← quoteTC Γ
+    x ← quoteTC x
+    case x return (λ _ → TC ⊤) of λ
+      { (meta x _) → blockOnMeta x
+      ; _ → return _
+      }
+    debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ [])
+    debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ [])
+    searchCtx (λ t → t) hole x Γ
+
+-- searchVarPos : Context → Name → Term → TC ⊤
+-- searchVarPos Γ x hole =
+--   do
+--     Γ ← quoteTC Γ
+--     (case Γ return (λ _ → TC ⊤) of λ
+--       { (meta m _) → blockOnMeta m
+--       ; _ → return _
+--       })
+--     x ← quoteTC x
+--     debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ [])
+--     debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ [])
+--     guesses ← searchCtx Γ x
+--     tryEach guesses hole
+
+-- Back to business as normal
+
+record Var (A : ValType) (Γ : Context) : Set where
+  constructor %%_
+  field
+    name : Name
+    @(tactic searchVarPos Γ name) {pos} : VarPos name A Γ
+
+open Var public
+
+toVar : VarPos x A Γ → Var A Γ
+toVar pos = (%% _) {pos}
+
+ThereVar : Var A Γ → Var A (Γ :< (y :- A′))
+ThereVar i = toVar $ There (i .pos)
+
+-- Substitutions --------------------------------------------------------------
+
+infixl 9 _⨾_ [_]_⨾_
+infixr 8 _＠_
+infixl 5 _:<_↦_
+infix 4 Subst _↝_
+
+data Subst (V : ValFamily) (Δ : Context) : Context → Set where
+  [<]     : Subst V Δ [<]
+  _:<_↦_ : Subst V Δ Γ → (x : Name) → V A Δ → Subst V Δ (Γ :< (x :- A))
+
+syntax Subst V Δ Γ = Γ ~[ V ]↝ Δ
+
+_↝_ : Context → Context → Set
+Γ ↝ Δ = Γ ~[ Var ]↝ Δ
+
+_⨾_ : Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ
+[<] ⨾ f = [<]
+(σ :< x ↦ v) ⨾ f = (σ ⨾ f) :< x ↦ f v
+
+[_]_⨾_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ
+[ V ] σ ⨾ f = σ ⨾ f
+
+tabulate : (∀ {A} → Var A Γ → V A Δ) → Γ ~[ V ]↝ Δ
+tabulate {Γ = [<]} f = [<]
+tabulate {Γ = Γ :< (x :- A)} f = tabulate (f ∘ ThereVar) :< x ↦ f (toVar Here)
+
+lookup : Γ ~[ V ]↝ Δ → VarPos x A Γ → V A Δ
+lookup (σ :< x ↦ v) Here = v
+lookup (σ :< x ↦ v) (There i) = lookup σ i
+
+_＠_ : Γ ~[ V ]↝ Δ → Var A Γ → V A Δ
+σ ＠ i = lookup σ (i .pos)
+
+[_]_＠_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → Var A Γ → V A Δ
+[ V ] σ ＠ i = σ ＠ i
+
+id : Γ ↝ Γ
+id = tabulate (λ x → x)
+
+weakrPos : VarPos x A Δ → VarPos x A (Γ ++ Δ)
+weakrPos Here = Here
+weakrPos (There i) = There (weakrPos i)
+
+weakrF : Var A Δ → Var A (Γ ++ Δ)
+weakrF i = toVar $ weakrPos $ i .pos
+
+weakr : Δ ↝ Γ ++ Δ
+weakr = tabulate weakrF
+
+weaklF : (Δ : Context) → Var A Γ → Var A (Γ ++ Δ)
+weaklF Δ i = toVar $ weaklPos Δ $ i .pos
+
+weakl : (Δ : Context) → Γ ↝ Γ ++ Δ
+weakl Δ = tabulate (weaklF Δ)
+
+copair : Γ ~[ V ]↝ Θ → Δ ~[ V ]↝ Θ → Γ ++ Δ ~[ V ]↝ Θ
+copair σ [<] = σ
+copair σ (ς :< x ↦ v) = copair σ ς :< x ↦ v
+
+pull : (Δ Θ : Context) → Γ ++ Δ ++ Θ ↝ Γ ++ Θ ++ Δ
+pull Δ Θ =
+  copair {Δ = Θ}
+    (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr)
+    (weakr ⨾ (weakl Δ ＠_))
+
+-- Properties
+
+subst-ext : (σ ς : Γ ~[ V ]↝ Δ) → (∀ {A} → (i : Var A Γ) → σ ＠ i ≡ ς ＠ i) → σ ≡ ς
+subst-ext [<] [<] ext = refl
+subst-ext (σ :< x ↦ v) (ς :< .x ↦ w) ext =
+  cong₂ (_:< x ↦_) (subst-ext σ ς $ λ i → ext $ ThereVar i) (ext $ %% x)
+
+⨾-assoc :
+  (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (g : ∀ {A} → W A Θ → X A Π) →
+  _⨾_ {V = W} {W = X} (σ ⨾ f) g ≡ σ ⨾ (g ∘ f)
+⨾-assoc [<] f g = refl
+⨾-assoc (σ :< x ↦ v) f g = cong (_:< x ↦ g (f v)) (⨾-assoc σ f g)
+
+⨾-cong :
+  (σ : Γ ~[ V ]↝ Δ) {f g : ∀ {A} → V A Δ → W A Θ} →
+  (∀ {A} → (v : V A Δ) → f v ≡ g v) →
+  _⨾_ {W = W} σ f ≡ σ ⨾ g
+⨾-cong [<] ext = refl
+⨾-cong (σ :< x ↦ v) ext = cong₂ (_:< x ↦_) (⨾-cong σ ext) (ext v)
+
+lookup-⨾ :
+  (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (i : VarPos x A Γ) →
+  lookup {V = W} (σ ⨾ f) i ≡ f (lookup σ i)
+lookup-⨾ (σ :< x ↦ v) f Here = refl
+lookup-⨾ (σ :< x ↦ v) f (There i) = lookup-⨾ σ f i
+
+lookup-tabulate :
+  (V : ValFamily) (f : ∀ {A} → Var A Γ → V A Δ) (i : VarPos x A Γ) →
+  lookup {V = V} (tabulate f) i ≡ f (toVar i)
+lookup-tabulate V f Here = refl
+lookup-tabulate V f (There i) = lookup-tabulate V (f ∘ ThereVar) i
+
+＠-⨾ :
+  (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (i : Var A Γ) →
+  _＠_ {V = W} (σ ⨾ f) i ≡ f (σ ＠ i)
+＠-⨾ σ f i = lookup-⨾ σ f (i .pos)
+
+＠-tabulate :
+  (V : ValFamily) (f : ∀ {A} → Var A Γ → V A Δ) (i : Var A Γ) →
+  _＠_ {V = V} (tabulate f) i ≡ f i
+＠-tabulate V f i = lookup-tabulate V f (i .pos)
+
+tabulate-cong :
+  (V : ValFamily) →
+  {f g : ∀ {A} → Var A Γ → V A Δ} →
+  (∀ {A} → (v : Var A Γ) → f v ≡ g v) →
+  tabulate {V = V} f ≡ tabulate g
+tabulate-cong {Γ = [<]} V ext = refl
+tabulate-cong {Γ = Γ :< (x :- A)} V ext =
+  cong₂ (_:< x ↦_) (tabulate-cong V (ext ∘ ThereVar)) (ext $ %% x)
+
+tabulate-⨾ :
+  (f : ∀ {A} → Var A Γ → V A Δ) (g : ∀ {A} → V A Δ → W A Θ) →
+  tabulate {V = V} f ⨾ g ≡ tabulate {V = W} (g ∘ f)
+tabulate-⨾ {Γ = [<]} f g = refl
+tabulate-⨾ {Γ = Γ :< (x :- A)} f g = cong (_:< x ↦ g (f $ toVar Here)) (tabulate-⨾ (f ∘ ThereVar) g)
+
+tabulate-＠ : (σ : Γ ~[ V ]↝ Δ) → tabulate (σ ＠_) ≡ σ
+tabulate-＠ [<] = refl
+tabulate-＠ (σ :< x ↦ v) = cong (_:< x ↦ v) (tabulate-＠ σ)
+
+copair-⨾ :
+  (σ : Γ ~[ V ]↝ Θ) (ς : Δ ~[ V ]↝ Θ) (f : ∀ {A} → V A Θ → W A Π) →
+  copair {V = W} (σ ⨾ f) (ς ⨾ f) ≡ copair {V = V} σ ς ⨾ f
+copair-⨾ σ [<] f = refl
+copair-⨾ σ (ς :< x ↦ v) f = cong (_:< x ↦ f v) (copair-⨾ σ ς f)
+
+copair-left :
+  (σ : Γ ~[ V ]↝ Θ) (ς : Δ ~[ V ]↝ Θ) (i : VarPos x A Γ) →
+  lookup (copair σ ς) (weaklPos Δ i) ≡ lookup σ i
+copair-left σ [<] i = refl
+copair-left σ (ς :< x ↦ v) i = copair-left σ ς i
 
-Context : Set
-Context = List ValType
+pull-left :
+  (Δ Θ : Context) (i : VarPos x A Γ) →
+  lookup (pull Δ Θ) (weaklPos Θ $ weaklPos Δ i) ≡ toVar (weaklPos Δ $ weaklPos Θ i)
+pull-left {Γ = Γ} Δ Θ i =
+  begin
+    lookup (pull Δ Θ) (weaklPos Θ $ weaklPos Δ i)
+  ≡⟨ copair-left (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) (weakr {Γ = Γ} ⨾ (weakl Δ ＠_)) (weaklPos Δ i) ⟩
+    lookup (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) (weaklPos Δ i)
+  ≡⟨ copair-left {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr i ⟩
+    lookup (weakl Θ ⨾ (weakl Δ ＠_)) i
+  ≡⟨ lookup-⨾ (weakl Θ) (weakl Δ ＠_) i ⟩
+    weakl Δ ＠ lookup (weakl Θ) i
+  ≡⟨ cong (weakl Δ ＠_) (lookup-tabulate Var (weaklF Θ) i) ⟩
+    lookup (weakl Δ) (weaklPos Θ i)
+  ≡⟨ lookup-tabulate Var (weaklF Δ) (weaklPos Θ i) ⟩
+    toVar (weaklPos Δ $ weaklPos Θ i)
+  ∎
+  where open ≡-Reasoning
 
-ValFamily : (ℓ : Level) → Set (suc ℓ)
-ValFamily ℓ = Context → ValType → Set ℓ
+-- Special Families -----------------------------------------------------------
 
-CompFamily : (ℓ : Level) → Set (suc ℓ)
-CompFamily ℓ = Context → CompType → Set ℓ
+infixr 5 _⇒_
 
-δᵛ : Context → ValFamily ℓ → ValFamily ℓ
-δᵛ Δ V Γ A = V (Γ ++ Δ) A
+_⇒_ : Family → Family → Family
+(X ⇒ Y) Γ = X Γ → Y Γ
 
-δᶜ : Context → CompFamily ℓ → CompFamily ℓ
-δᶜ Δ C Γ B = C (Γ ++ Δ) B
+_^_ : Family → ValFamily → Family
+(X ^ V) Γ = {Δ : Context} → Γ ~[ V ]↝ Δ → X Δ
 
-infix 0 _⇒ᵛ_ _⇒ᶜ_ _~[_]↝ᵛ_ _~[_]↝ᶜ_
+_^ᵛ_ : ValFamily → ValFamily → ValFamily
+(W ^ᵛ V) A = W A ^ V
 
-_⇒ᵛ_ : ValFamily ℓ → ValFamily ℓ′ → Set (ℓ ⊔ ℓ′)
-V ⇒ᵛ V′ = ∀ {Γ A} → V Γ A → V′ Γ A
+_^ᶜ_ : CompFamily → ValFamily → CompFamily
+(C ^ᶜ V) B = C B ^ V
 
-_⇒ᶜ_ : CompFamily ℓ → CompFamily ℓ′ → Set (ℓ ⊔ ℓ′)
-C ⇒ᶜ C′ = ∀ {Γ B} → C Γ B → C′ Γ B
+□_ : Family → Family
+□_ = _^ Var
 
-_~[_]↝ᵛ_ : List ValType → ValFamily ℓ → Context → Set ℓ
-As ~[ V ]↝ᵛ Γ = ∀ {A} → A ∈ As → V Γ A
+□ᵛ_ : ValFamily → ValFamily
+□ᵛ_ = _^ᵛ Var
 
-_~[_]↝ᶜ_ : List CompType → CompFamily ℓ → Context → Set ℓ
-Bs ~[ C ]↝ᶜ Γ = ∀ {B} → B ∈ Bs → C Γ B
+□ᶜ_ : CompFamily → CompFamily
+□ᶜ_ = _^ᶜ Var
 
-I : ValFamily _
-I Γ A = A ∈ Γ
+δ : Context → Family → Family
+δ Δ X Γ = X (Γ ++ Δ)
 
-⌞_⌟ᵛ : List (Context ×′ ValType) → ValFamily _
-⌞ Vs ⌟ᵛ Γ A = (Γ , A) ∈ Vs
+δᵛ : Context → ValFamily → ValFamily
+δᵛ Δ V A = δ Δ (V A)
 
-⌞_⌟ᶜ : List (Context ×′ CompType) → CompFamily _
-⌞ Cs ⌟ᶜ Γ B = (Γ , B) ∈ Cs
+δᶜ : Context → CompFamily → CompFamily
+δᶜ Δ C B = δ Δ (C B)
diff --git a/src/CBPV/Frex/Comp.agda b/src/CBPV/Frex/Comp.agda
new file mode 100644
index 0000000..1ae5b4d
--- /dev/null
+++ b/src/CBPV/Frex/Comp.agda
@@ -0,0 +1,324 @@
+open import Data.List using (List)
+
+open import CBPV.Structure
+open import CBPV.Type
+
+module CBPV.Frex.Comp
+  {A : RawAlgebra} (Aᴹ : IsModel A)
+  (Θ : List ValType) (Ψ : List CompType) (T : CompType)
+  where
+
+open import Function.Base using (_∘_; _$_)
+open import Function.Nary.NonDependent using (congₙ)
+open import Relation.Binary.PropositionalEquality.Core
+
+open ≡-Reasoning
+
+open import CBPV.Context
+open import CBPV.Family
+
+private
+  variable
+    Γ Δ Π : Context
+    x y : Name
+    A′ A′′ : ValType
+    B : CompType
+
+  module A where
+    open RawAlgebra A public
+    open IsModel Aᴹ public
+
+  ⟦T⟧ : ValType
+  ⟦T⟧ = U (Θ ⟶⋆ Ψ ⟶′⋆ T)
+
+  𝔐 : Context
+  𝔐 = [< 𝔪 :- ⟦T⟧ ]
+
+-- Cast and Expand substitutions
+
+cast : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ ~[ A.Val ]↝ Δ ++ 𝔐
+cast σ = σ ⨾ λ ◌ → ◌
+
+expand : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ :< (𝔪 :- ⟦T⟧) ~[ A.Val ]↝ Δ :< (𝔪 :- ⟦T⟧)
+expand σ = cast σ :< 𝔪 ↦ A.var (%% 𝔪)
+
+cast-comm :
+  (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (f : ∀ {A} → δᵛ 𝔐 A.Val A Δ → δᵛ 𝔐 A.Val A Π) →
+  cast σ ⨾ f ≡ cast (σ ⨾ f)
+cast-comm σ f = begin
+  cast σ ⨾ f   ≡⟨ ⨾-assoc σ (λ ◌ → ◌) f ⟩
+  σ ⨾ f        ≡˘⟨ ⨾-assoc σ f (λ ◌ → ◌) ⟩
+  cast (σ ⨾ f) ∎
+
+lookup-cast : (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (i : VarPos x A′ Γ) → lookup (cast σ) i ≡ lookup σ i
+lookup-cast σ i = lookup-⨾ σ (λ ◌ → ◌) i
+
+＠-cast : (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (i : Var A′ Γ) → cast σ ＠ i ≡ σ ＠ i
+＠-cast σ i = ＠-⨾ σ (λ ◌ → ◌) i
+
+expand-wkn : expand (id {Γ = Γ} ⨾ (A.var ∘ ThereVar)) ≡ (id ⨾ A.var)
+expand-wkn = cong (_:< 𝔪 ↦ A.var (%% 𝔪)) $ begin
+  cast (id ⨾ (A.var ∘ ThereVar)) ≡⟨ ⨾-assoc id (A.var ∘ ThereVar) (λ ◌ → ◌) ⟩
+  id ⨾ (A.var ∘ ThereVar)        ≡˘⟨ ⨾-assoc {W = Var} id ThereVar A.var ⟩
+  id ⨾ ThereVar ⨾ A.var          ≡⟨ cong (_⨾ A.var) (tabulate-⨾ (λ ◌ → ◌) ThereVar) ⟩
+  tabulate ThereVar ⨾ A.var      ∎
+
+-- Monoid Structure
+
+open RawMonoid
+
+frexMonoid : RawMonoid
+frexMonoid .Val = δᵛ 𝔐 A.Val
+frexMonoid .Comp = δᶜ 𝔐 A.Comp
+frexMonoid .var i = A.var (ThereVar i)
+frexMonoid .subᵛ v σ = A.subᵛ v (expand σ)
+frexMonoid .subᶜ c σ = A.subᶜ c (expand σ)
+
+open IsMonoid
+
+frexIsMonoid : IsMonoid frexMonoid
+frexIsMonoid .subᵛ-var i σ = begin
+  A.subᵛ (A.var $ ThereVar i) (expand σ) ≡⟨ A.subᵛ-var (ThereVar i) (expand σ) ⟩
+  expand σ ＠ ThereVar i                 ≡⟨⟩
+  cast σ ＠ i                            ≡⟨ ＠-cast σ i ⟩
+  σ ＠ i                                 ∎
+frexIsMonoid .renᵛ-id v = begin
+  A.subᵛ v (expand (id ⨾ λ ◌ → A.var $ ThereVar ◌)) ≡⟨ cong (A.subᵛ v) expand-wkn ⟩
+  A.renᵛ v id                                       ≡⟨ A.renᵛ-id v ⟩
+  v                                                 ∎
+frexIsMonoid .subᵛ-assoc v σ ς =
+  begin
+    A.subᵛ (A.subᵛ v (expand σ)) (expand ς)
+  ≡⟨ A.subᵛ-assoc v (expand σ) (expand ς) ⟩
+    A.subᵛ v (expand σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς))
+  ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → A.subᵛ v (◌ᵃ :< 𝔪 ↦ ◌ᵇ))
+       (cast-comm σ (λ ◌ → A.subᵛ ◌ (expand ς)))
+       (A.subᵛ-var (%% 𝔪) (expand ς)) ⟩
+    A.subᵛ v (expand (σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)))
+  ∎
+frexIsMonoid .renᶜ-id c = begin
+  A.subᶜ c (expand (id ⨾ λ ◌ → A.var $ ThereVar ◌)) ≡⟨ cong (A.subᶜ c) expand-wkn ⟩
+  A.renᶜ c id                                       ≡⟨ A.renᶜ-id c ⟩
+  c                                                 ∎
+frexIsMonoid .subᶜ-assoc c σ ς =
+  begin
+    A.subᶜ (A.subᶜ c (expand σ)) (expand ς)
+  ≡⟨ A.subᶜ-assoc c (expand σ) (expand ς) ⟩
+    A.subᶜ c ((cast σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)) :< 𝔪 ↦ A.subᵛ (A.var $ %% 𝔪) (expand ς))
+  ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → A.subᶜ c (◌ᵃ :< 𝔪 ↦ ◌ᵇ))
+       (cast-comm σ (λ ◌ → A.subᵛ ◌ (expand ς)))
+       (A.subᵛ-var (%% 𝔪) (expand ς)) ⟩
+    A.subᶜ c (expand (σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)))
+  ∎
+
+open RawAlgebra
+  renaming
+    ( have_be_ to [_]have_be_
+    ; drop_then_ to [_]drop_then_
+    ; ⟨_,_⟩ to [_]⟨_,_⟩
+    ; split_then_ to [_]split_then_
+    ; case_of_or_ to [_]case_of_or_
+    ; bind_to_ to [_]bind_to_
+    ; ⟪_,_⟫ to [_]⟪_,_⟫
+    ; push_then_ to [_]push_then_
+    )
+
+frexAlgebra : RawAlgebra
+frexAlgebra .monoid = frexMonoid
+[ frexAlgebra ]have v be c = A.have v be A.renᶜ c (pull [< _ :- _ ] 𝔐)
+frexAlgebra .thunk c = A.thunk c
+frexAlgebra .force v = A.force v
+frexAlgebra .point = A.point
+[ frexAlgebra ]drop v then c = A.drop v then c
+[ frexAlgebra ]⟨ v , w ⟩ = A.⟨ v , w ⟩
+[ frexAlgebra ]split v then c = A.split v then A.renᶜ c (pull [< _ :- _ , _ :- _ ] 𝔐)
+frexAlgebra .inl v = A.inl v
+frexAlgebra .inr v = A.inr v
+[ frexAlgebra ]case v of c or d =
+  A.case v
+  of A.renᶜ c (pull [< _ :- _ ] 𝔐)
+  or A.renᶜ d (pull [< _ :- _ ] 𝔐)
+frexAlgebra .ret v = A.ret v
+[ frexAlgebra ]bind c to d = A.bind c to A.renᶜ d (pull [< _ :- _ ] 𝔐)
+[ frexAlgebra ]⟪ c , d ⟫ = A.⟪ c , d ⟫
+frexAlgebra .fst c = A.fst c
+frexAlgebra .snd c = A.snd c
+frexAlgebra .pop c = A.pop (A.renᶜ c (pull [< _ :- _ ] 𝔐))
+[ frexAlgebra ]push v then c = A.push v then c
+
+private module X = RawAlgebra frexAlgebra
+
+open IsAlgebra
+
+lemma₀ : (v : X.Val A′ Γ) (ρ : Γ ↝ Δ) → X.renᵛ v ρ ≡ A.renᵛ v (ρ ⨾ ThereVar :< 𝔪 ↦ %% 𝔪)
+lemma₀ {A′ = A′} v ρ = begin
+  X.renᵛ v ρ                                                   ≡⟨⟩
+  X.subᵛ v (ρ ⨾ X.var)                                         ≡⟨⟩
+  A.subᵛ v (expand (ρ ⨾ X.var))                                ≡⟨⟩
+  A.subᵛ v (cast (ρ ⨾ X.var) :< 𝔪 ↦ A.var (%% 𝔪))              ≡⟨⟩
+  A.subᵛ v (cast (ρ ⨾ (A.var ∘ ThereVar)) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ cong (λ ◌ → A.subᵛ v (◌ :< 𝔪 ↦ A.var (toVar Here))) (⨾-assoc ρ (A.var ∘ ThereVar) (λ ◌ → ◌)) ⟩
+  A.subᵛ v (ρ ⨾ (A.var ∘ ThereVar) :< 𝔪 ↦ A.var (%% 𝔪))        ≡˘⟨ cong (λ ◌ → A.subᵛ v (◌ :< 𝔪 ↦ A.var (toVar Here))) (⨾-assoc ρ ThereVar A.var) ⟩
+  A.subᵛ v (ρ ⨾ ThereVar ⨾ A.var :< 𝔪 ↦ A.var (%% 𝔪))          ≡⟨⟩
+  A.subᵛ v ((ρ ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) ⨾ A.var)                ≡⟨⟩
+  A.renᵛ v (ρ ⨾ ThereVar {y = 𝔪} :< 𝔪 ↦ %% 𝔪)                  ∎
+
+lemma₁ :
+  (c : δᶜ [< x :- A′ ] X.Comp B Γ) (σ : Γ ~[ X.Val ]↝ Δ) →
+  A.subᶜ (A.renᶜ c (pull [< x :- A′ ] 𝔐)) (A.lift [< x :- A′ ] (expand σ)) ≡
+  A.renᶜ (X.subᶜ c (X.lift [< x :- A′ ] σ)) (pull [< x :- A′ ] 𝔐)
+lemma₁ {x = x} c σ =
+  begin
+    A.subᶜ (A.renᶜ c (pull [< x :- _ ] 𝔐)) (A.lift [< x :- _ ] (expand σ))
+  ≡⟨ A.subᶜ-renᶜ c (pull [< x :- _ ] 𝔐) (A.lift [< x :- _ ] (expand σ)) ⟩
+    A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ (A.lift [< x :- _ ] (expand σ) ＠_))
+  ≡⟨ congₙ 3 (λ ◌ᵃ ◌ᵇ ◌ᶜ → A.subᶜ c (◌ᵃ :< x ↦ ◌ᵇ :< 𝔪 ↦ ◌ᶜ))
+       (begin
+          weakl 𝔐 ⨾ (weakl [< x :- _ ] ＠_) ⨾ (A.lift [< x :- _ ] (expand σ) ＠_)
+        ≡⟨ cong (_⨾ (A.lift [< x :- _ ] (expand σ) ＠_)) (⨾-cong (weakl 𝔐) (＠-tabulate Var ThereVar)) ⟩
+          weakl 𝔐 ⨾ ThereVar ⨾ (A.lift [< x :- _ ] (expand σ) ＠_)
+        ≡⟨ ⨾-assoc (weakl 𝔐) ThereVar (A.lift [< x :- _ ] (expand σ) ＠_) ⟩
+          weakl 𝔐 ⨾ (λ ◌ → A.lift [< x :- _ ] (expand σ) ＠ ThereVar ◌)
+        ≡⟨ ⨾-cong (weakl 𝔐) (＠-⨾ (expand σ) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) ⟩
+          weakl 𝔐 ⨾ (λ ◌ → A.renᵛ (expand σ ＠ ◌) (weakl [< x :- _ ]))
+        ≡˘⟨ ⨾-assoc (weakl 𝔐) (expand σ ＠_) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) ⟩
+          ([ A.Val ] (weakl 𝔐 ⨾ (expand σ ＠_)) ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])))
+        ≡⟨ cong (_⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) (tabulate-⨾ (weaklF 𝔐) (expand σ ＠_)) ⟩
+          tabulate (cast σ ＠_) ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))
+        ≡⟨ cong (_⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) (tabulate-＠ (cast σ)) ⟩
+          cast σ ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))
+        ≡⟨ ⨾-assoc σ (λ ◌ → ◌) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) ⟩
+          σ ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))
+        ≡⟨ ⨾-cong σ (λ v → cong (λ ◌ → A.renᵛ v (◌ :< 𝔪 ↦ %% 𝔪)) $
+             begin
+               tabulate (ThereVar ∘ ThereVar)                              ≡˘⟨ tabulate-cong Var (λ i → pull-left [< x :- _ ] 𝔐 (i .pos)) ⟩
+               (tabulate ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar ∘ ThereVar)) ≡˘⟨ tabulate-⨾ {V = Var} ThereVar ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar) ⟩
+               (tabulate ThereVar ⨾ ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar)) ≡˘⟨ ⨾-assoc (tabulate ThereVar) ThereVar (pull [< x :- _ ] 𝔐 ＠_) ⟩
+               (tabulate ThereVar ⨾ ThereVar ⨾ (pull [< x :- _ ] 𝔐 ＠_))   ∎) ⟩
+          σ ⨾ (λ ◌ → A.renᵛ ◌ ((weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) ⨾ (pull [< x :- _ ] 𝔐 ＠_)))
+        ≡˘⟨ ⨾-cong σ (λ v → A.renᵛ-assoc v (weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) (pull [< x :- _ ] 𝔐)) ⟩
+          σ ⨾ (λ ◌ → A.renᵛ (A.renᵛ ◌ (weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪)) (pull [< x :- _ ] 𝔐))
+        ≡˘⟨ ⨾-cong σ (λ v → cong (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) (lemma₀ v (weakl [< x :- _ ]))) ⟩
+          σ ⨾ (λ ◌ → A.renᵛ (X.renᵛ ◌ (weakl [< x :- _ ])) (pull [< x :- _ ] 𝔐))
+        ≡˘⟨ ⨾-assoc σ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) ⟩
+          σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) ⨾ (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐))
+        ≡˘⟨ ⨾-assoc (σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ]))) (λ ◌ → ◌) (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) ⟩
+          σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) ⨾ (λ ◌ → ◌) ⨾ (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐))
+        ∎)
+       (begin
+         A.var (%% x)                                 ≡˘⟨ A.renᵛ-var (%% x) (pull [< x :- _ ] 𝔐) ⟩
+         A.renᵛ (A.var (%% x)) (pull [< x :- _ ] 𝔐) ∎)
+       {!!} ⟩
+    A.subᶜ c (expand (X.lift [< x :- _ ] σ) ⨾ λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐))
+  ≡˘⟨ A.subᶜ-assoc c (expand $ X.lift [< x :- _ ] σ) (pull [< x :- _ ] 𝔐 ⨾ A.var) ⟩
+    A.renᶜ (A.subᶜ c (expand $ X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐)
+  ≡⟨⟩
+    A.renᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐)
+  ∎
+-- lemma₁ {x = x} {A′} c σ =
+--   begin
+--     A.subᶜ (A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ A.var)) (A.lift [< x :- _ ] (expand σ))
+--   ≡⟨ A.subᶜ-assoc c (pull [< x :- _ ] 𝔐 ⨾ A.var) (A.lift [< x :- _ ] (expand σ)) ⟩
+--     A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- _ ] (expand σ)))
+--   ≡⟨ cong (A.subᶜ c) (subst-ext _ _ (λ i → helper (i .pos))) ⟩
+--     A.subᶜ c (expand (X.lift [< x :- _ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- _ ] 𝔐 ⨾ A.var))
+--   ≡˘⟨ A.subᶜ-assoc c (expand (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐 ⨾ A.var) ⟩
+--     A.subᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐 ⨾ A.var)
+--   ∎
+--   where
+--   helper :
+--     (i : VarPos y A′′ _) →
+--       lookup
+--         (pull [< x :- A′ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ)))
+--         i
+--     ≡
+--       lookup {V = A.Val}
+--         (expand (X.lift [< x :- A′ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var))
+--         i
+--   helper Here = begin
+--     A.subᵛ (A.var $ toVar $ There Here) (A.lift [< x :- _ ] (expand σ)) ≡⟨ A.subᵛ-var _ _ ⟩
+--     A.subᵛ (A.var $ %% 𝔪) (weakl [< x :- A′ ] ⨾ A.var)                  ≡⟨ A.subᵛ-var _ _ ⟩
+--     A.var (%% 𝔪)                                                        ≡˘⟨ A.subᵛ-var _ _ ⟩
+--     A.subᵛ (A.var $ %% 𝔪) (pull [< x :- _ ] 𝔐 ⨾ A.var)                  ∎
+--   helper (There Here) = begin
+--     A.subᵛ (A.var $ %% x) (A.lift [< x :- _ ] (expand σ)) ≡⟨ A.subᵛ-var _ _ ⟩
+--     A.var (%% x)                                          ≡˘⟨ A.subᵛ-var _ _ ⟩
+--     A.subᵛ (A.var $ %% x) (pull [< x :- _ ] 𝔐 ⨾ A.var)   ∎
+--   helper (There (There i)) =
+--     begin
+--       lookup
+--         (pull [< x :- _ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ)))
+--         (There $ There i)
+--     ≡⟨ lookup-⨾ (pull [< x :- _ ] 𝔐 ⨾ A.var) (λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) (There $ There i) ⟩
+--       A.subᵛ
+--         (lookup {V = A.Val}
+--           (pull [< x :- _ ] 𝔐 ⨾ A.var)
+--           (There $ There i))
+--         (A.lift [< x :- A′ ] (expand σ))
+--     ≡⟨ cong (λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) (lookup-⨾ (pull [< x :- _ ] 𝔐) A.var (There $ There i)) ⟩
+--       A.subᵛ
+--         (A.var $ lookup (pull [< x :- _ ] 𝔐) (There $ There i))
+--         (A.lift [< x :- A′ ] (expand σ))
+--     ≡⟨ A.subᵛ-var (lookup (pull [< x :- _ ] 𝔐) (There $ There i)) (A.lift [< x :- A′ ] (expand σ)) ⟩
+--       A.lift [< x :- A′ ] (expand σ) ＠
+--        lookup (pull [< x :- _ ] 𝔐) (There $ There i)
+--     ≡⟨ cong (A.lift [< x :- _ ] (expand σ) ＠_) (pull-left [< x :- _ ] 𝔐 i) ⟩
+--       lookup (A.lift [< x :- A′ ] (expand σ)) (There $ There i)
+--     ≡⟨ A.lift-left [< x :- A′ ] (expand σ) (There i) ⟩
+--       A.subᵛ (lookup (cast σ) i) (weakl [< x :- A′ ] ⨾ A.var)
+--     ≡⟨ cong (λ ◌ → A.subᵛ ◌ (weakl [< x :- A′ ] ⨾ A.var)) (lookup-cast σ i) ⟩
+--       A.subᵛ (lookup σ i) (weakl [< x :- A′ ] ⨾ A.var)
+--     ≡⟨ {!!} ⟩
+--       A.subᵛ (lookup σ i)
+--         (expand (weakl [< x :- A′ ] ⨾ X.var) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var))
+--     ≡˘⟨ A.subᵛ-assoc (lookup σ i) (expand (weakl [< x :- A′ ] ⨾ X.var)) (pull [< x :- A′ ] 𝔐 ⨾ A.var) ⟩
+--       A.subᵛ
+--         (A.subᵛ (lookup σ i) (expand (weakl [< x :- A′ ] ⨾ X.var)))
+--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
+--     ≡⟨⟩
+--       A.subᵛ
+--         (X.subᵛ (lookup σ i) (weakl [< x :- A′ ] ⨾ X.var))
+--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
+--     ≡˘⟨ cong (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (X.lift-left [< x :- A′ ] σ i) ⟩
+--       A.subᵛ
+--         (lookup (X.lift [< x :- A′ ] σ) (There i))
+--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
+--     ≡˘⟨ cong (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (lookup-cast (X.lift [< x :- A′ ] σ) (There i)) ⟩
+--       A.subᵛ
+--         (lookup (cast $ X.lift [< x :- A′ ] σ) (There i))
+--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
+--     ≡˘⟨ lookup-⨾ (expand (X.lift [< x :- A′ ] σ)) (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (There $ There i) ⟩
+--       lookup {V = A.Val}
+--         (expand (X.lift [< x :- A′ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var))
+--         (There $ There i)
+--     ∎
+
+-- frexIsAlgebra : IsAlgebra frexAlgebra
+-- frexIsAlgebra .isMonoid = frexIsMonoid
+-- frexIsAlgebra .sub-have v c σ =
+--   begin
+--     A.subᶜ
+--       (A.have v be A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var))
+--       (expand σ)
+--   ≡⟨ A.sub-have v (A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) (expand σ) ⟩
+--     (A.have A.subᵛ v (expand σ) be
+--       A.subᶜ (A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) (A.lift [< _ :- _ ] (expand σ)))
+--   ≡⟨ cong (λ ◌ → A.have A.subᵛ v (expand σ) be ◌) (lemma₁ c σ) ⟩
+--     (A.have A.subᵛ v (expand σ) be
+--       A.subᶜ (X.subᶜ c (X.lift [< _ :- _ ] σ)) (pull [< _ :- _ ] 𝔐 ⨾ A.var))
+--   ∎
+-- frexIsAlgebra .sub-thunk c σ = A.sub-thunk c (expand σ)
+-- frexIsAlgebra .sub-force v σ = A.sub-force v (expand σ)
+-- frexIsAlgebra .sub-point σ = A.sub-point (expand σ)
+-- frexIsAlgebra .sub-drop v c σ = A.sub-drop v c (expand σ)
+-- frexIsAlgebra .sub-pair v w σ = A.sub-pair v w (expand σ)
+-- frexIsAlgebra .sub-split = {!!}
+-- frexIsAlgebra .sub-inl v σ = A.sub-inl v (expand σ)
+-- frexIsAlgebra .sub-inr v σ = A.sub-inr v (expand σ)
+-- frexIsAlgebra .sub-case = {!!}
+-- frexIsAlgebra .sub-ret v σ = A.sub-ret v (expand σ)
+-- frexIsAlgebra .sub-bind = {!!}
+-- frexIsAlgebra .sub-bundle c d σ = A.sub-bundle c d (expand σ)
+-- frexIsAlgebra .sub-fst c σ = A.sub-fst c (expand σ)
+-- frexIsAlgebra .sub-snd c σ = A.sub-snd c (expand σ)
+-- frexIsAlgebra .sub-pop = {!!}
+-- frexIsAlgebra .sub-push v c σ = A.sub-push v c (expand σ)
diff --git a/src/CBPV/Structure.agda b/src/CBPV/Structure.agda
new file mode 100644
index 0000000..0f64b1c
--- /dev/null
+++ b/src/CBPV/Structure.agda
@@ -0,0 +1,648 @@
+module CBPV.Structure where
+
+open import CBPV.Context
+open import CBPV.Family
+open import CBPV.Type
+
+open import Data.List using (List)
+open import Data.List.Relation.Unary.All using (All; map)
+
+open import Function.Base using (_∘_; _$_)
+
+open import Relation.Binary.PropositionalEquality.Core
+
+private
+  variable
+    A A′ : ValType
+    B B′ : CompType
+    Γ Δ Θ : Context
+    x y z : Name
+
+-- Raw Bundles ----------------------------------------------------------------
+
+record RawMonoid : Set₁ where
+  field
+    Val  : ValFamily
+    Comp : CompFamily
+    var  : Var ⇾ᵛ Val
+    subᵛ : Val ⇾ᵛ Val ^ᵛ Val
+    subᶜ : Comp ⇾ᶜ Comp ^ᶜ Val
+
+  renᵛ : Val ⇾ᵛ □ᵛ Val
+  renᵛ v ρ = subᵛ v (ρ ⨾ var)
+
+  renᶜ : Comp ⇾ᶜ □ᶜ Comp
+  renᶜ c ρ = subᶜ c (ρ ⨾ var)
+
+  lift : (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) → Γ ++ Θ ~[ Val ]↝ Δ ++ Θ
+  lift Θ σ = copair (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var)
+
+  lift-left :
+    (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) (i : VarPos x A Γ) →
+    lookup (lift Θ σ) (weaklPos Θ i) ≡ renᵛ (lookup σ i) (weakl Θ)
+  lift-left Θ σ i =
+    begin
+      lookup (lift Θ σ) (weaklPos Θ i)
+    ≡⟨ copair-left {V = Val} {Δ = Θ} (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var) i ⟩
+      lookup (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) i
+    ≡⟨ lookup-⨾ σ (λ ◌ → renᵛ ◌ (weakl Θ)) i ⟩
+      renᵛ (lookup σ i) (weakl Θ)
+    ∎
+    where open ≡-Reasoning
+
+record RawAlgebra : Set₁ where
+  infixr 1 have_be_ drop_then_ split_then_ bind_to_ push_then_
+  infixr 1 have_be[_]_ split_then[_,_]_ bind_to[_]_
+  infix 1 case_of_or_
+  infix 1 case_of[_]_or[_]_
+  field
+    monoid : RawMonoid
+
+  open RawMonoid monoid public
+
+  field
+    have_be_ : Val A ⇾ δᶜ [< x :- A ] Comp B ⇒ Comp B
+    thunk : Comp B ⇾ Val (U B)
+    force : Val (U B) ⇾ Comp B
+    point : Val 𝟙 Γ
+    drop_then_ : Val 𝟙 ⇾ Comp B ⇒ Comp B
+    ⟨_,_⟩ : Val A ⇾ Val A′ ⇒ Val (A × A′)
+    split_then_ : Val (A × A′) ⇾ δᶜ [< x :- A , y :- A′ ] Comp B ⇒ Comp B
+    inl : Val A ⇾ Val (A + A′)
+    inr : Val A′ ⇾ Val (A + A′)
+    case_of_or_ : Val (A + A′) ⇾ δᶜ [< x :- A ] Comp B ⇒ δᶜ [< y :- A′ ] Comp B ⇒ Comp B
+    ret : Val A ⇾ Comp (F A)
+    bind_to_ : Comp (F A) ⇾ δᶜ [< x :- A ] Comp B ⇒ Comp B
+    ⟪_,_⟫ : Comp B ⇾ Comp B′ ⇒ Comp (B × B′)
+    fst : Comp (B × B′) ⇾ Comp B
+    snd : Comp (B × B′) ⇾ Comp B′
+    pop : δᶜ [< x :- A ] Comp B ⇾ Comp (A ⟶ B)
+    push_then_ : Val A ⇾ Comp (A ⟶ B) ⇒ Comp B
+
+  have_be[_]_ : Val A Γ → (x : Name) → δᶜ [< x :- A ] Comp B Γ → Comp B Γ
+  have v be[ x ] c = have v be c
+
+  split_then[_,_]_ : Val (A × A′) Γ → (x y : Name) → δᶜ [< x :- A , y :- A′ ] Comp B Γ → Comp B Γ
+  split v then[ x , y ] c = split v then c
+
+  case_of[_]_or[_]_ :
+    Val (A + A′) Γ →
+    (x : Name) → δᶜ [< x :- A ] Comp B Γ →
+    (y : Name) → δᶜ [< y :- A′ ] Comp B Γ →
+    Comp B Γ
+  case v of[ x ] c or[ y ] d = case v of c or d
+
+  bind_to[_]_ : Comp (F A) Γ → (x : Name) → δᶜ [< x :- A ] Comp B Γ → Comp B Γ
+  bind c to[ x ] d = bind c to d
+
+  pop[_] : (x : Name) → δᶜ [< x :- A ] Comp B ⇾ Comp (A ⟶ B)
+  pop[ x ] c = pop c
+
+open RawAlgebra
+
+record RawCompExtension
+  (A : RawAlgebra)
+  (Θ : List ValType) (Ψ : List CompType) (T : CompType) : Set₁
+  where
+  field
+    X : RawAlgebra
+    staᵛ : A .Val ⇾ᵛ X .Val
+    staᶜ : A .Comp ⇾ᶜ X .Comp
+    dyn  : All (λ A → X .Val A Γ) Θ → All (λ B → X .Comp B Γ) Ψ → X .Comp T Γ
+
+record RawValExtension
+  (A : RawAlgebra)
+  (Θ : List ValType) (Ψ : List CompType) (T : ValType) : Set₁
+  where
+  field
+    X : RawAlgebra
+    staᵛ : A .Val ⇾ᵛ X .Val
+    staᶜ : A .Comp ⇾ᶜ X .Comp
+    dyn  : All (λ A → X .Val A Γ) Θ → All (λ B → X .Comp B Γ) Ψ → X .Val T Γ
+
+record RawFreeCompExtension
+  (A : RawAlgebra)
+  (Θ : List ValType) (Ψ : List CompType) (T : CompType) : Set₁
+  where
+  field
+    extension : RawCompExtension A Θ Ψ T
+
+  open RawCompExtension
+
+  field
+    evalᵛ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Val ⇾ᵛ ext .X .Val
+    evalᶜ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Comp ⇾ᶜ ext .X .Comp
+
+record RawFreeValExtension
+  (A : RawAlgebra)
+  (Θ : List ValType) (Ψ : List CompType) (T : ValType) : Set₁
+  where
+  field
+    extension : RawValExtension A Θ Ψ T
+
+  open RawValExtension
+
+  field
+    evalᵛ : (ext : RawValExtension A Θ Ψ T) → extension .X .Val ⇾ᵛ ext .X .Val
+    evalᶜ : (ext : RawValExtension A Θ Ψ T) → extension .X .Comp ⇾ᶜ ext .X .Comp
+
+-- Structures -----------------------------------------------------------------
+
+record IsMonoid (M : RawMonoid) : Set where
+  private module M = RawMonoid M
+  field
+    subᵛ-var : (i : Var A Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ (M.var i) σ ≡ σ ＠ i
+    renᵛ-id : (v : M.Val A Γ) → M.renᵛ v id ≡ v
+    subᵛ-assoc :
+      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) (ς : Δ ~[ M.Val ]↝ Θ) →
+      M.subᵛ (M.subᵛ v σ) ς ≡ M.subᵛ v (σ ⨾ λ ◌ → M.subᵛ ◌ ς)
+    renᶜ-id : (c : M.Comp B Γ) → M.renᶜ c id ≡ c
+    subᶜ-assoc :
+      (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) (ς : Δ ~[ M.Val ]↝ Θ) →
+      M.subᶜ (M.subᶜ c σ) ς ≡ M.subᶜ c (σ ⨾ λ ◌ → M.subᵛ ◌ ς)
+
+  open ≡-Reasoning
+
+  renᵛ-var : (i : Var A Γ) (ρ : Γ ↝ Δ) → M.renᵛ (M.var i) ρ ≡ M.var (ρ ＠ i)
+  renᵛ-var i ρ = begin
+    M.renᵛ (M.var i) ρ ≡⟨ subᵛ-var i (ρ ⨾ M.var) ⟩
+    (ρ ⨾ M.var) ＠ i   ≡⟨ ＠-⨾ ρ M.var i ⟩
+    M.var (ρ ＠ i)     ∎
+
+  subᵛ-renᵛ :
+    (v : M.Val A Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) →
+    M.subᵛ (M.renᵛ v ρ) σ ≡ M.subᵛ v (ρ ⨾ (σ ＠_))
+  subᵛ-renᵛ v ρ σ = begin
+    M.subᵛ (M.renᵛ v ρ) σ                   ≡⟨ subᵛ-assoc v (ρ ⨾ M.var) σ ⟩
+    M.subᵛ v (ρ ⨾ M.var ⨾ λ ◌ → M.subᵛ ◌ σ) ≡⟨ cong (M.subᵛ v) (⨾-assoc ρ M.var (λ ◌ → M.subᵛ ◌ σ)) ⟩
+    M.subᵛ v (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ cong (M.subᵛ v) (⨾-cong ρ (λ v → subᵛ-var v σ)) ⟩
+    M.subᵛ v (ρ ⨾ (σ ＠_))                  ∎
+
+  subᶜ-renᶜ :
+    (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) →
+    M.subᶜ (M.renᶜ c ρ) σ ≡ M.subᶜ c (ρ ⨾ (σ ＠_))
+  subᶜ-renᶜ c ρ σ = begin
+    M.subᶜ (M.renᶜ c ρ) σ                   ≡⟨ subᶜ-assoc c (ρ ⨾ M.var) σ ⟩
+    M.subᶜ c (ρ ⨾ M.var ⨾ λ ◌ → M.subᵛ ◌ σ) ≡⟨ cong (M.subᶜ c) (⨾-assoc ρ M.var (λ ◌ → M.subᵛ ◌ σ)) ⟩
+    M.subᶜ c (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ cong (M.subᶜ c) (⨾-cong ρ (λ v → subᵛ-var v σ)) ⟩
+    M.subᶜ c (ρ ⨾ (σ ＠_))                  ∎
+
+  private
+    lemma :
+      (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
+      (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡ (ρ ⨾ (ϱ ＠_) ⨾ M.var)
+    lemma ρ ϱ = begin
+      (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡⟨ ⨾-assoc ρ M.var (λ ◌ → M.renᵛ ◌ ϱ) ⟩
+      (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ ⨾-cong ρ (λ v → renᵛ-var v ϱ) ⟩
+      (ρ ⨾ λ ◌ → M.var (ϱ ＠ ◌))     ≡˘⟨ ⨾-assoc ρ (ϱ ＠_) M.var ⟩
+      (ρ ⨾ (ϱ ＠_) ⨾ M.var)          ∎
+
+  renᵛ-assoc :
+    (v : M.Val A Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
+    M.renᵛ (M.renᵛ v ρ) ϱ ≡ M.renᵛ v (ρ ⨾ (ϱ ＠_))
+  renᵛ-assoc v ρ ϱ = begin
+    M.renᵛ (M.renᵛ v ρ) ϱ                   ≡⟨ subᵛ-assoc v (ρ ⨾ M.var) (ϱ ⨾ M.var) ⟩
+    M.subᵛ v (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡⟨ cong (M.subᵛ v) (lemma ρ ϱ) ⟩
+    M.renᵛ v (ρ ⨾ (ϱ ＠_))                  ∎
+
+  renᶜ-assoc :
+    (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
+    M.renᶜ (M.renᶜ c ρ) ϱ ≡ M.renᶜ c (ρ ⨾ (ϱ ＠_))
+  renᶜ-assoc c ρ ϱ = begin
+    M.renᶜ (M.renᶜ c ρ) ϱ                   ≡⟨ subᶜ-assoc c (ρ ⨾ M.var) (ϱ ⨾ M.var) ⟩
+    M.subᶜ c (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡⟨ cong (M.subᶜ c) (lemma ρ ϱ) ⟩
+    M.renᶜ c (ρ ⨾ (ϱ ＠_))                  ∎
+
+  lift-ren :
+    (Θ : Context) (ρ : Γ ↝ Δ) →
+    M.lift Θ (ρ ⨾ M.var) ≡ copair (ρ ⨾ weaklF Θ) weakr ⨾ M.var
+  lift-ren Θ ρ = begin
+    M.lift Θ (ρ ⨾ M.var)                                          ≡⟨⟩
+    copair (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ (weakl Θ)) (weakr ⨾ M.var) ≡⟨ cong (λ ◌ → copair ◌ (weakr ⨾ M.var)) (⨾-assoc ρ M.var (λ ◌ → M.renᵛ ◌ (weakl Θ))) ⟩
+    copair (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) (weakl Θ)) (weakr ⨾ M.var) ≡⟨ cong (λ ◌ → copair ◌ (weakr ⨾ M.var)) (⨾-cong ρ (λ v → trans (renᵛ-var v (weakl Θ)) (cong M.var (＠-tabulate Var (weaklF Θ) v)))) ⟩
+    copair (ρ ⨾ λ ◌ → M.var (weaklF Θ ◌)) (weakr ⨾ M.var)         ≡˘⟨ cong (λ ◌ → copair ◌ (weakr ⨾ M.var)) (⨾-assoc ρ (weaklF Θ) M.var) ⟩
+    copair (ρ ⨾ weaklF Θ ⨾ M.var) (weakr ⨾ M.var)                 ≡⟨ copair-⨾ (ρ ⨾ weaklF Θ) weakr M.var ⟩
+    copair (ρ ⨾ weaklF Θ) weakr ⨾ M.var                           ∎
+
+record IsMonoidArrow
+  (M N : RawMonoid)
+  (fᵛ : RawMonoid.Val M ⇾ᵛ RawMonoid.Val N)
+  (fᶜ : RawMonoid.Comp M ⇾ᶜ RawMonoid.Comp N) : Set
+  where
+  private
+    module M = RawMonoid M
+    module N = RawMonoid N
+  field
+    ⟨var⟩ : (i : Var A Γ) → fᵛ (M.var i) ≡ N.var i
+    ⟨subᵛ⟩ :
+      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      fᵛ (M.subᵛ v σ) ≡ N.subᵛ (fᵛ v) (σ ⨾ fᵛ)
+    ⟨subᶜ⟩ :
+      (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      fᶜ (M.subᶜ c σ) ≡ N.subᶜ (fᶜ c) (σ ⨾ fᵛ)
+
+  open ≡-Reasoning
+
+  ⟨renᵛ⟩ : (v : M.Val A Γ) (ρ : Γ ↝ Δ) → fᵛ (M.renᵛ v ρ) ≡ N.renᵛ (fᵛ v) ρ
+  ⟨renᵛ⟩ v ρ = begin
+    fᵛ (M.renᵛ v ρ)                        ≡⟨ ⟨subᵛ⟩ v (ρ ⨾ M.var) ⟩
+    N.subᵛ (fᵛ v) (ρ ⨾ M.var ⨾ fᵛ)         ≡⟨ cong (N.subᵛ (fᵛ v)) (⨾-assoc ρ M.var fᵛ) ⟩
+    N.subᵛ (fᵛ v) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ cong (N.subᵛ (fᵛ v)) (⨾-cong ρ ⟨var⟩) ⟩
+    N.renᵛ (fᵛ v) ρ                        ∎
+
+  ⟨renᶜ⟩ : (c : M.Comp B Γ) (ρ : Γ ↝ Δ) → fᶜ (M.renᶜ c ρ) ≡ N.renᶜ (fᶜ c) ρ
+  ⟨renᶜ⟩ c ρ = begin
+    fᶜ (M.renᶜ c ρ)                        ≡⟨ ⟨subᶜ⟩ c (ρ ⨾ M.var) ⟩
+    N.subᶜ (fᶜ c) (ρ ⨾ M.var ⨾ fᵛ)         ≡⟨ cong (N.subᶜ (fᶜ c)) (⨾-assoc ρ M.var fᵛ) ⟩
+    N.subᶜ (fᶜ c) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ cong (N.subᶜ (fᶜ c)) (⨾-cong ρ ⟨var⟩) ⟩
+    N.renᶜ (fᶜ c) ρ                        ∎
+
+record IsAlgebra (M : RawAlgebra) : Set where
+  private module M = RawAlgebra M
+  field
+    isMonoid : IsMonoid M.monoid
+
+  open IsMonoid isMonoid public
+
+  field
+    sub-have :
+      (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.have v be c) σ ≡ (M.have M.subᵛ v σ be M.subᶜ c (M.lift [< x :- A ] σ))
+    sub-thunk :
+      (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᵛ (M.thunk c) σ ≡ M.thunk (M.subᶜ c σ)
+    sub-force :
+      (v : M.Val (U B) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.force v) σ ≡ M.force (M.subᵛ v σ)
+    sub-point : (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ M.point σ ≡ M.point
+    sub-drop :
+      (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.drop v then c) σ ≡ (M.drop M.subᵛ v σ then M.subᶜ c σ)
+    sub-pair :
+      (v : M.Val A Γ) (w : M.Val A′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᵛ M.⟨ v , w ⟩ σ ≡ M.⟨ M.subᵛ v σ , M.subᵛ w σ ⟩
+    sub-split :
+      (v : M.Val (A × A′) Γ) (c : δᶜ [< x :- A , y :- A′ ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.split v then c) σ ≡
+        (M.split M.subᵛ v σ then M.subᶜ c (M.lift [< x :- A , y :- A′ ] σ))
+    sub-inl :
+      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᵛ (M.inl {A′ = A′} v) σ ≡ M.inl (M.subᵛ v σ)
+    sub-inr :
+      (v : M.Val A′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᵛ (M.inr {A = A} v) σ ≡ M.inr (M.subᵛ v σ)
+    sub-case :
+      (v : M.Val (A + A′) Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) →
+      (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.case v of c or d) σ ≡
+        (M.case M.subᵛ v σ of M.subᶜ c (M.lift [< x :- A ] σ) or M.subᶜ d (M.lift [< y :- A′ ] σ))
+    sub-ret :
+      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.ret v) σ ≡ M.ret (M.subᵛ v σ)
+    sub-bind :
+      (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.bind c to d) σ ≡ (M.bind M.subᶜ c σ to M.subᶜ d (M.lift [< x :- A ] σ))
+    sub-bundle :
+      (c : M.Comp B Γ) (d : M.Comp B′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ M.⟪ c , d ⟫ σ ≡ M.⟪ M.subᶜ c σ , M.subᶜ d σ ⟫
+    sub-fst :
+      (c : M.Comp (B × B′) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.fst c) σ ≡ M.fst (M.subᶜ c σ)
+    sub-snd :
+      (c : M.Comp (B × B′) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.snd c) σ ≡ M.snd (M.subᶜ c σ)
+    sub-pop :
+      (c : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.pop c) σ ≡ M.pop (M.subᶜ c (M.lift [< x :- A ] σ))
+    sub-push :
+      (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      M.subᶜ (M.push v then c) σ ≡ (M.push M.subᵛ v σ then M.subᶜ c σ)
+
+  open ≡-Reasoning
+
+  ren-have :
+    (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.have v be c) ρ ≡ (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x))
+  ren-have {x = x} v c ρ =
+    begin
+      M.renᶜ (M.have v be c) ρ
+    ≡⟨ sub-have v c (ρ ⨾ M.var) ⟩
+      (M.have M.renᵛ v ρ be M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var)))
+    ≡⟨ cong (λ ◌ → M.have M.renᵛ v ρ be M.subᶜ c ◌) (lift-ren [< x :- _ ] ρ) ⟩
+      (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x))
+    ∎
+
+  ren-thunk :
+    (c : M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᵛ (M.thunk c) ρ ≡ M.thunk (M.renᶜ c ρ)
+  ren-thunk c ρ = sub-thunk c (ρ ⨾ M.var)
+
+  ren-force :
+    (v : M.Val (U B) Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.force v) ρ ≡ M.force (M.renᵛ v ρ)
+  ren-force c ρ = sub-force c (ρ ⨾ M.var)
+
+  ren-point : (ρ : Γ ↝ Δ) → M.renᵛ M.point ρ ≡ M.point
+  ren-point ρ = sub-point (ρ ⨾ M.var)
+
+  ren-drop :
+    (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.drop v then c) ρ ≡ (M.drop M.renᵛ v ρ then M.renᶜ c ρ)
+  ren-drop v c ρ = sub-drop v c (ρ ⨾ M.var)
+
+  ren-pair :
+    (v : M.Val A Γ) (w : M.Val A′ Γ) (ρ : Γ ↝ Δ) →
+    M.renᵛ M.⟨ v , w ⟩ ρ ≡ M.⟨ M.renᵛ v ρ , M.renᵛ w ρ ⟩
+  ren-pair v w ρ = sub-pair v w (ρ ⨾ M.var)
+
+  ren-split :
+    (v : M.Val (A × A′) Γ) (c : δᶜ [< x :- A , y :- A′ ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.split v then c) ρ ≡
+    ( M.split M.renᵛ v ρ
+      then[ x , y ] M.renᶜ c (ρ ⨾ (ThereVar ∘ ThereVar) :< x ↦ %% x :< y ↦ %% y)
+    )
+  ren-split {x = x} {y = y} v c ρ =
+    begin
+      M.renᶜ (M.split v then c) ρ
+    ≡⟨ sub-split v c (ρ ⨾ M.var) ⟩
+      (M.split M.subᵛ v (ρ ⨾ M.var) then M.subᶜ c (M.lift [< x :- _ , y :- _ ] (ρ ⨾ M.var)))
+    ≡⟨ cong (λ ◌ → M.split M.subᵛ v (ρ ⨾ M.var) then M.subᶜ c ◌) (lift-ren [< x :- _ , y :- _ ] ρ) ⟩
+      ( M.split M.renᵛ v ρ
+        then[ x , y ] M.renᶜ c (ρ ⨾ (ThereVar ∘ ThereVar) :< x ↦ %% x :< y ↦ %% y)
+      )
+    ∎
+
+  ren-inl :
+    (v : M.Val A Γ) (ρ : Γ ↝ Δ) →
+    M.renᵛ (M.inl {A′ = A′} v) ρ ≡ M.inl (M.renᵛ v ρ)
+  ren-inl v ρ = sub-inl v (ρ ⨾ M.var)
+
+  ren-inr :
+    (v : M.Val A′ Γ) (ρ : Γ ↝ Δ) →
+    M.renᵛ (M.inr {A = A} v) ρ ≡ M.inr (M.renᵛ v ρ)
+  ren-inr v ρ = sub-inr v (ρ ⨾ M.var)
+
+  ren-case :
+    (v : M.Val (A + A′) Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) →
+    (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.case v of c or d) ρ ≡
+    ( M.case M.renᵛ v ρ
+    of[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x)
+    or[ y ] M.renᶜ d (ρ ⨾ ThereVar :< y ↦ %% y))
+  ren-case {x = x} {y = y} v c d ρ =
+    begin
+      M.renᶜ (M.case v of c or d) ρ
+    ≡⟨ sub-case v c d (ρ ⨾ M.var) ⟩
+      ( M.case M.subᵛ v (ρ ⨾ M.var)
+      of M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var))
+      or M.subᶜ d (M.lift [< y :- _ ] (ρ ⨾ M.var)))
+    ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → M.case M.subᵛ v (ρ ⨾ M.var) of M.subᶜ c ◌ᵃ or M.subᶜ d ◌ᵇ)
+         (lift-ren [< x :- _ ] ρ)
+         (lift-ren [< y :- _ ] ρ) ⟩
+      ( M.case M.subᵛ v (ρ ⨾ M.var)
+      of[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x)
+      or[ y ] M.renᶜ d (ρ ⨾ ThereVar :< y ↦ %% y))
+    ∎
+
+  ren-ret :
+    (v : M.Val A Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.ret v) ρ ≡ M.ret (M.renᵛ v ρ)
+  ren-ret v ρ = sub-ret v (ρ ⨾ M.var)
+
+  ren-bind :
+    (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.bind c to d) ρ ≡ (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (ρ ⨾ ThereVar :< x ↦ %% x))
+  ren-bind {x = x} c d ρ =
+    begin
+      M.renᶜ (M.bind c to d) ρ
+    ≡⟨ sub-bind c d (ρ ⨾ M.var) ⟩
+      (M.bind M.renᶜ c ρ to M.subᶜ d (M.lift [< x :- _ ] (ρ ⨾ M.var)))
+    ≡⟨ cong (λ ◌ → M.bind M.renᶜ c ρ to M.subᶜ d ◌) (lift-ren [< x :- _ ] ρ) ⟩
+      (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (ρ ⨾ ThereVar :< x ↦ %% x))
+    ∎
+
+  ren-bundle :
+    (c : M.Comp B Γ) (d : M.Comp B′ Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ M.⟪ c , d ⟫ ρ ≡ M.⟪ M.renᶜ c ρ , M.renᶜ d ρ ⟫
+  ren-bundle c d ρ = sub-bundle c d (ρ ⨾ M.var)
+
+  ren-fst :
+    (c : M.Comp (B × B′) Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.fst c) ρ ≡ M.fst (M.renᶜ c ρ)
+  ren-fst c ρ = sub-fst c (ρ ⨾ M.var)
+
+  ren-snd :
+    (c : M.Comp (B × B′) Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.snd c) ρ ≡ M.snd (M.renᶜ c ρ)
+  ren-snd c ρ = sub-snd c (ρ ⨾ M.var)
+
+  ren-pop :
+    (c : δᶜ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.pop c) ρ ≡ M.pop[ x ] (M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x))
+  ren-pop {x = x} c ρ =
+    begin
+      M.renᶜ (M.pop c) ρ
+    ≡⟨ sub-pop c (ρ ⨾ M.var) ⟩
+      M.pop (M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var)))
+    ≡⟨ cong (M.pop ∘ M.subᶜ c) (lift-ren [< x :- _ ] ρ) ⟩
+      M.pop[ x ] (M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x))
+    ∎
+
+  ren-push :
+    (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.push v then c) ρ ≡ (M.push M.renᵛ v ρ then M.renᶜ c ρ)
+  ren-push v c ρ = sub-push v c (ρ ⨾ M.var)
+
+record IsModel (M : RawAlgebra) : Set where
+  private module M = RawAlgebra M
+  field
+    isAlgebra : IsAlgebra M
+
+  open IsAlgebra isAlgebra public
+
+  field
+    have-beta :
+      (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) →
+      (M.have v be c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    force-beta : (c : M.Comp B Γ) → M.force (M.thunk c) ≡ c
+    thunk-eta : (v : M.Val (U B) Γ) → M.thunk (M.force v) ≡ v
+    point-beta : (c : M.Comp B Γ) → (M.drop M.point then c) ≡ c
+    drop-eta :
+      (v : M.Val 𝟙 Γ) (c : δᶜ _ M.Comp B Γ) →
+      (M.drop v then M.subᶜ c (id ⨾ M.var :< x ↦ M.point)) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    pair-beta :
+      (v : M.Val A Γ) (w : M.Val A′ Γ) (c : δᶜ _ M.Comp B Γ) →
+      (M.split M.⟨ v , w ⟩ then c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v :< y ↦ w)
+    pair-eta :
+      (v : M.Val (A × A′) Γ) (c : δᶜ _ M.Comp B Γ) →
+        (M.split v then
+          M.subᶜ c
+            (  weakl [< y :- A , z :- A′ ] ⨾ M.var
+            :< x ↦ M.⟨ M.var (%% y) , M.var (%% z) ⟩
+            ))
+      ≡
+        M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    inl-beta :
+      (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) →
+      (M.case (M.inl v) of c or d) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    inr-beta :
+      (v : M.Val A′ Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ _ M.Comp B Γ) →
+      (M.case (M.inr v) of c or d) ≡ M.subᶜ d (id ⨾ M.var :< y ↦ v)
+    case-eta :
+      (v : M.Val (A + A′) Γ) (c : δᶜ _ M.Comp B Γ) →
+        ( M.case v
+          of M.subᶜ c (weakl [< y :- A ]  ⨾ M.var :< x ↦ M.inl (M.var $ %% y))
+          or M.subᶜ c (weakl [< z :- A′ ] ⨾ M.var :< x ↦ M.inr (M.var $ %% z)))
+      ≡
+        M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    ret-beta :
+      (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) →
+      (M.bind M.ret v to c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    bind-bind-comm :
+      (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp (F A′) Γ) (e : δᶜ [< y :- A′ ] M.Comp B Γ) →
+        (M.bind (M.bind c to d) to e)
+      ≡
+        (M.bind c to M.bind d to M.subᶜ e (weakl [< x :- _ , y :- _ ] ⨾ M.var :< y ↦ M.var (%% y)))
+    bind-fst-comm :
+      (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp (B × B′) Γ) →
+      (M.bind c to M.fst d) ≡ M.fst (M.bind c to d)
+    bind-snd-comm :
+      (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp (B × B′) Γ) →
+      (M.bind c to M.snd d) ≡ M.snd (M.bind c to d)
+    bind-push-comm :
+      (v : M.Val A Γ) (c : M.Comp (F A′) Γ) (d : δᶜ [< x :- A′ ] M.Comp (A ⟶ B) Γ) →
+      (M.push v then M.bind c to d) ≡ (M.bind c to M.push M.subᵛ v (weakl _ ⨾ M.var) then d)
+    fst-beta : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → M.fst M.⟪ c , d ⟫ ≡ c
+    snd-beta : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → M.snd M.⟪ c , d ⟫ ≡ d
+    bundle-eta : (c : M.Comp (B × B′) Γ) → M.⟪ M.fst c , M.snd c ⟫ ≡ c
+    push-beta :
+      (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) →
+      (M.push v then M.pop c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
+    push-eta :
+      (c : M.Comp (A ⟶ B) Γ) →
+      M.pop (M.push (M.var $ %% x) then M.subᶜ c (weakl [< x :- _ ] ⨾ M.var)) ≡ c
+
+record IsAlgebraArrow
+  (M N : RawAlgebra)
+  (fᵛ : M .Val ⇾ᵛ N .Val) (fᶜ : M .Comp ⇾ᶜ N .Comp) : Set
+  where
+  private
+    module M = RawAlgebra M
+    module N = RawAlgebra N
+  field
+    isMonoidArrow : IsMonoidArrow M.monoid N.monoid fᵛ fᶜ
+    ⟨have⟩ : (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) → fᶜ (M.have v be c) ≡ (N.have fᵛ v be fᶜ c)
+    ⟨thunk⟩ : (c : M.Comp B Γ) → fᵛ (M.thunk c) ≡ N.thunk (fᶜ c)
+    ⟨force⟩ : (v : M.Val (U B) Γ) → fᶜ (M.force v) ≡ N.force (fᵛ v)
+    ⟨point⟩ : fᵛ M.point ≡ N.point {Γ = Γ}
+    ⟨drop⟩ : (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) → fᶜ (M.drop v then c) ≡ (N.drop fᵛ v then fᶜ c)
+    ⟨pair⟩ : (v : M.Val A Γ) (w : M.Val A′ Γ) → fᵛ M.⟨ v , w ⟩ ≡ N.⟨ fᵛ v , fᵛ w ⟩
+    ⟨split⟩ :
+      (v : M.Val (A × A′) Γ) (c : δᶜ [< x :- A , y :- A′ ] M.Comp B Γ) →
+      fᶜ (M.split v then c) ≡ (N.split fᵛ v then fᶜ c)
+    ⟨inl⟩ : (v : M.Val A  Γ) → fᵛ {A + A′} (M.inl v) ≡ N.inl (fᵛ v)
+    ⟨inr⟩ : (v : M.Val A′ Γ) → fᵛ {A + A′} (M.inr v) ≡ N.inr (fᵛ v)
+    ⟨case⟩ :
+      (v : M.Val (A + A′) Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) →
+      fᶜ (M.case v of c or d) ≡ (N.case fᵛ v of fᶜ c or fᶜ d)
+    ⟨ret⟩ : (v : M.Val A Γ) → fᶜ (M.ret v) ≡ N.ret (fᵛ v)
+    ⟨bind⟩ : (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp B Γ) → fᶜ (M.bind c to d) ≡ (N.bind fᶜ c to fᶜ d)
+    ⟨bundle⟩ : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → fᶜ M.⟪ c , d ⟫ ≡ N.⟪ fᶜ c , fᶜ d ⟫
+    ⟨fst⟩ : (c : M.Comp (B × B′) Γ) → fᶜ (M.fst c) ≡ N.fst (fᶜ c)
+    ⟨snd⟩ : (c : M.Comp (B × B′) Γ) → fᶜ (M.snd c) ≡ N.snd (fᶜ c)
+    ⟨pop⟩ : (c : δᶜ [< x :- A ] M.Comp B Γ) → fᶜ (M.pop c) ≡ N.pop (fᶜ c)
+    ⟨push⟩ : (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) → fᶜ (M.push v then c) ≡ (N.push fᵛ v then fᶜ c)
+
+record IsCompExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawCompExtension A Θ Ψ T) : Set where
+  open RawCompExtension M
+  field
+    isModel : IsModel X
+    sta-arrow : IsAlgebraArrow A X staᵛ staᶜ
+    dyn-sub :
+      (vs : All (λ A → X .Val A Γ) Θ) (cs : All (λ A → X .Comp A Γ) Ψ) (σ : Γ ~[ X .Val ]↝ Δ) →
+      X .subᶜ (dyn vs cs) σ ≡ dyn (map (λ ◌ → X .subᵛ ◌ σ) vs) (map (λ ◌ → X .subᶜ ◌ σ) cs)
+
+record IsValExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawValExtension A Θ Ψ T) : Set where
+  open RawValExtension M
+  field
+    isModel : IsModel X
+    sta-arrow : IsAlgebraArrow A X staᵛ staᶜ
+    dyn-sub :
+      (vs : All (λ A → X .Val A Γ) Θ) (cs : All (λ A → X .Comp A Γ) Ψ) (σ : Γ ~[ X .Val ]↝ Δ) →
+      X .subᵛ (dyn vs cs) σ ≡ dyn (map (λ ◌ → X .subᵛ ◌ σ) vs) (map (λ ◌ → X .subᶜ ◌ σ) cs)
+
+record IsCompExtArrow {A Θ Ψ T} (M N : RawCompExtension A Θ Ψ T)
+  (fᵛ : RawCompExtension.X M .Val ⇾ᵛ RawCompExtension.X N .Val)
+  (fᶜ : RawCompExtension.X M .Comp ⇾ᶜ RawCompExtension.X N .Comp) : Set
+  where
+  private
+    module M = RawCompExtension M
+    module N = RawCompExtension N
+  field
+    isAlgebraArrow : IsAlgebraArrow M.X N.X fᵛ fᶜ
+    ⟨staᵛ⟩ : (v : A .Val A′ Γ) → fᵛ (M.staᵛ v) ≡ N.staᵛ v
+    ⟨staᶜ⟩ : (c : A .Comp B Γ) → fᶜ (M.staᶜ c) ≡ N.staᶜ c
+    ⟨dyn⟩ :
+      (vs : All (λ A → M.X .Val A Γ) Θ) (cs : All (λ A → M.X .Comp A Γ) Ψ) →
+      fᶜ (M.dyn vs cs) ≡ N.dyn (map fᵛ vs) (map fᶜ cs)
+
+record IsValExtArrow {A Θ Ψ T} (M N : RawValExtension A Θ Ψ T)
+  (fᵛ : RawValExtension.X M .Val ⇾ᵛ RawValExtension.X N .Val)
+  (fᶜ : RawValExtension.X M .Comp ⇾ᶜ RawValExtension.X N .Comp) : Set
+  where
+  private
+    module M = RawValExtension M
+    module N = RawValExtension N
+  field
+    isAlgebraArrow : IsAlgebraArrow M.X N.X fᵛ fᶜ
+    ⟨staᵛ⟩ : (v : A .Val A′ Γ) → fᵛ (M.staᵛ v) ≡ N.staᵛ v
+    ⟨staᶜ⟩ : (c : A .Comp B Γ) → fᶜ (M.staᶜ c) ≡ N.staᶜ c
+    ⟨dyn⟩ :
+      (vs : All (λ A → M.X .Val A Γ) Θ) (cs : All (λ A → M.X .Comp A Γ) Ψ) →
+      fᵛ (M.dyn vs cs) ≡ N.dyn (map fᵛ vs) (map fᶜ cs)
+
+record IsFreeCompExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeCompExtension A Θ Ψ T) : Set₁ where
+  private module M = RawFreeCompExtension M
+  open RawCompExtension
+  field
+    isExtension : IsCompExtension Aᴹ M.extension
+    eval-homo :
+      (ext : RawCompExtension A Θ Ψ T) →
+      IsCompExtArrow M.extension ext (M.evalᵛ ext) (M.evalᶜ ext)
+    eval-uniqueᵛ :
+      (ext : RawCompExtension A Θ Ψ T) →
+      (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) →
+      (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) →
+      IsCompExtArrow M.extension ext fᵛ fᶜ →
+      (v : M.extension .X .Val A′ Γ) →
+      fᵛ v ≡ M.evalᵛ ext v
+    eval-uniqueᶜ :
+      (ext : RawCompExtension A Θ Ψ T) →
+      (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) →
+      (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) →
+      IsCompExtArrow M.extension ext fᵛ fᶜ →
+      (c : M.extension .X .Comp B Γ) →
+      fᶜ c ≡ M.evalᶜ ext c
+
+record IsFreeValExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeValExtension A Θ Ψ T) : Set₁ where
+  private module M = RawFreeValExtension M
+  open RawValExtension
+  field
+    isExtension : IsValExtension Aᴹ M.extension
+    eval-homo :
+      (ext : RawValExtension A Θ Ψ T) →
+      IsValExtArrow M.extension ext (M.evalᵛ ext) (M.evalᶜ ext)
+    eval-uniqueᵛ :
+      (ext : RawValExtension A Θ Ψ T) →
+      (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) →
+      (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) →
+      IsValExtArrow M.extension ext fᵛ fᶜ →
+      (v : M.extension .X .Val A′ Γ) →
+      fᵛ v ≡ M.evalᵛ ext v
+    eval-uniqueᶜ :
+      (ext : RawValExtension A Θ Ψ T) →
+      (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) →
+      (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) →
+      IsValExtArrow M.extension ext fᵛ fᶜ →
+      (c : M.extension .X .Comp B Γ) →
+      fᶜ c ≡ M.evalᶜ ext c
diff --git a/src/CBPV/Term.agda b/src/CBPV/Term.agda
deleted file mode 100644
index ec05de4..0000000
--- a/src/CBPV/Term.agda
+++ /dev/null
@@ -1,309 +0,0 @@
-{-# 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
index 3d27e4e..2b52f54 100644
--- a/src/CBPV/Type.agda
+++ b/src/CBPV/Type.agda
@@ -1,27 +1,25 @@
-{-# OPTIONS --safe #-}
-
 module CBPV.Type where
 
-open import Data.List using (List)
+open import Data.List
+
+infixr 5 _⟶_ _⟶⋆_ _⟶′⋆_
 
 data ValType : Set
 data CompType : Set
 
-infix 8 U_ F_
-infixr 7 _×_
-infixr 6 _+_
-infixr 5 _⟶_
-
 data ValType where
-  U_  : CompType → ValType
-  𝟘   : ValType
+  U   : CompType → ValType
   𝟙   : ValType
-  _+_ : ValType → ValType → ValType
   _×_ : ValType → ValType → ValType
-  _⟶_ : ValType → ValType → ValType
+  _+_ : ValType → ValType → ValType
 
 data CompType where
-  F_  : ValType → CompType
-  𝟙   : CompType
+  F   : ValType → CompType
   _×_ : CompType → CompType → CompType
   _⟶_ : ValType → CompType → CompType
+
+_⟶⋆_ : List ValType → CompType → CompType
+Γ ⟶⋆ B = foldr _⟶_ B Γ
+
+_⟶′⋆_ : List CompType → CompType → CompType
+Γ ⟶′⋆ B = foldr (λ ◌ᵃ ◌ᵇ → U ◌ᵃ ⟶ ◌ᵇ) B Γ