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`.

4 files changed, 587 insertions, 656 deletions

diff --git a/src/CBPV/Context.agda b/src/CBPV/Context.agda
index d1aafc4..0ab5093 100644
--- a/src/CBPV/Context.agda
+++ b/src/CBPV/Context.agda
@@ -1,6 +1,7 @@
 module CBPV.Context where
 
 open import Data.Bool using (Bool)
+open import Data.List using (List; []; _∷_)
 open import Data.String using (String)
 import Data.String.Properties as String
 
@@ -15,23 +16,41 @@ abstract
   𝔪 : Name
   𝔪 = "𝔪"
 
-record Named : Set where
+record GenNamed (A : Set) : Set where
   constructor _:-_
   field
     name   : Name
-    ofType : ValType
+    ofType : A
 
-open Named public
+open GenNamed public
 
-infixl 5 _:<_ _++_
+Named : Set
+Named = GenNamed ValType
 
-data Context : Set where
-  [<]  : Context
-  _:<_ : Context → (ex : Named) → Context
+infixl 5 _:<_ _++_ _<><_
+
+data GenContext (A : Set) : Set where
+  [<]  : GenContext A
+  _:<_ : GenContext A → (ex : GenNamed A) → GenContext A
+
+Context : Set
+Context = GenContext ValType
+
+map : {A B : Set} → (A → B) → GenContext A → GenContext B
+map f [<] = [<]
+map f (Γ :< (n :- ty)) = map f Γ :< (n :- f ty)
+
+foldr : {A B : Set} → (A → B → B) → B → GenContext A → B
+foldr f z [<] = z
+foldr f z (Γ :< ex) = foldr f (f (ex .ofType) z) Γ
 
 pattern [<_:-_] x A = [<] :< (x :- A)
 pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
 
-_++_ : Context → Context → Context
+_++_ : {A : Set} → GenContext A → GenContext A → GenContext A
 Γ ++ [<] = Γ
 Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
+
+_<><_ : {A : Set} → GenContext A → List (GenNamed A) → GenContext A
+Γ <>< [] = Γ
+Γ <>< (x ∷ xs) = Γ :< x <>< xs
diff --git a/src/CBPV/Family.agda b/src/CBPV/Family.agda
index 4a64726..dd01777 100644
--- a/src/CBPV/Family.agda
+++ b/src/CBPV/Family.agda
@@ -1,362 +1,396 @@
 module CBPV.Family where
 
-open import Data.List as List using (List; []; _∷_; map)
+open import Data.List as List using (List; []; _∷_; foldr)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.Sum as ⊎ using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Unit using (⊤)
-open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_return_of_)
+open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_returning_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 Reflection.AST.Argument using (_⟨∷⟩_; _⟅∷⟆_)
+open import Reflection.AST.Term as Term using (_⋯⟅∷⟆_)
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
 open import Relation.Nullary using (yes; no)
 
-open import CBPV.Context
+import Data.Sum.Properties as ⊎
+
+open import CBPV.Context hiding (foldr)
 open import CBPV.Type
 
 -- Families and Morphisms -----------------------------------------------------
 
-infix 4 _⇾_ _⇾ᵛ_ _⇾ᶜ_
+infix 4 _⇾_ _⇾ᵗ_
+
+_-Family : Set → Set₁
+A -Family = GenContext A → Set
+
+_-Sorted-_-Family : Set → Set → Set₁
+A -Sorted- B -Family = A → B -Family
 
-Family : Set₁
-Family = Context → Set
+_-SortedFamily : Set → Set₁
+A -SortedFamily = A -Sorted- A -Family
 
 ValFamily : Set₁
-ValFamily = ValType → Family
+ValFamily = ValType -SortedFamily
 
 CompFamily : Set₁
-CompFamily = CompType → Family
+CompFamily = CompType -Sorted- ValType -Family
 
-_⇾_ : Family → Family → Set
-X ⇾ Y = {Γ : Context} → X Γ → Y Γ
+_⇾_ : {A : Set} → A -Family → A -Family → Set
+X ⇾ Y = {Γ : _} → X Γ → Y Γ
 
-_⇾ᵛ_ : ValFamily → ValFamily → Set
-V ⇾ᵛ W = {A : ValType} → V A ⇾ W A
-
-_⇾ᶜ_ : CompFamily → CompFamily → Set
-C ⇾ᶜ D = {B : CompType} → C B ⇾ D B
+_⇾ᵗ_ : {A B : Set} → A -Sorted- B -Family → A -Sorted- B -Family → Set
+V ⇾ᵗ W = {τ : _} → V τ ⇾ W τ
 
 -- Variables -------------------------------------------------------------------
 
 private
   variable
-    Γ Δ Θ Π : Context
-    A A′ : ValType
     x y : Name
-    V W X : ValFamily
+    A B C : Set
+    Γ Δ Θ Π : GenContext A
+    τ τ′ : A
+    X Y : A -Sorted- B -Family
 
-data VarPos (x : Name) (A : ValType) : Context → Set where
-  Here  : VarPos x A (Γ :< (x :- A))
-  There : VarPos x A Γ → VarPos x A (Γ :< (y :- A′))
+data VarPos (x : Name) (τ : A) : GenContext A → Set where
+  Here  : VarPos x τ (Γ :< (x :- τ))
+  There : VarPos x τ Γ → VarPos x τ (Γ :< (y :- τ′))
 
-weaklPos : (Δ : Context) → VarPos x A Γ → VarPos x A (Γ ++ Δ)
-weaklPos [<] i = i
-weaklPos (Δ :< (x :- A)) i = There (weaklPos Δ i)
+record Var (τ : A) (Γ : GenContext A) : Set where
+  constructor MkVar
+  field
+    name : Name
+    pos : VarPos name τ Γ
 
--- Reflection
+open Var public
 
-wknTerm : Term → Term
-wknTerm t = quote There ⟨ con ⟩ 5 ⋯⟅∷⟆ t ⟨∷⟩ []
+toVar : VarPos x τ Γ → Var τ Γ
+toVar pos = MkVar _ pos
 
-weaklTerm : Term → Term → Term
-weaklTerm Δ t = quote weaklPos ⟨ def ⟩ 3 ⋯⟅∷⟆ Δ ⟨∷⟩ t ⟨∷⟩ []
+-- Substitutions --------------------------------------------------------------
 
-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 Γ
+infixl 9 _⨾_ [_]_⨾_ _⨾′_ _≈⨾_ _≈⨾′_ _⨾≈_
+infixl 4 copair _∥ˡ_ _∥ʳ_
+infixl 5 _:<_↦_ subst-step
+infix 4 _~[_]↝_ _↝_ [_]_≈_ _≈_
 
--- 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 %%_
+record _~[_]↝_ (Γ : GenContext A) (X : A -Sorted- B -Family) (Δ : GenContext B) : Set where
+  constructor tabulate
+  infixr 8 _＠_
   field
-    name : Name
-    @(tactic searchVarPos Γ name) {pos} : VarPos name A Γ
+    _＠_ : Var τ Γ → X τ Δ
 
-open Var public
+open _~[_]↝_ public
 
-toVar : VarPos x A Γ → Var A Γ
-toVar pos = (%% _) {pos}
+_↝_ : GenContext A → GenContext A → Set
+Γ ↝ Δ = Γ ~[ Var ]↝ Δ
 
-ThereVar : Var A Γ → Var A (Γ :< (y :- A′))
-ThereVar i = toVar $ There (i .pos)
+[_]_＠_ : (X : A -Sorted- B -Family) → Γ ~[ X ]↝ Δ → Var τ Γ → X τ Δ
+[ X ] σ ＠ i = σ ＠ i
 
--- Substitutions --------------------------------------------------------------
+-- Equality
 
-infixl 9 _⨾_ [_]_⨾_
-infixr 8 _＠_
-infixl 5 _:<_↦_
-infix 4 Subst _↝_
+record _≈_ (σ ς : Γ ~[ X ]↝ Δ) : Set where
+  constructor tabulate≈
+  infixr 8 _＠_
+  field
+    _＠_ : (i : Var τ Γ) → σ ＠ i ≡ ς ＠ i
 
-data Subst (V : ValFamily) (Δ : Context) : Context → Set where
-  [<]     : Subst V Δ [<]
-  _:<_↦_ : Subst V Δ Γ → (x : Name) → V A Δ → Subst V Δ (Γ :< (x :- A))
+open _≈_ public
 
-syntax Subst V Δ Γ = Γ ~[ V ]↝ Δ
+[_]_≈_ : (X : A -SortedFamily) → Γ ~[ X ]↝ Δ → Γ ~[ X ]↝ Δ → Set
+[ V ] σ ≈ ς = σ ≈ ς
 
-_↝_ : Context → Context → Set
-Γ ↝ Δ = Γ ~[ Var ]↝ Δ
+trans≈ : {σ₁ σ₂ σ₃ : Γ ~[ X ]↝ Δ} → σ₁ ≈ σ₂ → σ₂ ≈ σ₃ → σ₁ ≈ σ₃
+trans≈ σ₁≈σ₂ σ₂≈σ₃ ＠ i = trans (σ₁≈σ₂ ＠ i) (σ₂≈σ₃ ＠ i)
+
+-- Combinators
+
+_⨾_ : Γ ~[ X ]↝ Δ → (∀ {τ} → X τ Δ → Y τ Θ) → Γ ~[ Y ]↝ Θ
+(σ ⨾ f) ＠ i = f (σ ＠ i)
 
-_⨾_ : Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ
-[<] ⨾ f = [<]
-(σ :< x ↦ v) ⨾ f = (σ ⨾ f) :< x ↦ f v
+_⨾′_ : Γ ↝ Δ → Δ ~[ X ]↝ Θ → Γ ~[ X ]↝ Θ
+(ρ ⨾′ f) ＠ i = f ＠ (ρ ＠ i)
 
-[_]_⨾_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ
+[_]_⨾_ : (X : A -SortedFamily) → Γ ~[ X ]↝ Δ → (∀ {τ} → X τ Δ → Y τ Θ) → Γ ~[ Y ]↝ Θ
 [ V ] σ ⨾ f = σ ⨾ f
 
-tabulate : (∀ {A} → Var A Γ → V A Δ) → Γ ~[ V ]↝ Δ
-tabulate {Γ = [<]} f = [<]
-tabulate {Γ = Γ :< (x :- A)} f = tabulate (f ∘ ThereVar) :< x ↦ f (toVar Here)
+_≈⨾_ : {σ ς : Γ ~[ X ]↝ Δ} → σ ≈ ς → (f : ∀ {τ} → X τ Δ → Y τ Θ) → [ Y ] (σ ⨾ f) ≈ (ς ⨾ f)
+(σ≈ς ≈⨾ f) ＠ i = cong f (σ≈ς ＠ i)
 
-lookup : Γ ~[ V ]↝ Δ → VarPos x A Γ → V A Δ
-lookup (σ :< x ↦ v) Here = v
-lookup (σ :< x ↦ v) (There i) = lookup σ i
+_≈⨾′_ : {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → (σ : Δ ~[ X ]↝ Θ) → ρ ⨾′ σ ≈ ϱ ⨾′ σ
+(ρ≈ϱ ≈⨾′ σ) ＠ i = cong (σ ＠_) (ρ≈ϱ ＠ i)
 
-_＠_ : Γ ~[ V ]↝ Δ → Var A Γ → V A Δ
-σ ＠ i = lookup σ (i .pos)
+_⨾≈_ : (ρ : Γ ↝ Δ) → {σ ς : Δ ~[ X ]↝ Θ} → σ ≈ ς → ρ ⨾′ σ ≈ ρ ⨾′ ς
+(ρ ⨾≈ σ≈ς) ＠ i = σ≈ς ＠ ρ ＠ i
 
-[_]_＠_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → Var A Γ → V A Δ
-[ V ] σ ＠ i = σ ＠ i
+-- Particular Substitutions
+
+-- id
 
 id : Γ ↝ Γ
 id = tabulate (λ x → x)
 
-weakrPos : VarPos x A Δ → VarPos x A (Γ ++ Δ)
+-- empty
+
+empty : [<] ~[ X ]↝ Γ
+empty = tabulate (λ ())
+
+-- weakr
+
+weakrPos : VarPos x τ Δ → VarPos x τ (Γ ++ Δ)
 weakrPos Here = Here
 weakrPos (There i) = There (weakrPos i)
 
-weakrF : Var A Δ → Var A (Γ ++ Δ)
+weakrF : Var τ Δ → Var τ (Γ ++ Δ)
 weakrF i = toVar $ weakrPos $ i .pos
 
 weakr : Δ ↝ Γ ++ Δ
 weakr = tabulate weakrF
 
-weaklF : (Δ : Context) → Var A Γ → Var A (Γ ++ Δ)
+-- weakl
+
+weaklPos : (Δ : GenContext A) → VarPos x τ Γ → VarPos x τ (Γ ++ Δ)
+weaklPos [<] i = i
+weaklPos (Δ :< (x :- τ)) i = There (weaklPos Δ i)
+
+weaklF : (Δ : GenContext A) → Var τ Γ → Var τ (Γ ++ Δ)
 weaklF Δ i = toVar $ weaklPos Δ $ i .pos
 
-weakl : (Δ : Context) → Γ ↝ Γ ++ Δ
+weakl : (Δ : GenContext A) → Γ ↝ Γ ++ Δ
 weakl Δ = tabulate (weaklF Δ)
 
-copair : Γ ~[ V ]↝ Θ → Δ ~[ V ]↝ Θ → Γ ++ Δ ~[ V ]↝ Θ
-copair σ [<] = σ
-copair σ (ς :< x ↦ v) = copair σ ς :< x ↦ v
+-- copair
+
+splitPos : (Δ : GenContext A) → VarPos x τ (Γ ++ Δ) → VarPos x τ Γ ⊎ VarPos x τ Δ
+splitPos [<] i = inj₁ i
+splitPos (Δ :< _) Here = inj₂ Here
+splitPos (Δ :< _) (There i) = ⊎.map₂ There (splitPos Δ i)
+
+splitF : (Δ : GenContext A) → Var τ (Γ ++ Δ) → Var τ Γ ⊎ Var τ Δ
+splitF Δ i = ⊎.map toVar toVar $ splitPos Δ $ i .pos
+
+copair : Γ ~[ X ]↝ Θ → Δ ~[ X ]↝ Θ → Γ ++ Δ ~[ X ]↝ Θ
+copair σ ς ＠ i = [ σ ＠_ , ς ＠_ ] $ splitF _ i
+
+syntax copair σ ς = σ ∥ ς
+
+copairₙ : {Γs : List (GenContext A)} → All (_~[ X ]↝ Θ) Γs → foldr _++_ [<] Γs ~[ X ]↝ Θ
+copairₙ [] ＠ ()
+copairₙ (σ ∷ σs) = σ ∥ copairₙ σs
 
-pull : (Δ Θ : Context) → Γ ++ Δ ++ Θ ↝ Γ ++ Θ ++ Δ
-pull Δ Θ =
-  copair {Δ = Θ}
-    (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr)
-    (weakr ⨾ (weakl Δ ＠_))
+-- singleton
+
+singleton : (x : Name) → X τ Γ → [< x :- τ ] ~[ X ]↝ Γ
+singleton x v ＠ (MkVar .x Here) = v
+
+-- snoc
+
+_:<_↦_ : Γ ~[ X ]↝ Δ → (x : Name) → X τ Δ → Γ :< (x :- τ) ~[ X ]↝ Δ
+σ :< x ↦ v = σ ∥ singleton x v
+
+-- weakening
+
+data Path {A : Set} : GenContext A → GenContext A → Set where
+  ⌞_⌟ : (Γ : GenContext A) → Path Γ Γ
+  _∥ˡ_ : Path Γ Δ → (Θ : GenContext A) → Path Γ (Δ ++ Θ)
+  _∥ʳ_ : (Θ : GenContext A) → Path Γ Δ → Path Γ (Θ ++ Δ)
+
+wkn : Path Γ Δ → Γ ↝ Δ
+wkn ⌞ Γ ⌟ = id
+wkn (path ∥ˡ Θ) = wkn path ⨾′ weakl Θ
+wkn (Θ ∥ʳ path) = wkn path ⨾′ weakr
+
+-- lift
+
+lift′ : (Θ : GenContext A) → Γ ↝ Δ → Γ ++ Θ ↝ Δ ++ Θ
+lift′ Θ ρ = ρ ⨾ weaklF Θ ∥ weakr
+
+-- weakening variables
+
+_↑_ : Var τ Γ → (Δ : GenContext A) → Var τ (Γ ++ Δ)
+i ↑ Δ = weakl Δ ＠ i
+
+_↑[_] : Var τ Γ → (x : Name) → Var τ (Γ :< (x :- τ′))
+i ↑[ x ] = i ↑ [< x :- _ ]
+
+_↑ : Var τ Γ → Var τ (Γ :< (x :- τ′))
+i ↑ = i ↑[ _ ]
+
+-- interaction with map
+
+map⁺Pos : {f : A → B} → Γ ~[ X ∘ f ]↝ Δ → VarPos x τ (map f Γ) → X τ Δ
+map⁺Pos {Γ = Γ :< (x :- τ)} σ Here = σ ＠ toVar Here
+map⁺Pos {Γ = Γ :< (x :- τ)} {X = X} σ (There i) = map⁺Pos {X = X} (tabulate (λ i → σ ＠ (i ↑))) i
+
+map⁺ : {f : A → B} → Γ ~[ X ∘ f ]↝ Δ → map f Γ ~[ X ]↝ Δ
+map⁺ σ ＠ i = map⁺Pos σ (i .pos)
+
+varPosMap⁺ : {f : A → B} → VarPos x τ Γ → VarPos x (f τ) (map f Γ)
+varPosMap⁺ Here = Here
+varPosMap⁺ (There i) = There (varPosMap⁺ i)
+
+varMap⁺ : {f : A → B} → Var τ Γ → Var (f τ) (map f Γ)
+varMap⁺ v = toVar (varPosMap⁺ $ v .pos)
+
+map⁻ : {f : A → B} → map f Γ ~[ X ]↝ Δ → Γ ~[ X ∘ f ]↝ Δ
+map⁻ σ ＠ i = σ ＠ varMap⁺ i
 
 -- 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
-
-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)
-  ∎
+subst-step :
+  {x : Name} {σ ς : Γ :< (x :- τ) ~[ X ]↝ Δ} →
+  weakl [< x :- τ ] ⨾′ σ ≈ weakl [< x :- τ ] ⨾′ ς →
+  σ ＠ MkVar x Here ≡ ς ＠ MkVar x Here →
+  σ ≈ ς
+subst-step σ↑≈ς↑ σ₀≡ς₀ ＠ MkVar x Here = σ₀≡ς₀
+subst-step σ↑≈ς↑ σ₀≡ς₀ ＠ MkVar x (There pos) = σ↑≈ς↑ ＠ MkVar x pos
+
+syntax subst-step {x = x} σ≈ς v≡w = σ≈ς :< x ⇒ v≡w
+
+-- weakl [<] is id
+
+weakl[<]≈id : weakl {Γ = Γ} [<] ≈ id
+weakl[<]≈id = tabulate≈ (λ i → refl)
+
+-- copair is coslice coproduct
+
+splitPos-weaklPos : (Δ : GenContext A) → (i : VarPos x τ Γ) → splitPos Δ (weaklPos Δ i) ≡ inj₁ i
+splitPos-weaklPos [<] i = refl
+splitPos-weaklPos (Δ :< _) i = cong (⊎.map₂ There) (splitPos-weaklPos Δ i)
+
+splitF-weaklF : (Δ : GenContext A) (i : Var τ Γ) → splitF Δ (weaklF Δ i) ≡ inj₁ i
+splitF-weaklF Δ i = cong (⊎.map toVar toVar) (splitPos-weaklPos Δ $ i .pos)
+
+copair-weakl :
+  (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) →
+  [ X ] weakl Δ ⨾′ (σ ∥ ς) ≈ σ
+copair-weakl σ ς ＠ i = cong [ σ ＠_ , ς ＠_ ] (splitF-weaklF _ i)
+
+splitPos-weakrPos :
+  (Γ : GenContext A) → (i : VarPos x τ Δ) →
+  splitPos {Γ = Γ} Δ (weakrPos i) ≡ inj₂ i
+splitPos-weakrPos Γ Here = refl
+splitPos-weakrPos Γ (There i) = cong (⊎.map₂ There) (splitPos-weakrPos Γ i)
+
+splitF-weakrF : (Γ : GenContext A) (i : Var τ Δ) → splitF Δ (weakrF i) ≡ inj₂ i
+splitF-weakrF Γ i = cong (⊎.map toVar toVar) (splitPos-weakrPos Γ $ i .pos)
+
+copair-weakr :
+  (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) →
+  [ X ] weakr {Γ = Γ} ⨾′ (σ ∥ ς) ≈ ς
+copair-weakr σ ς ＠ i = cong [ σ ＠_ , ς ＠_ ] (splitF-weakrF _ i)
+
+weakPos-splitPos :
+  (Δ : GenContext A) (i : VarPos x τ (Γ ++ Δ)) →
+  [ weaklPos Δ , weakrPos ] (splitPos Δ i) ≡ i
+weakPos-splitPos [<] i = refl
+weakPos-splitPos (Δ :< _) Here = refl
+weakPos-splitPos (Δ :< _) (There i) = begin
+  [ There ∘ weaklPos Δ , weakrPos ]′ (⊎.map₂ There $ splitPos Δ i) ≡⟨ ⊎.[,]-map (splitPos Δ i) ⟩
+  [ There ∘ weaklPos Δ , weakrPos ∘ There ]′ (splitPos Δ i)        ≡⟨⟩
+  [ There ∘ weaklPos Δ , There ∘ weakrPos ]′ (splitPos Δ i)        ≡˘⟨ ⊎.[,]-∘ There (splitPos Δ i) ⟩
+  There ([ weaklPos Δ , weakrPos ]′ $ splitPos Δ i)                ≡⟨ cong There (weakPos-splitPos Δ i) ⟩
+  There i                                                          ∎
+  where open ≡-Reasoning
+
+weakF-splitF : (Δ : GenContext A) (i : Var τ (Γ ++ Δ)) → [ weaklF Δ , weakrF ] (splitF Δ i) ≡ i
+weakF-splitF Δ i = begin
+  [ weaklF Δ , weakrF ] (splitF Δ i)                              ≡⟨ ⊎.[,]-map (splitPos Δ $ i .pos) ⟩
+  [ weaklF Δ ∘ toVar , weakrF ∘ toVar ] (splitPos Δ $ i .pos)     ≡⟨⟩
+  [ toVar ∘ weaklPos Δ , toVar ∘ weakrPos ] (splitPos Δ $ i .pos) ≡˘⟨ ⊎.[,]-∘ toVar (splitPos Δ $ i .pos) ⟩
+  toVar ([ weaklPos Δ , weakrPos ]′ $ splitPos Δ $ i .pos)        ≡⟨ cong toVar (weakPos-splitPos Δ (i .pos)) ⟩
+  toVar (i .pos)                                                  ≡⟨⟩
+  i                                                               ∎
+  where open ≡-Reasoning
+
+copair-unique :
+  {X : A -Sorted- B -Family} →
+  (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) (s : Γ ++ Δ ~[ X ]↝ Θ) →
+  (weakl Δ ⨾′ s ≈ σ) → (weakr ⨾′ s ≈ ς) →
+  (σ ∥ ς) ≈ s
+copair-unique {Δ = Δ} σ ς s wkl⨾s≈σ wkr⨾s≈ς ＠ i = begin
+  [ σ ＠_ , ς ＠_ ] (splitF Δ i)                         ≡˘⟨ ⊎.[,]-cong (wkl⨾s≈σ ＠_) (wkr⨾s≈ς ＠_) (splitF Δ i) ⟩
+  [ (weakl Δ ⨾′ s) ＠_ , (weakr ⨾′ s) ＠_ ] (splitF Δ i) ≡˘⟨ ⊎.[,]-∘ (s ＠_) (splitF Δ i) ⟩
+  s ＠ ([ weaklF Δ , weakrF ] $ splitF Δ i)              ≡⟨ cong (s ＠_) (weakF-splitF Δ i) ⟩
+  s ＠ i                                                 ∎
   where open ≡-Reasoning
 
 -- Special Families -----------------------------------------------------------
 
 infixr 5 _⇒_
 
-_⇒_ : Family → Family → Family
+_⇒_ : A -Family → A -Family → A -Family
 (X ⇒ Y) Γ = X Γ → Y Γ
 
-_^_ : Family → ValFamily → Family
-(X ^ V) Γ = {Δ : Context} → Γ ~[ V ]↝ Δ → X Δ
-
-_^ᵛ_ : ValFamily → ValFamily → ValFamily
-(W ^ᵛ V) A = W A ^ V
+_^_ : A -Family → B -Sorted- A -Family → B -Family
+(X ^ V) Γ = {Δ : GenContext _} → Γ ~[ V ]↝ Δ → X Δ
 
-_^ᶜ_ : CompFamily → ValFamily → CompFamily
-(C ^ᶜ V) B = C B ^ V
+_^ᵗ_ : A -Sorted- B -Family → C -Sorted- B -Family → A -Sorted- C -Family
+(W ^ᵗ V) τ = W τ ^ V
 
-□_ : Family → Family
+□_ : A -Family → A -Family
 □_ = _^ Var
 
-□ᵛ_ : ValFamily → ValFamily
-□ᵛ_ = _^ᵛ Var
+□ᵗ_ : A -Sorted- B -Family → A -Sorted- B -Family
+□ᵗ_ = _^ᵗ Var
 
-□ᶜ_ : CompFamily → CompFamily
-□ᶜ_ = _^ᶜ Var
-
-δ : Context → Family → Family
+δ : GenContext A → A -Family → A -Family
 δ Δ X Γ = X (Γ ++ Δ)
 
-δᵛ : Context → ValFamily → ValFamily
-δᵛ Δ V A = δ Δ (V A)
+δᵗ : GenContext B → A -Sorted- B -Family → A -Sorted- B -Family
+δᵗ Δ V τ = δ Δ (V τ)
+
+-- 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 _:<_) (_ ⟅∷⟆ Γ ⟨∷⟩ con (quote _:-_) (_ ⟅∷⟆ meta x _ ⟨∷⟩ ty ∷ []) ⟨∷⟩ [])) =
+  blockOnMeta x
+searchCtx wkn hole name (con (quote _:<_) (_ ⟅∷⟆ Γ ⟨∷⟩ con (quote _:-_) (_ ⟅∷⟆ x ⟨∷⟩ ty ∷ []) ⟨∷⟩ [])) =
+  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 (con (quote [<]) (_ ⟅∷⟆ [])) =
+  typeError (termErr name ∷ strErr " not in context." ∷ [])
+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 Γ ∷ [])
+
+searchVarPos : {A : Set} → GenContext A → Name → Term → TC ⊤
+searchVarPos Γ x hole =
+  do
+    Γ ← quoteTC Γ
+    x ← quoteTC x
+    case x returning (λ _ → TC ⊤) of λ
+      { (meta x _) → blockOnMeta x
+      ; _ → pure _
+      }
+    debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ [])
+    debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ [])
+    searchCtx (λ t → t) hole x Γ
 
-δᶜ : Context → CompFamily → CompFamily
-δᶜ Δ C B = δ Δ (C B)
+%%_ :
+  {A : Set} → {ty : A} → {Γ : GenContext A} →
+  (x : Name) → {@(tactic searchVarPos Γ x) pos : VarPos x ty Γ} → Var ty Γ
+%%_ x {pos} = MkVar x pos
diff --git a/src/CBPV/Frex/Comp.agda b/src/CBPV/Frex/Comp.agda
index 1ae5b4d..843ea52 100644
--- a/src/CBPV/Frex/Comp.agda
+++ b/src/CBPV/Frex/Comp.agda
@@ -11,6 +11,7 @@ module CBPV.Frex.Comp
 open import Function.Base using (_∘_; _$_)
 open import Function.Nary.NonDependent using (congₙ)
 open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
 
 open ≡-Reasoning
 
@@ -34,81 +35,54 @@ private
   𝔐 : Context
   𝔐 = [< 𝔪 :- ⟦T⟧ ]
 
--- Cast and Expand substitutions
+-- Helper
 
-cast : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ ~[ A.Val ]↝ Δ ++ 𝔐
+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      ∎
+cast≈ : {σ ς : Γ ~[ δᵗ 𝔐 A.Val ]↝ Δ} → σ ≈ ς → cast σ ≈ cast ς
+cast≈ σ≈ς ＠ i = σ≈ς ＠ i
 
 -- 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 σ)
+frexMonoid .Val = δᵗ 𝔐 A.Val
+frexMonoid .Comp = δᵗ 𝔐 A.Comp
+frexMonoid .var i = A.var (i ↑)
+frexMonoid .subᵛ v σ = A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexMonoid .subᶜ c σ = A.subᶜ c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
 
 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 .subᵛ-cong v σ≈ς = A.subᵛ-cong v (cast≈ σ≈ς :< 𝔪 ⇒ refl)
+frexIsMonoid .subᶜ-cong c σ≈ς = A.subᶜ-cong c (cast≈ σ≈ς :< 𝔪 ⇒ refl)
+frexIsMonoid .subᵛ-var i σ = A.subᵛ-var (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                                                 ∎
+  A.subᵛ v (tabulate (A.var ∘ _↑[ 𝔪 ]) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) ⟩
+  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 ς)))
+    A.subᵛ (A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))
+  ≡⟨ A.subᵛ-assoc v _ _ ⟩
+    A.subᵛ v ((cast σ :< 𝔪 ↦ A.var (%% 𝔪)) ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪)))
+  ≡⟨ A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ A.subᵛ-var (%% 𝔪) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) ⟩
+    A.subᵛ v (cast (σ ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) :< 𝔪 ↦ A.var (%% 𝔪))
   ∎
 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                                                 ∎
+  A.subᶜ c (tabulate (A.var ∘ _↑[ 𝔪 ]) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ A.subᶜ-cong c (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) ⟩
+  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 ς)))
+    A.subᶜ (A.subᶜ c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))
+  ≡⟨ A.subᶜ-assoc c _ _ ⟩
+    A.subᶜ c ((cast σ :< 𝔪 ↦ A.var (%% 𝔪)) ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪)))
+  ≡⟨ A.subᶜ-cong c (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ A.subᵛ-var (%% 𝔪) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) ⟩
+    A.subᶜ c (cast (σ ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) :< 𝔪 ↦ A.var (%% 𝔪))
   ∎
 
 open RawAlgebra
@@ -123,202 +97,109 @@ open RawAlgebra
     ; push_then_ to [_]push_then_
     )
 
+pull₁ : Γ :< x :- A′ :< 𝔪 :- ⟦T⟧ ↝ Γ :< 𝔪 :- ⟦T⟧ :< x :- A′
+pull₁ {x = x} = weakl _ :< x ↦ %% x :< 𝔪 ↦ %% 𝔪
+
+pull₂ : Γ :< x :- A′ :< y :- A′′ :< 𝔪 :- ⟦T⟧ ↝ Γ :< 𝔪 :- ⟦T⟧ :< x :- A′ :< y :- A′′
+pull₂ {x = x} {y = y} = weakl _ :< x ↦ %% x :< y ↦ %% y :< 𝔪 ↦ %% 𝔪
+
 frexAlgebra : RawAlgebra
 frexAlgebra .monoid = frexMonoid
-[ frexAlgebra ]have v be c = A.have v be A.renᶜ c (pull [< _ :- _ ] 𝔐)
+[ 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 ]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 [< _ :- _ ] 𝔐)
+  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 ]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 .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₀ : (v : X.Val A′ Γ) (ρ : Γ ↝ Δ) → X.renᵛ v ρ ≡ A.renᵛ v (lift′ [< 𝔪 :- ⟦T⟧ ] ρ)
+lemma₀ v ρ = A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl)
 
 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′ ] 𝔐)
+  (c : δᵗ [< x :- A′ ] X.Comp B Γ) (σ : Γ ~[ X.Val ]↝ Δ) →
+  A.subᶜ (A.renᶜ c pull₁) (A.lift [< x :- A′ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) ≡
+  A.renᶜ (X.subᶜ c (X.lift [< x :- A′ ] σ)) pull₁
 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 :- _ ] 𝔐)
+    A.subᶜ (A.renᶜ c pull₁) (A.lift [< x :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪)))
+  ≡⟨ A.subᶜ-renᶜ c _ _ ⟩
+    A.subᶜ c (pull₁ ⨾′ A.lift [< x :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪)))
+  ≡˘⟨ A.subᶜ-cong c
+       (  tabulate≈ (λ i →
+            begin
+              A.renᵛ
+                (A.subᵛ (σ ＠ i) (cast (weakl [< x :- _ , 𝔪 :- _ ] ⨾ A.var) :< 𝔪 ↦ A.var (%% 𝔪)))
+                pull₁
+            ≡⟨ A.subᵛ-assoc (σ ＠ i) _ _ ⟩
+              A.subᵛ (σ ＠ i)
+                ( (cast (weakl [< x :- _ , 𝔪 :- _ ] ⨾ A.var) :< 𝔪 ↦ A.var (%% 𝔪))
+                ⨾ λ ◌ → A.renᵛ ◌ pull₁)
+            ≡⟨ A.subᵛ-cong (σ ＠ i)
+                  (  tabulate≈ (λ i → A.renᵛ-var (i ↑ ↑) pull₁)
+                  :< 𝔪 ⇒ A.renᵛ-var (%% 𝔪) pull₁) ⟩
+              A.renᵛ (σ ＠ i) (weakl [< x :- _ ])
+            ∎)
+       :< x ⇒ A.renᵛ-var (%% x) pull₁
+       :< 𝔪 ⇒ (begin
+         A.renᵛ (A.var $ %% 𝔪) pull₁                       ≡⟨ A.renᵛ-var (%% 𝔪) pull₁ ⟩
+         A.var (%% 𝔪)                                      ≡˘⟨ A.renᵛ-var (MkVar 𝔪 Here) (weakl [< x :- _ ]) ⟩
+         A.renᵛ (A.var $ MkVar 𝔪 Here) (weakl [< x :- _ ]) ∎)
+       ) ⟩
+    A.subᶜ c
+      ( (cast (X.lift [< x :- _ ] σ) :< 𝔪 ↦ A.var (%% 𝔪))
+      ⨾ λ ◌ → A.renᵛ ◌ pull₁
+      )
+  ≡˘⟨ A.subᶜ-assoc c _ _ ⟩
+    A.renᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) pull₁
   ∎
--- 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 σ)
+frexIsAlgebra : IsAlgebra frexAlgebra
+frexIsAlgebra .isMonoid = frexIsMonoid
+frexIsAlgebra .sub-have v c σ =
+  begin
+    A.subᶜ
+      (A.have v be A.renᶜ c pull₁)
+      (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+  ≡⟨ A.sub-have v (A.renᶜ c pull₁) _ ⟩
+    (A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be
+      A.subᶜ
+        (A.renᶜ c pull₁)
+        (A.lift [< _ :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))))
+  ≡⟨ cong (λ ◌ → A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be ◌) (lemma₁ c σ) ⟩
+    (A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be
+      A.renᶜ (X.subᶜ c (X.lift [< _ :- _ ] σ)) pull₁)
+  ∎
+frexIsAlgebra .sub-thunk c σ = A.sub-thunk c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-force v σ = A.sub-force v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-point σ = A.sub-point (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-drop v c σ = A.sub-drop v c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-pair v w σ = A.sub-pair v w (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-split v c σ = {!A.sub-split!}
+frexIsAlgebra .sub-inl v σ = A.sub-inl v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-inr v σ = A.sub-inr v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-case = {!!}
+frexIsAlgebra .sub-ret v σ = A.sub-ret v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-bind = {!!}
+frexIsAlgebra .sub-bundle c d σ = A.sub-bundle c d (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-fst c σ = A.sub-fst c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-snd c σ = A.sub-snd c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
+frexIsAlgebra .sub-pop = {!!}
+frexIsAlgebra .sub-push v c σ = A.sub-push v c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))
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