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, 314 insertions, 280 deletions

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