WIP: concrete families

1 files changed, 648 insertions, 0 deletions

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