Update to stdlib 2.1.1 and other changes.main

I don't fully know what has changed because the changes are so old.

Doesn't yet compile due to not finishing proofs in `CBPV.Frex.Comp`.

1 files changed, 138 insertions, 141 deletions

diff --git a/src/CBPV/Structure.agda b/src/CBPV/Structure.agda
index 0f64b1c..1c51e0e 100644
--- a/src/CBPV/Structure.agda
+++ b/src/CBPV/Structure.agda
@@ -1,6 +1,6 @@
 module CBPV.Structure where
 
-open import CBPV.Context
+open import CBPV.Context hiding (map)
 open import CBPV.Family
 open import CBPV.Type
 
@@ -10,6 +10,7 @@ open import Data.List.Relation.Unary.All using (All; map)
 open import Function.Base using (_∘_; _$_)
 
 open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
 
 private
   variable
@@ -24,31 +25,23 @@ record RawMonoid : Set₁ where
   field
     Val  : ValFamily
     Comp : CompFamily
-    var  : Var ⇾ᵛ Val
-    subᵛ : Val ⇾ᵛ Val ^ᵛ Val
-    subᶜ : Comp ⇾ᶜ Comp ^ᶜ Val
+    var  : Var ⇾ᵗ Val
+    subᵛ : Val ⇾ᵗ Val ^ᵗ Val
+    subᶜ : Comp ⇾ᵗ Comp ^ᵗ Val
 
-  renᵛ : Val ⇾ᵛ □ᵛ Val
+  renᵛ : Val ⇾ᵗ □ᵗ Val
   renᵛ v ρ = subᵛ v (ρ ⨾ var)
 
-  renᶜ : Comp ⇾ᶜ □ᶜ Comp
+  renᶜ : Comp ⇾ᵗ □ᵗ Comp
   renᶜ c ρ = subᶜ c (ρ ⨾ var)
 
   lift : (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) → Γ ++ Θ ~[ Val ]↝ Δ ++ Θ
-  lift Θ σ = copair (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var)
+  lift Θ σ = σ ⨾ (λ ◌ → 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
+  lift-weakl :
+    (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) →
+    weakl Θ ⨾′ lift Θ σ ≈ σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)
+  lift-weakl Θ σ = copair-weakl {X = Val} {Δ = Θ} (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var)
 
 record RawAlgebra : Set₁ where
   infixr 1 have_be_ drop_then_ split_then_ bind_to_ push_then_
@@ -61,41 +54,41 @@ record RawAlgebra : Set₁ where
   open RawMonoid monoid public
 
   field
-    have_be_ : Val A ⇾ δᶜ [< x :- A ] Comp B ⇒ Comp B
+    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
+    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
+    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
+    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)
+    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_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_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 Γ →
+    (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_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 : Name) → δᵗ [< x :- A ] Comp B ⇾ Comp (A ⟶ B)
   pop[ x ] c = pop c
 
 open RawAlgebra
@@ -106,8 +99,8 @@ record RawCompExtension
   where
   field
     X : RawAlgebra
-    staᵛ : A .Val ⇾ᵛ X .Val
-    staᶜ : A .Comp ⇾ᶜ X .Comp
+    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
@@ -116,8 +109,8 @@ record RawValExtension
   where
   field
     X : RawAlgebra
-    staᵛ : A .Val ⇾ᵛ X .Val
-    staᶜ : A .Comp ⇾ᶜ X .Comp
+    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
@@ -130,8 +123,8 @@ record RawFreeCompExtension
   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
+    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)
@@ -143,14 +136,16 @@ record RawFreeValExtension
   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
+    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ᵛ-cong : (v : M.Val A Γ) → {σ ς : Γ ~[ M.Val ]↝ Δ} → σ ≈ ς → M.subᵛ v σ ≡ M.subᵛ v ς
+    subᶜ-cong : (c : M.Comp B Γ) → {σ ς : Γ ~[ M.Val ]↝ Δ} → σ ≈ ς → M.subᶜ c σ ≡ M.subᶜ c ς
     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 :
@@ -163,71 +158,64 @@ record IsMonoid (M : RawMonoid) : Set where
 
   open ≡-Reasoning
 
+  renᵛ-cong : (v : M.Val A Γ) → {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → M.renᵛ v ρ ≡ M.renᵛ v ϱ
+  renᵛ-cong v ρ≈ϱ = subᵛ-cong v (tabulate≈ $ cong M.var ∘ (ρ≈ϱ ＠_))
+
+  renᶜ-cong : (c : M.Comp B Γ) → {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → M.renᶜ c ρ ≡ M.renᶜ c ϱ
+  renᶜ-cong c ρ≈ϱ = subᶜ-cong c (tabulate≈ $ cong M.var ∘ (ρ≈ϱ ＠_))
+
   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 (ρ ⨾ (σ ＠_))
+    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 (ρ ⨾ (σ ＠_))                  ∎
+    M.subᵛ v (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ subᵛ-cong v (tabulate≈ $ λ i → subᵛ-var (ρ ＠ i) σ) ⟩
+    M.subᵛ v (ρ ⨾′ σ)                       ∎
 
   subᶜ-renᶜ :
     (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) →
-    M.subᶜ (M.renᶜ c ρ) σ ≡ M.subᶜ c (ρ ⨾ (σ ＠_))
+    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)          ∎
+    M.subᶜ c (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ subᶜ-cong c (tabulate≈ $ λ i → subᵛ-var (ρ ＠ i) σ) ⟩
+    M.subᶜ c (ρ ⨾′ σ)                       ∎
 
   renᵛ-assoc :
     (v : M.Val A Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
-    M.renᵛ (M.renᵛ v ρ) ϱ ≡ M.renᵛ v (ρ ⨾ (ϱ ＠_))
+    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 (ρ ⨾ (ϱ ＠_))                  ∎
+    M.subᵛ v (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ subᵛ-cong v (tabulate≈ $ λ i → renᵛ-var (ρ ＠ i) ϱ) ⟩
+    M.renᵛ v (ρ ⨾′ ϱ)                       ∎
 
   renᶜ-assoc :
     (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
-    M.renᶜ (M.renᶜ c ρ) ϱ ≡ M.renᶜ c (ρ ⨾ (ϱ ＠_))
+    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 (ρ ⨾ (ϱ ＠_))                  ∎
+    M.subᶜ c (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ subᶜ-cong c (tabulate≈ $ λ i → renᵛ-var (ρ ＠ i) ϱ) ⟩
+    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                           ∎
+    M.lift Θ (ρ ⨾ M.var) ≈ lift′ Θ ρ ⨾ M.var
+  lift-ren Θ ρ =
+    copair-unique {X = M.Val} _ _ _
+      (tabulate≈ $ λ i → begin
+        M.var ((ρ ⨾ weaklF Θ ∥ weakr) ＠ weakl Θ ＠ i) ≡⟨ cong M.var (copair-weakl {Δ = Θ} (ρ ⨾ weaklF Θ) weakr ＠ i) ⟩
+        M.var (weaklF Θ $ ρ ＠ i)                      ≡˘⟨ renᵛ-var (ρ ＠ i) (weakl Θ) ⟩
+        M.renᵛ (M.var $ ρ ＠ i) (weakl Θ)              ∎)
+      (tabulate≈ $ λ i → cong M.var (copair-weakr (ρ ⨾ weaklF Θ) weakr ＠ i))
 
 record IsMonoidArrow
   (M N : RawMonoid)
-  (fᵛ : RawMonoid.Val M ⇾ᵛ RawMonoid.Val N)
-  (fᶜ : RawMonoid.Comp M ⇾ᶜ RawMonoid.Comp N) : Set
+  (fᵛ : RawMonoid.Val M ⇾ᵗ RawMonoid.Val N)
+  (fᶜ : RawMonoid.Comp M ⇾ᵗ RawMonoid.Comp N) : Set
   where
   private
     module M = RawMonoid M
@@ -241,20 +229,33 @@ record IsMonoidArrow
       (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
       fᶜ (M.subᶜ c σ) ≡ N.subᶜ (fᶜ c) (σ ⨾ fᵛ)
 
+module MonArrow
+  {M N}
+  {fᵛ : RawMonoid.Val M ⇾ᵗ RawMonoid.Val N}
+  {fᶜ : RawMonoid.Comp M ⇾ᵗ RawMonoid.Comp N}
+  (arr : IsMonoidArrow M N fᵛ fᶜ)
+  (Nᵐ : IsMonoid N)
+  where
+
+  private
+    module M = RawMonoid M
+    module N where
+      open RawMonoid N public
+      open IsMonoid Nᵐ public
+
+  open IsMonoidArrow arr
   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.subᵛ (fᵛ v) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ N.subᵛ-cong (fᵛ v) (tabulate≈ $ λ i → ⟨var⟩ (ρ ＠ i)) ⟩
     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.subᶜ (fᶜ c) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ N.subᶜ-cong (fᶜ c) (tabulate≈ $ λ i → ⟨var⟩ (ρ ＠ i)) ⟩
     N.renᶜ (fᶜ c) ρ                        ∎
 
 record IsAlgebra (M : RawAlgebra) : Set where
@@ -266,7 +267,7 @@ record IsAlgebra (M : RawAlgebra) : Set where
 
   field
     sub-have :
-      (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
+      (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 ]↝ Δ) →
@@ -282,7 +283,7 @@ record IsAlgebra (M : RawAlgebra) : Set where
       (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 ]↝ Δ) →
+      (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 :
@@ -292,7 +293,7 @@ record IsAlgebra (M : RawAlgebra) : Set where
       (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 Γ) →
+      (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′ ] σ))
@@ -300,7 +301,7 @@ record IsAlgebra (M : RawAlgebra) : Set where
       (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 ]↝ Δ) →
+      (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 ]↝ Δ) →
@@ -312,7 +313,7 @@ record IsAlgebra (M : RawAlgebra) : Set where
       (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 ]↝ Δ) →
+      (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 ]↝ Δ) →
@@ -321,15 +322,15 @@ record IsAlgebra (M : RawAlgebra) : Set where
   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))
+    (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 (lift′ [< x :- A ] ρ))
   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))
+    ≡⟨ cong (λ ◌ → M.have M.renᵛ v ρ be ◌) (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) ⟩
+      (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (lift′ [< x :- _ ] ρ))
     ∎
 
   ren-thunk :
@@ -356,20 +357,16 @@ record IsAlgebra (M : RawAlgebra) : Set where
   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 Γ) (ρ : Γ ↝ Δ) →
+    (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)
-    )
+    (M.split M.renᵛ v ρ then[ x , y ] M.renᶜ c (lift′ [< x :- _ , 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)
-      )
+    ≡⟨ cong (λ ◌ → M.split M.subᵛ v (ρ ⨾ M.var) then ◌) (subᶜ-cong c $ lift-ren [< x :- _ , y :- _ ] ρ) ⟩
+      (M.split M.renᵛ v ρ then[ x , y ] M.renᶜ c (lift′ [< x :- _ , y :- _ ] ρ))
     ∎
 
   ren-inl :
@@ -383,12 +380,12 @@ record IsAlgebra (M : RawAlgebra) : Set where
   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 Γ) →
+    (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))
+    of[ x ] M.renᶜ c (lift′ [< x :- A ] ρ)
+    or[ y ] M.renᶜ d (lift′ [< y :- A′ ] ρ))
   ren-case {x = x} {y = y} v c d ρ =
     begin
       M.renᶜ (M.case v of c or d) ρ
@@ -396,12 +393,12 @@ record IsAlgebra (M : RawAlgebra) : Set where
       ( 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 :- _ ] ρ) ⟩
+    ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → M.case M.subᵛ v (ρ ⨾ M.var) of ◌ᵃ or ◌ᵇ)
+         (subᶜ-cong c $ lift-ren [< x :- _ ] ρ)
+         (subᶜ-cong d $ 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))
+      of[ x ] M.renᶜ c (lift′ [< x :- _ ] ρ)
+      or[ y ] M.renᶜ d (lift′ [< y :- _ ] ρ))
     ∎
 
   ren-ret :
@@ -410,15 +407,15 @@ record IsAlgebra (M : RawAlgebra) : Set where
   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))
+    (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 (lift′ [< x :- A ] ρ))
   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))
+    ≡⟨ cong (λ ◌ → M.bind M.renᶜ c ρ to ◌) (subᶜ-cong d $ lift-ren [< x :- _ ] ρ) ⟩
+      (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (lift′ [< x :- _ ] ρ))
     ∎
 
   ren-bundle :
@@ -437,15 +434,15 @@ record IsAlgebra (M : RawAlgebra) : Set where
   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))
+    (c : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
+    M.renᶜ (M.pop c) ρ ≡ M.pop[ x ] (M.renᶜ c (lift′ [< x :- A ] ρ))
   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))
+    ≡⟨ cong M.pop (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) ⟩
+      M.pop[ x ] (M.renᶜ c (lift′ [< x :- _ ] ρ))
     ∎
 
   ren-push :
@@ -462,19 +459,19 @@ record IsModel (M : RawAlgebra) : Set where
 
   field
     have-beta :
-      (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) →
+      (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 Γ) →
+      (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 Γ) →
+      (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 Γ) →
+      (v : M.Val (A × A′) Γ) (c : δᵗ _ M.Comp B Γ) →
         (M.split v then
           M.subᶜ c
             (  weakl [< y :- A , z :- A′ ] ⨾ M.var
@@ -483,40 +480,40 @@ record IsModel (M : RawAlgebra) : Set where
       ≡
         M.subᶜ c (id ⨾ M.var :< x ↦ v)
     inl-beta :
-      (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) →
+      (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 Γ) →
+      (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 Γ) →
+      (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 Γ) →
+      (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 Γ) →
+      (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′) Γ) →
+      (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′) Γ) →
+      (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) Γ) →
+      (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 Γ) →
+      (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) Γ) →
@@ -524,33 +521,33 @@ record IsModel (M : RawAlgebra) : Set where
 
 record IsAlgebraArrow
   (M N : RawAlgebra)
-  (fᵛ : M .Val ⇾ᵛ N .Val) (fᶜ : M .Comp ⇾ᶜ N .Comp) : Set
+  (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)
+    ⟨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 Γ) →
+      (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 Γ) →
+      (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)
+    ⟨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)
+    ⟨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
@@ -572,8 +569,8 @@ record IsValExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawValExtension A Θ �
       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
+  (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
@@ -587,8 +584,8 @@ record IsCompExtArrow {A Θ Ψ T} (M N : RawCompExtension A Θ Ψ T)
       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
+  (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
@@ -611,15 +608,15 @@ record IsFreeCompExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeCompExtension A
       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) →
+      (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) →
+      (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
@@ -634,15 +631,15 @@ record IsFreeValExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeValExtension A Θ
       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) →
+      (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) →
+      (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