From 61a568696914129aa203a03797be081fd542fcfd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 08:19:18 +0000
Subject: [PATCH 01/13] add : lemmas about balance factors at height 0

---
 src/Data/Tree/AVL/Height.agda | 24 +++++++++++++++++++-----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/Data/Tree/AVL/Height.agda b/src/Data/Tree/AVL/Height.agda
index fa50705952..4e03ee0307 100644
--- a/src/Data/Tree/AVL/Height.agda
+++ b/src/Data/Tree/AVL/Height.agda
@@ -11,6 +11,12 @@ module Data.Tree.AVL.Height where
 
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+
+private
+  variable
+    i j m n : ℕ
+
 
 ℕ₂ = Fin 2
 pattern 0# = zero
@@ -39,18 +45,26 @@ infix 4 _∼_⊔_
 -- absolute value of the balance factor is never more than 1.
 
 data _∼_⊔_ : ℕ → ℕ → ℕ → Set where
-  ∼+ : ∀ {n} →     n ∼ 1 + n ⊔ 1 + n
-  ∼0 : ∀ {n} →     n ∼ n     ⊔ n
-  ∼- : ∀ {n} → 1 + n ∼ n     ⊔ 1 + n
+  ∼+ :     n ∼ 1 + n ⊔ 1 + n
+  ∼0 :     n ∼ n     ⊔ n
+  ∼- : 1 + n ∼ n     ⊔ 1 + n
 
 -- Some lemmas.
 
-max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m
+max∼ : i ∼ j ⊔ m → m ∼ i ⊔ m
 max∼ ∼+ = ∼-
 max∼ ∼0 = ∼0
 max∼ ∼- = ∼0
 
-∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m
+∼max : i ∼ j ⊔ m → j ∼ m ⊔ m
 ∼max ∼+ = ∼0
 ∼max ∼0 = ∼0
 ∼max ∼- = ∼+
+
+0∼⊔ : 0 ∼ j ⊔ m → j ≡ m
+0∼⊔ ∼+ = refl
+0∼⊔ ∼0 = refl
+
+∼0⊔ : i ∼ 0 ⊔ m → i ≡ m
+∼0⊔ ∼- = refl
+∼0⊔ ∼0 = refl

From 669d9bc0983aaa1570489081465b0a389adeeea5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 08:24:56 +0000
Subject: [PATCH 02/13] add: `variable`s; tighten `import`s

---
 src/Data/Tree/AVL/Value.agda | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda
index 6305bd5c2c..91b05ee857 100644
--- a/src/Data/Tree/AVL/Value.agda
+++ b/src/Data/Tree/AVL/Value.agda
@@ -8,14 +8,20 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (_Respects_)
 
 module Data.Tree.AVL.Value {a ℓ} (S : Setoid a ℓ) where
 
 open import Data.Product.Base using (Σ; _,_)
-open import Level using (suc; _⊔_)
-import Function.Base as F
-open Setoid S renaming (Carrier to Key)
+open import Level using (Level; suc; _⊔_)
+import Function.Base as Function
+open import Relation.Binary.Definitions using (_Respects_)
+
+open Setoid S using (_≈_) renaming (Carrier to Key)
+
+private
+  variable
+    v : Level
+
 
 ------------------------------------------------------------------------
 -- A Value
@@ -26,23 +32,25 @@ record Value v : Set (a ⊔ ℓ ⊔ suc v) where
     family   : Key → Set v
     respects : family Respects _≈_
 
+open Value using (family)
+
 ------------------------------------------------------------------------
 -- A Key together with its value
 
-record K&_ {v} (V : Value v) : Set (a ⊔ v) where
+record K&_ (V : Value v) : Set (a ⊔ v) where
   constructor _,_
   field
     key   : Key
-    value : Value.family V key
+    value : family V key
 infixr 4 _,_
 open K&_ public
 
-module _ {v} {V : Value v} where
+module _ {V : Value v} where
 
-  toPair : K& V → Σ Key (Value.family V)
+  toPair : K& V → Σ Key (family V)
   toPair (k , v) = k , v
 
-  fromPair : Σ Key (Value.family V) → K& V
+  fromPair : Σ Key (family V) → K& V
   fromPair (k , v) = k , v
 
 ------------------------------------------------------------------------
@@ -50,6 +58,6 @@ module _ {v} {V : Value v} where
 
 -- The function `const` is defined using copatterns to prevent eager
 -- unfolding of the function in goal types.
-const : ∀ {v} → Set v → Value v
-Value.family   (const V) = F.const V
-Value.respects (const V) = F.const F.id
+const : Set v → Value v
+Value.family   (const V) = Function.const V
+Value.respects (const V) = Function.const F.id

From 8a4efef57bf5eb861164bc8f7d6a14e61eda1cd9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 08:26:17 +0000
Subject: [PATCH 03/13] fix: qualified module name `Function`

---
 src/Data/Tree/AVL/Value.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda
index 91b05ee857..f6662512d3 100644
--- a/src/Data/Tree/AVL/Value.agda
+++ b/src/Data/Tree/AVL/Value.agda
@@ -60,4 +60,4 @@ module _ {V : Value v} where
 -- unfolding of the function in goal types.
 const : Set v → Value v
 Value.family   (const V) = Function.const V
-Value.respects (const V) = Function.const F.id
+Value.respects (const V) = Function.const Function.id

From bab782252595163f2b379c6187b6828e22c37bec Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 09:23:00 +0000
Subject: [PATCH 04/13] refactor: introduce typedefs, remove parentheses,
 streamline functions definitions

---
 src/Data/Tree/AVL/Indexed.agda | 286 +++++++++++++++++----------------
 1 file changed, 147 insertions(+), 139 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 94d1b0782b..c6ac393cf8 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -16,17 +16,12 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.List.Base as List using (List)
-open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
-open import Function.Base as F hiding (const)
+open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _++_)
+open import Function.Base as Function hiding (const)
 open import Relation.Unary
 open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
-private
-  variable
-    l v : Level
-    A : Set l
-
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
@@ -37,7 +32,19 @@ open import Data.Tree.AVL.Value Eq.setoid public
 open import Data.Tree.AVL.Height public
 
 ------------------------------------------------------------------------
--- Definitions of the tree
+-- Now we have vocabulary in which to state things more cleanly
+
+private
+  variable
+    ℓ v w : Level
+    A : Set ℓ
+    k : Key
+    l m u : Key⁺
+    hˡ hʳ h : ℕ
+
+
+------------------------------------------------------------------------
+-- Definitions of the tree types
 
 -- The trees have three parameters/indices: a lower bound on the
 -- keys, an upper bound, and a height.
@@ -53,15 +60,45 @@ data Tree {v} (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) wh
          (bal : hˡ ∼ hʳ ⊔ h) →
          Tree V l u (suc h)
 
-module _ {v} {V : Value v} where
+-- Auxiliary type definitions for the types of insert, delete etc.
+
+module _ (V : Value v) (l u : Key⁺) where
+
+  Tree⁺ Tree⁻ : (h : ℕ) → Set (a ⊔ v ⊔ ℓ₂)
+  Tree⁺ h = ∃ λ i → Tree V l u (i ⊕ h)
+  Tree⁻ h = ∃ λ i → Tree V l u pred[ i ⊕ h ]
+
+  pattern leaf⁻ l<u = _ , leaf l<u  -- empty trees when passed as Tree⁻ V l u 0
+
+------------------------------------------------------------------------
+-- Functorial map over all values in the tree.
+
+module _ {V : Value v} {W : Value w}
+         (open Value using (family))
+         (f : family V ⊆ family W) where
+
+  map : Tree V l u h → Tree W l u h
+  map (leaf l<u)             = leaf l<u
+  map (node (k , v) l r bal) = node (k , f v) (map l) (map r) bal
+
+------------------------------------------------------------------------
+-- Properties relative to a fixed Value type family
+
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
   ordered : ∀ {l u n} → Tree V l u n → l <⁺ u
   ordered (leaf l<u)          = l<u
   ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
 
   private
-    Val = Value.family V
-    V≈  = Value.respects V
+  
+  -- This lemma justifies the use of `leaf⁻` pattern matches in code below
+
+    tree⁻0 : (t⁻ : Tree⁻ V l u 0) →
+             ∃ λ i → ∃ λ t → t⁻ ≡ (i , t) × t ≡ leaf (ordered t)
+    tree⁻0 t⁻@(leaf⁻ _) = _ , _ , refl , refl
+
+  -- Injectivity of constructors
 
   leaf-injective : ∀ {l u} {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
   leaf-injective refl = refl
@@ -77,6 +114,19 @@ module _ {v} {V : Value v} where
   -- See also node-injectiveˡ, node-injectiveʳ, and node-injective-bal
   -- in Data.Tree.AVL.Indexed.WithK.
 
+------------------------------------------------------------------------
+-- Constructions on trees
+
+  -- An empty tree.
+
+  empty : l <⁺ u → Tree V l u 0
+  empty = leaf
+
+  -- A singleton tree.
+
+  singleton : ∀ (k : Key) → Val k → l < k < u → Tree V l u 1
+  singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0
+
   -- Cast operations. Logarithmic in the size of the tree, if we don't
   -- count the time needed to construct the new proofs in the leaf
   -- cases. (The same kind of caveat applies to other operations
@@ -87,170 +137,139 @@ module _ {v} {V : Value v} where
   -- proof manipulation). However, note that this would not change the
   -- worst-case time complexity of the operations below (up to Θ).
 
-  castˡ : ∀ {l m u h} → l <⁺ m → Tree V m u h → Tree V l u h
-  castˡ {l} l<m (leaf m<u)         = leaf (trans⁺ l l<m m<u)
-  castˡ     l<m (node k mk ku bal) = node k (castˡ l<m mk) ku bal
+  castˡ : l <⁺ m → Tree V m u h → Tree V l u h
+  castˡ l<m (leaf m<u)         = leaf (trans⁺ _ l<m m<u)
+  castˡ l<m (node k mk ku bal) = node k (castˡ l<m mk) ku bal
 
-  castʳ : ∀ {l m u h} → Tree V l m h → m <⁺ u → Tree V l u h
-  castʳ {l} (leaf l<m)         m<u = leaf (trans⁺ l l<m m<u)
-  castʳ     (node k lk km bal) m<u = node k lk (castʳ km m<u) bal
+  castʳ : Tree V l m h → m <⁺ u → Tree V l u h
+  castʳ (leaf l<m)         m<u = leaf (trans⁺ _ l<m m<u)
+  castʳ (node k lk km bal) m<u = node k lk (castʳ km m<u) bal
 
   -- Various constant-time functions which construct trees out of
   -- smaller pieces, sometimes using rotation.
 
+  pattern node⁰ʳ k₁ t₁ k₂ t₂ t₃ = node k₁ t₁ (node k₂ t₂ t₃ ∼0) ∼0
+  pattern node⁰ˡ k₁ k₂ t₁ t₂ t₃ = node k₁ (node k₂ t₁ t₂ ∼0) t₃ ∼0
+
   pattern node⁺ k₁ t₁ k₂ t₂ t₃ bal = node k₁ t₁ (node k₂ t₂ t₃ bal) ∼+
 
-  joinˡ⁺ : ∀ {l u hˡ hʳ h} →
-           (k : K& V) →
-           (∃ λ i → Tree V l [ k .key ] (i ⊕ hˡ)) →
-           Tree V [ k .key ] u hʳ →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ (1 + h))
-  joinˡ⁺ k₂ (0# , t₁)                t₃ bal = (0# , node k₂ t₁ t₃ bal)
-  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼-)
-  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼+  = (0# , node k₂ t₁ t₃ ∼0)
-  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼-) t₅ ∼-  = (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
-  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼0) t₅ ∼-  = (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
+  joinˡ⁺ : ∀ kv → let k = [ kv . key ] in
+           Tree⁺ V l k hˡ → Tree V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u (suc h)
+  joinˡ⁺ k₂ (0# , t₁)                t₃ bal = 0# , node k₂ t₁ t₃ bal
+  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼0  = 1# , node k₂ t₁ t₃ ∼-
+  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼+  = 0# , node k₂ t₁ t₃ ∼0
+  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼-) t₅ ∼-  = 0# , node⁰ʳ k₂ t₁ k₄ t₃ t₅
+  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼0) t₅ ∼-  = 1# , node⁺ k₂ t₁ k₄ t₃ t₅ ∼-
   joinˡ⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-
-    = (0# , node k₄ (node k₂ t₁ t₃ (max∼ bal))
-                    (node k₆ t₅ t₇ (∼max bal))
-                    ∼0)
+    = 0# , node k₄ (node k₂ t₁ t₃ (max∼ bal)) (node k₆ t₅ t₇ (∼max bal)) ∼0
 
   pattern node⁻ k₁ k₂ t₁ t₂ bal t₃ = node k₁ (node k₂ t₁ t₂ bal) t₃ ∼-
 
-  joinʳ⁺ : ∀ {l u hˡ hʳ h} →
-           (k : K& V) →
-           Tree V l [ k .key ] hˡ →
-           (∃ λ i → Tree V [ k .key ] u (i ⊕ hʳ)) →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ (1 + h))
-  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = (0# , node k₂ t₁ t₃ bal)
-  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = (1# , node k₂ t₁ t₃ ∼+)
-  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = (0# , node k₂ t₁ t₃ ∼0)
-  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = (0# , node k₄ (node k₂ t₁ t₃ ∼0) t₅ ∼0)
-  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = (1# , node k₄ (node k₂ t₁ t₃ ∼+) t₅ ∼-)
+  joinʳ⁺ : ∀ kv → let k = [ kv . key ] in
+           Tree V l k hˡ → Tree⁺ V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u (suc h)
+  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = 0# , node k₂ t₁ t₃ bal
+  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = 1# , node k₂ t₁ t₃ ∼+
+  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = 0# , node k₂ t₁ t₃ ∼0
+  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = 0# , node⁰ˡ k₄ k₂ t₁ t₃ t₅
+  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = 1# , node⁻ k₄ k₂ t₁ t₃ ∼+ t₅
   joinʳ⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+
-    = (0# , node k₄ (node k₂ t₁ t₃ (max∼ bal))
-                    (node k₆ t₅ t₇ (∼max bal))
-                    ∼0)
-
-  joinˡ⁻ : ∀ {l u} hˡ {hʳ h} →
-           (k : K& V) →
-           (∃ λ i → Tree V l [ k .key ] pred[ i ⊕ hˡ ]) →
-           Tree V [ k .key ] u hʳ →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ h)
-  joinˡ⁻ zero    k₂ (0# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
-  joinˡ⁻ zero    k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
-  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼+  = joinʳ⁺ k₂ t₁ (1# , t₃) ∼+
-  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼+)
-  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼-  = (0# , node k₂ t₁ t₃ ∼0)
-  joinˡ⁻ (suc _) k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
-
-  joinʳ⁻ : ∀ {l u hˡ} hʳ {h} →
-           (k : K& V) →
-           Tree V l [ k .key ] hˡ →
-           (∃ λ i → Tree V [ k .key ] u pred[ i ⊕ hʳ ]) →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ h)
-  joinʳ⁻ zero    k₂ t₁ (0# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
-  joinʳ⁻ zero    k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
-  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼-  = joinˡ⁺ k₂ (1# , t₁) t₃ ∼-
-  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼0  = (1# , node k₂ t₁ t₃ ∼-)
-  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼+  = (0# , node k₂ t₁ t₃ ∼0)
-  joinʳ⁻ (suc _) k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
+    = 0# , node k₄ (node k₂ t₁ t₃ (max∼ bal)) (node k₆ t₅ t₇ (∼max bal)) ∼0
+
+  joinˡ⁻ : ∀ hˡ (kv : K& V) → let k = [ kv . key ] in
+           Tree⁻ V l k hˡ → Tree V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u h
+  joinˡ⁻ zero    k₂ (leaf⁻ l<k) t₃ bal = 1# , node k₂ (leaf l<k) t₃ bal
+  joinˡ⁻ (suc _) k₂ (0# , t₁)   t₃ ∼+  = joinʳ⁺ k₂ t₁ (1# , t₃) ∼+
+  joinˡ⁻ (suc _) k₂ (0# , t₁)   t₃ ∼0  = 1# , node k₂ t₁ t₃ ∼+
+  joinˡ⁻ (suc _) k₂ (0# , t₁)   t₃ ∼-  = 0# , node k₂ t₁ t₃ ∼0
+  joinˡ⁻ (suc _) k₂ (1# , t₁)   t₃ bal = 1# , node k₂ t₁ t₃ bal
+
+  joinʳ⁻ : ∀ hʳ (kv : K& V) → let k = [ kv . key ] in
+           Tree V l k hˡ → Tree⁻ V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u h
+  joinʳ⁻ zero    k₂ t₁ (leaf⁻ k<u) bal = 1# , node k₂ t₁ (leaf k<u) bal
+  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃)   ∼-  = joinˡ⁺ k₂ (1# , t₁) t₃ ∼-
+  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃)   ∼0  = 1# , node k₂ t₁ t₃ ∼-
+  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃)   ∼+  = 0# , node k₂ t₁ t₃ ∼0
+  joinʳ⁻ (suc _) k₂ t₁ (1# , t₃)   bal = 1# , node k₂ t₁ t₃ bal
 
   -- Extracts the smallest element from the tree, plus the rest.
   -- Logarithmic in the size of the tree.
 
-  headTail : ∀ {l u h} → Tree V l u (1 + h) →
-             ∃ λ (k : K& V) → l <⁺ [ k .key ] ×
-                            ∃ λ i → Tree V [ k .key ] u (i ⊕ h)
-  headTail (node k₁ (leaf l<k₁) t₂ ∼+) = (k₁ , l<k₁ , 0# , t₂)
-  headTail (node k₁ (leaf l<k₁) t₂ ∼0) = (k₁ , l<k₁ , 0# , t₂)
-  headTail (node {hˡ = suc _} k₃ t₁₂ t₄ bal) with headTail t₁₂
-  ... | (k₁ , l<k₁ , t₂) = (k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal)
+  headTail : Tree V l u (suc h) →
+             ∃ λ kv → let k = [ kv . key ] in l <⁺ k × Tree⁺ V k u h
+  headTail (node k₁ (leaf l<k₁) t₂ bal)
+    with refl ← 0∼⊔ bal                 = k₁ , l<k₁ , 0# , t₂
+  headTail (node k₃ t₁₂@(node _ _ _ _) t₄ bal)
+    using k₁ , l<k₁ , t₂ ← headTail t₁₂ = k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal
 
   -- Extracts the largest element from the tree, plus the rest.
   -- Logarithmic in the size of the tree.
 
-  initLast : ∀ {l u h} → Tree V l u (1 + h) →
-             ∃ λ (k : K& V) → [ k .key ] <⁺ u ×
-                            ∃ λ i → Tree V l [ k .key ] (i ⊕ h)
-  initLast (node k₂ t₁ (leaf k₂<u) ∼-) = (k₂ , k₂<u , (0# , t₁))
-  initLast (node k₂ t₁ (leaf k₂<u) ∼0) = (k₂ , k₂<u , (0# , t₁))
-  initLast (node {hʳ = suc _} k₂ t₁ t₃₄ bal) with initLast t₃₄
-  ... | (k₄ , k₄<u , t₃) = (k₄ , k₄<u , joinʳ⁻ _ k₂ t₁ t₃ bal)
+  initLast : Tree V l u (suc h) →
+             ∃ λ kv → let k = [ kv . key ] in k <⁺ u × Tree⁺ V l k h
+  initLast (node k₂ t₁ (leaf k₂<u) bal)
+    with refl ← ∼0⊔ bal                 = k₂ , k₂<u , 0# , t₁
+  initLast (node k₂ t₁ t₃₄@(node _ _ _ _) bal)
+    using k₄ , k₄<u , t₃ ← initLast t₃₄ = k₄ , k₄<u , joinʳ⁻ _ k₂ t₁ t₃ bal
 
   -- Another joining function. Logarithmic in the size of either of
   -- the input trees (which need to have almost equal heights).
 
-  join : ∀ {l m u hˡ hʳ h} →
-         Tree V l m hˡ → Tree V m u hʳ → (bal : hˡ ∼ hʳ ⊔ h) →
-         ∃ λ i → Tree V l u (i ⊕ h)
-  join t₁ (leaf m<u) ∼0 = (0# , castʳ t₁ m<u)
-  join t₁ (leaf m<u) ∼- = (0# , castʳ t₁ m<u)
-  join {hʳ = suc _} t₁ t₂₃ bal with headTail t₂₃
-  ... | (k₂ , m<k₂ , t₃) = joinʳ⁻ _ k₂ (castʳ t₁ m<k₂) t₃ bal
-
-  -- An empty tree.
-
-  empty : ∀ {l u} → l <⁺ u → Tree V l u 0
-  empty = leaf
-
-  -- A singleton tree.
-
-  singleton : ∀ {l u} (k : Key) → Val k → l < k < u → Tree V l u 1
-  singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0
+  join : Tree V l m hˡ → Tree V m u hʳ → hˡ ∼ hʳ ⊔ h → Tree⁺ V l u h
+  join t₁ (leaf m<u) bal
+    with refl ← ∼0⊔ bal                 = 0# , castʳ t₁ m<u
+  join t₁ t₂₃@(node _ _ _ _) bal
+    using k₂ , m<k₂ , t₃ ← headTail t₂₃ = joinʳ⁻ _ k₂ (castʳ t₁ m<k₂) t₃ bal
 
   -- Inserts a key into the tree, using a function to combine any
   -- existing value with the new value. Logarithmic in the size of the
   -- tree (assuming constant-time comparisons and a constant-time
   -- combining function).
 
-  insertWith : ∀ {l u h} (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
-               Tree V l u h → l < k < u →
-               ∃ λ i → Tree V l u (i ⊕ h)
-  insertWith k f (leaf l<u) l<k<u = (1# , singleton k (f nothing) l<k<u)
-  insertWith k f (node (k′ , v′) lp pu bal) (l<k , k<u) with compare k k′
-  ... | tri< k<k′ _ _ = joinˡ⁺ (k′ , v′) (insertWith k f lp (l<k , [ k<k′ ]ᴿ)) pu bal
-  ... | tri> _ _ k′<k = joinʳ⁺ (k′ , v′) lp (insertWith k f pu ([ k′<k ]ᴿ , k<u)) bal
-  ... | tri≈ _ k≈k′ _ = (0# , node (k′ , V≈ k≈k′ (f (just (V≈ (Eq.sym k≈k′) v′)))) lp pu bal)
+  insertWith : ∀ (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
+               Tree V l u h → l < k < u → Tree⁺ V l u h
+  insertWith k f (leaf l<u) l<k<u = 1# , singleton k (f nothing) l<k<u
+  insertWith k f (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k k′
+  ... | tri< k<k′ _ _ = joinˡ⁺ kv (insertWith k f lk (l<k , [ k<k′ ]ᴿ)) ku bal
+  ... | tri> _ _ k′<k = joinʳ⁺ kv lk (insertWith k f ku ([ k′<k ]ᴿ , k<u)) bal
+  ... | tri≈ _ k≈k′ _ = 0# , node (k′ , v′) lk ku bal
+        where v′ = respects k≈k′ (f (just (respects (Eq.sym k≈k′) v)))
 
   -- Inserts a key into the tree. If the key already exists, then it
   -- is replaced. Logarithmic in the size of the tree (assuming
   -- constant-time comparisons).
 
-  insert : ∀ {l u h} → (k : Key) → Val k → Tree V l u h → l < k < u →
-           ∃ λ i → Tree V l u (i ⊕ h)
-  insert k v = insertWith k (F.const v)
+  insert : ∀ k → Val k → Tree V l u h → l < k < u → Tree⁺ V l u h
+  insert k v = insertWith k (Function.const v)
 
   -- Deletes the key/value pair containing the given key, if any.
   -- Logarithmic in the size of the tree (assuming constant-time
   -- comparisons).
 
-  delete : ∀ {l u h} (k : Key) → Tree V l u h → l < k < u →
-           ∃ λ i → Tree V l u pred[ i ⊕ h ]
-  delete k (leaf l<u) l<k<u = (0# , leaf l<u)
-  delete k (node p@(k′ , v) lp pu bal) (l<k , k<u) with compare k′ k
-  ... | tri< k′<k _ _ = joinʳ⁻ _ p lp (delete k pu ([ k′<k ]ᴿ , k<u)) bal
-  ... | tri> _ _ k′>k = joinˡ⁻ _ p (delete k lp (l<k , [ k′>k ]ᴿ)) pu bal
-  ... | tri≈ _ k′≡k _ = join lp pu bal
+  delete : ∀ k → Tree V l u h → l < k < u → Tree⁻ V l u h
+  delete k (leaf l<u) l<k<u = 0# , leaf l<u
+  delete k (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k′ k
+  ... | tri< k′<k _ _ = joinʳ⁻ _ kv lk (delete k ku ([ k′<k ]ᴿ , k<u)) bal
+  ... | tri> _ _ k′>k = joinˡ⁻ _ kv (delete k lk (l<k , [ k′>k ]ᴿ)) ku bal
+  ... | tri≈ _ k′≡k _ = join lk ku bal
 
   -- Looks up a key. Logarithmic in the size of the tree (assuming
   -- constant-time comparisons).
 
-  lookup : ∀ {l u h} → Tree V l u h → (k : Key) → l < k < u → Maybe (Val k)
-  lookup (leaf _) k l<k<u = nothing
-  lookup (node (k′ , v) lk′ k′u _) k (l<k , k<u) with compare k′ k
-  ... | tri< k′<k _ _ = lookup k′u k ([ k′<k ]ᴿ , k<u)
-  ... | tri> _ _ k′>k = lookup lk′ k (l<k , [ k′>k ]ᴿ)
-  ... | tri≈ _ k′≡k _ = just (V≈ k′≡k v)
+  lookup : Tree V l u h → ∀ k → l < k < u → Maybe (Val k)
+  lookup (leaf _)                  k l<k<u       = nothing
+  lookup (node (k′ , v) lk ku _) k (l<k , k<u) with compare k′ k
+  ... | tri< k′<k _ _ = lookup ku k ([ k′<k ]ᴿ , k<u)
+  ... | tri> _ _ k′>k = lookup lk k (l<k , [ k′>k ]ᴿ)
+  ... | tri≈ _ k′≡k _ = just (respects k′≡k v)
 
   -- Converts the tree to an ordered list. Linear in the size of the
   -- tree.
 
-  foldr : ∀ {l u h} → (∀ {k} → Val k → A → A) → A → Tree V l u h → A
+  foldr : (∀ {k} → Val k → A → A) → A → Tree V l u h → A
   foldr cons nil (leaf l<u)             = nil
   foldr cons nil (node (_ , v) l r bal) = foldr cons (cons v (foldr cons nil r)) l
 
@@ -259,19 +278,8 @@ module _ {v} {V : Value v} where
   toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r
 
   toList : ∀ {l u h} → Tree V l u h → List (K& V)
-  toList t = toDiffList t List.[]
+  toList = DiffList.toList ∘ toDiffList
 
   size : ∀ {l u h} → Tree V l u h → ℕ
   size = List.length ∘′ toList
 
-module _ {v w} {V : Value v} {W : Value w} where
-
-  private
-    Val = Value.family V
-    Wal = Value.family W
-
-  -- Maps a function over all values in the tree.
-
-  map : ∀[ Val ⇒ Wal ] → ∀ {l u h} → Tree V l u h → Tree W l u h
-  map f (leaf l<u)             = leaf l<u
-  map f (node (k , v) l r bal) = node (k , f v) (map f l) (map f r) bal

From 47008bd0785a2c26d8f7a75c201d841b35f7d661 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 09:32:12 +0000
Subject: [PATCH 05/13] refactor: use of `variable`s; tighten `import`s

---
 .../Tree/AVL/Indexed/Relation/Unary/Any.agda  | 35 ++++++++++---------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index c81599da2a..2e7b636f5e 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -18,9 +18,9 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘′_; _∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎?_)
-open import Relation.Unary
+open import Relation.Unary using (Pred; _⊆_; Satisfiable; Decidable)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
+open StrictTotalOrder strictTotalOrder using () renaming (Carrier to Key)
 open import Data.Tree.AVL.Indexed strictTotalOrder
   using (Tree; Value; Key⁺; [_]; _<⁺_; K&_; _,_; key; _∼_⊔_; ∼0; leaf; node)
 
@@ -31,9 +31,12 @@ private
     V : Value v
     P : Pred (K& V) p
     Q : Pred (K& V) q
+    k : Key
     l u : Key⁺
     n : ℕ
-    t : Tree V l u n
+    hˡ hʳ h : ℕ
+    t : Tree V l u h
+
 
 ------------------------------------------------------------------------
 -- Definition
@@ -42,20 +45,20 @@ private
 -- satisfies P. There may be others.
 -- See `Relation.Unary` for an explanation of predicates.
 
-data Any {V : Value v} (P : Pred (K& V) p) {l u}
-     : ∀ {n} → Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
-  here  : ∀ {hˡ hʳ h} {kv : K& V} → P kv →
+data Any {V : Value v} (P : Pred (K& V) p)
+     : Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
+  here  : ∀ {kv : K& V} → P kv →
           {lk : Tree V l [ kv .key ] hˡ}
           {ku : Tree V [ kv .key ] u hʳ}
           {bal : hˡ ∼ hʳ ⊔ h} →
           Any P (node kv lk ku bal)
-  left  : ∀ {hˡ hʳ h} {kv : K& V}
+  left  : ∀ {kv : K& V}
           {lk : Tree V l [ kv .key ] hˡ} →
           Any P lk →
           {ku : Tree V [ kv .key ] u hʳ}
           {bal : hˡ ∼ hʳ ⊔ h} →
           Any P (node kv lk ku bal)
-  right : ∀ {hˡ hʳ h} {kv : K& V}
+  right : ∀ {kv : K& V}
           {lk : Tree V l [ kv .key ] hˡ}
           {ku : Tree V [ kv .key ] u hʳ} →
           Any P ku →
@@ -80,12 +83,12 @@ lookupKey = key ∘′ lookup
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : Any P t → ∃ P
+satisfied : Any P t → Satisfiable P
 satisfied (here  p) = -, p
 satisfied (left  p) = satisfied p
 satisfied (right p) = satisfied p
 
-module _ {hˡ hʳ h} {kv : K& V}
+module _ {kv : K& V}
   {lk : Tree V l [ kv .key ] hˡ}
   {ku : Tree V [ kv .key ] u hʳ}
   {bal : hˡ ∼ hʳ ⊔ h}
@@ -104,13 +107,11 @@ module _ {hˡ hʳ h} {kv : K& V}
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by Any
 
-any? : Decidable P → (t : Tree V l u n) → Dec (Any P t)
-any? P? (leaf _)          = no λ ()
-any? P? (node kv l r bal) = map′ fromSum toSum
-  (P? kv ⊎? any? P? l ⊎? any? P? r)
+any? : Decidable P → Decidable {A = Tree V l u h} (Any P)
+any? P? (leaf _)        = no λ()
+any? P? (node kv l r _) = map′ fromSum toSum (P? kv ⊎? any? P? l ⊎? any? P? r)
 
-satisfiable : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u →
+satisfiable : l <⁺ [ k ] → [ k ] <⁺ u →
               Satisfiable (P ∘ (k ,_)) →
               Satisfiable {A = Tree V l u 1} (Any P)
-satisfiable {k = k} lb ub sat = node (k , proj₁ sat) (leaf lb) (leaf ub) ∼0
-                              , here (proj₂ sat)
+satisfiable {k = k} lb ub (v , pv) = node (k , v) (leaf lb) (leaf ub) ∼0 , here pv

From 6535cd0b6c8ac51474ee304fe5ae2e6b011a8071 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 10:01:54 +0000
Subject: [PATCH 06/13] tidy up: use of `variable`s; tighten `import`s

---
 src/Data/Tree/AVL/Indexed.agda                | 25 +++++++++----------
 .../Tree/AVL/Indexed/Relation/Unary/Any.agda  |  2 +-
 2 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index c6ac393cf8..74bd58669a 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -13,7 +13,7 @@ module Data.Tree.AVL.Indexed
 
 open import Level using (Level; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
-open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁)
+open import Data.Product.Base using (Σ; ∃; _×_; _,_)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.List.Base as List using (List)
 open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _++_)
@@ -22,7 +22,8 @@ open import Relation.Unary
 open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
+open StrictTotalOrder strictTotalOrder
+  using (module Eq; compare) renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
 -- Re-export core definitions publicly
@@ -38,7 +39,6 @@ private
   variable
     ℓ v w : Level
     A : Set ℓ
-    k : Key
     l m u : Key⁺
     hˡ hʳ h : ℕ
 
@@ -51,10 +51,9 @@ private
 --
 -- (The bal argument is the balance factor.)
 
-data Tree {v} (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) where
+data Tree (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) where
   leaf : (l<u : l <⁺ u) → Tree V l u 0
-  node : ∀ {hˡ hʳ h}
-         (kv : K& V)
+  node : (kv : K& V)
          (lk : Tree V l [ kv .key ] hˡ)
          (ku : Tree V [ kv .key ] u hʳ)
          (bal : hˡ ∼ hʳ ⊔ h) →
@@ -86,7 +85,7 @@ module _ {V : Value v} {W : Value w}
 
 module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
-  ordered : ∀ {l u n} → Tree V l u n → l <⁺ u
+  ordered : Tree V l u h → l <⁺ u
   ordered (leaf l<u)          = l<u
   ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
 
@@ -100,7 +99,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   -- Injectivity of constructors
 
-  leaf-injective : ∀ {l u} {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
+  leaf-injective : ∀ {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
   leaf-injective refl = refl
 
   node-injective-key :
@@ -124,7 +123,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   -- A singleton tree.
 
-  singleton : ∀ (k : Key) → Val k → l < k < u → Tree V l u 1
+  singleton : ∀ k → Val k → l < k < u → Tree V l u 1
   singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0
 
   -- Cast operations. Logarithmic in the size of the tree, if we don't
@@ -229,7 +228,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   -- tree (assuming constant-time comparisons and a constant-time
   -- combining function).
 
-  insertWith : ∀ (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
+  insertWith : ∀ k → (Maybe (Val k) → Val k) →  -- Maybe old → result.
                Tree V l u h → l < k < u → Tree⁺ V l u h
   insertWith k f (leaf l<u) l<k<u = 1# , singleton k (f nothing) l<k<u
   insertWith k f (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k k′
@@ -273,13 +272,13 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   foldr cons nil (leaf l<u)             = nil
   foldr cons nil (node (_ , v) l r bal) = foldr cons (cons v (foldr cons nil r)) l
 
-  toDiffList : ∀ {l u h} → Tree V l u h → DiffList (K& V)
+  toDiffList : Tree V l u h → DiffList (K& V)
   toDiffList (leaf _)       = []
   toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r
 
-  toList : ∀ {l u h} → Tree V l u h → List (K& V)
+  toList : Tree V l u h → List (K& V)
   toList = DiffList.toList ∘ toDiffList
 
-  size : ∀ {l u h} → Tree V l u h → ℕ
+  size : Tree V l u h → ℕ
   size = List.length ∘′ toList
 
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 2e7b636f5e..527e0b3788 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -81,7 +81,7 @@ lookup (right p)          = lookup p
 lookupKey : Any P t → Key
 lookupKey = key ∘′ lookup
 
--- If any element satisfies P, then P is satisfied.
+-- If any element satisfies P, then P is satisfiable.
 
 satisfied : Any P t → Satisfiable P
 satisfied (here  p) = -, p

From 21e69ddc5ea14e32cbd4b6d532b787d79e5aaf05 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 10:05:53 +0000
Subject: [PATCH 07/13] fix: `CHANGELOG`

---
 CHANGELOG.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 99dea4e749..6c43eae734 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -397,6 +397,20 @@ Additions to existing modules
   showAtPrecision : ℕ → ℚᵘ → String
   ```
 
+* In `Data.Tree.AVL.Height`:
+  ```agda
+  0∼⊔ : 0 ∼ j ⊔ m → j ≡ m
+  ∼0⊔ : i ∼ 0 ⊔ m → i ≡ m
+  ```
+
+* In `Data.Tree.AVL.Indexed`:
+  ```agda
+  Tree⁺ Tree⁻ : (V : Value v) (l u : Key⁺) (h : ℕ) → Set _
+  pattern leaf⁻ l<u = _ , leaf l<u
+  pattern node⁰ʳ k₁ t₁ k₂ t₂ t₃ = node k₁ t₁ (node k₂ t₂ t₃ ∼0) ∼0
+  pattern node⁰ˡ k₁ k₂ t₁ t₂ t₃ = node k₁ (node k₂ t₁ t₂ ∼0) t₃ ∼0
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) →

From 10d8877e67c6057600c013b2c9a3d7ff843b3267 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 10:06:47 +0000
Subject: [PATCH 08/13] fix: whitespace

---
 src/Data/Tree/AVL/Indexed.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 74bd58669a..9510b125ae 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -90,7 +90,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
 
   private
-  
+
   -- This lemma justifies the use of `leaf⁻` pattern matches in code below
 
     tree⁻0 : (t⁻ : Tree⁻ V l u 0) →

From a1615e7cbc6ecefd487d1cb61a69fd03f1635cf8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 09:29:38 +0000
Subject: [PATCH 09/13] fix: remove `n` as a name for height `h`

---
 src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 527e0b3788..100584948c 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -33,7 +33,6 @@ private
     Q : Pred (K& V) q
     k : Key
     l u : Key⁺
-    n : ℕ
     hˡ hʳ h : ℕ
     t : Tree V l u h
 
@@ -46,7 +45,7 @@ private
 -- See `Relation.Unary` for an explanation of predicates.
 
 data Any {V : Value v} (P : Pred (K& V) p)
-     : Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
+     : Tree V l u h → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
   here  : ∀ {kv : K& V} → P kv →
           {lk : Tree V l [ kv .key ] hˡ}
           {ku : Tree V [ kv .key ] u hʳ}

From f40e5726913e9cba104be6551b0415b6560f0fe2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 09:36:19 +0000
Subject: [PATCH 10/13] add: `private` lemma `tree0`

---
 src/Data/Tree/AVL/Indexed.agda | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 9510b125ae..fac711cbec 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -91,7 +91,10 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   private
 
-  -- This lemma justifies the use of `leaf⁻` pattern matches in code below
+  -- Lemmas justifying the use of `leaf`/`leaf⁻` pattern matches in code below
+
+    tree0 : (t : Tree V l u 0) → t ≡ leaf (ordered t)
+    tree0 t@(leaf _) = refl
 
     tree⁻0 : (t⁻ : Tree⁻ V l u 0) →
              ∃ λ i → ∃ λ t → t⁻ ≡ (i , t) × t ≡ leaf (ordered t)
@@ -281,4 +284,3 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   size : Tree V l u h → ℕ
   size = List.length ∘′ toList
-

From 75fd7422c67636e2a244ee5a5ab7c4eda8e4db6c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 09:46:17 +0000
Subject: [PATCH 11/13] refactor: rename and deprecate

---
 CHANGELOG.md                                  |  8 ++
 .../Relation/Unary/Any/Properties.agda        | 77 ++++++++++++++-----
 2 files changed, 64 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6c43eae734..62062b45f6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -104,6 +104,14 @@ Deprecated names
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
   ```
 
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties`:
+  ```agda
+  Any-insertWith-nothing  ↦  insertWith-nothing
+  Any-insertWith-just     ↦  insertWith-just
+  Any-insert-nothing      ↦  insert-nothing
+  Any-insert-just         ↦  insert-just
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index c2762172b9..322b7daac3 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -249,31 +249,33 @@ module _ {V : Value v} where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    Any-insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
-                             P (k , f nothing) →
-                             ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
-    Any-insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
+    insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
+                         P (k , f nothing) →
+                         ¬ (Any ((k ≈_) ∘′ key) t) →
+                         Any P (proj₂ (insertWith k f t seg))
+    insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
+    insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
       with compare k k′
     ... | tri≈ _ k≈k′ _ = contradiction (here k≈k′) ¬p
     ... | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′
-                              ih = Any-insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
+                              ih = insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
                           in joinˡ⁺-left⁺ kv lk′ ku bal ih
     ... | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′
-                              ih = Any-insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
+                              ih = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
                           in joinʳ⁺-right⁺ kv lk ku′ bal ih
 
-    Any-insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
-                          (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
-                          Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
+    insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
+                      (pr : ∀ k′ v → (eq : k ≈ k′) →
+                            P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
+                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
+    insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
     -- happy paths
     ... | here _   | tri≈ _ k≈k′ _ = here (pr k′ v k≈k′)
     ... | left lp  | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′ in
-                                     joinˡ⁺-left⁺ kv lk′ ku bal (Any-insertWith-just lk seg′ pr lp)
+                                     joinˡ⁺-left⁺ kv lk′ ku bal (insertWith-just lk seg′ pr lp)
     ... | right rp | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′ in
-                                     joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
+                                     joinʳ⁺-right⁺ kv lk ku′ bal (insertWith-just ku seg′ pr rp)
 
     -- impossible cases
     ... | here eq  | tri< k<k′ _ _ = begin-contradiction
@@ -311,17 +313,18 @@ module _ {V : Value v} where
 
   module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
 
-    Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
-    Any-insert-nothing = Any-insertWith-nothing k (F.const v) t seg
+    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
+                     Any P (proj₂ (insert k v t seg))
+    insert-nothing = insertWith-nothing k (F.const v) t seg
 
-    Any-insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
-                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    Any-insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
+                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
+    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
     insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
-                  (p : Any P t) → k ≉ Any.lookupKey p →
+                  (p : Any P t) → k ≉ lookupKey p →
                   Any P (proj₂ (insertWith k f t seg))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
@@ -348,7 +351,7 @@ module _ {V : Value v} where
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
   insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
-            (p : Any P t) → k ≉ Any.lookupKey p →
+            (p : Any P t) → k ≉ lookupKey p →
             Any P (proj₂ (insert k v t seg))
   insert⁺ k v = insertWith⁺ k (F.const v)
 
@@ -393,7 +396,7 @@ module _ {V : Value v} where
 
   lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
             (p : Any P t) →
-            key (Any.lookup p) ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
+            lookupKey p ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p
   ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
@@ -417,3 +420,35 @@ module _ {V : Value v} where
   ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
   ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
   ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+Any-insertWith-nothing = insertWith-nothing
+{-# WARNING_ON_USAGE Any-insertWith-nothing
+"Warning: Any-insertWith-nothing was deprecated in v2.4.
+Please use insertWith-nothing instead."
+#-}
+Any-insertWith-just = insertWith-just
+{-# WARNING_ON_USAGE Any-insertWith-just
+"Warning: Any-insertWith-just was deprecated in v2.4.
+Please use insertWith-just instead."
+#-}
+Any-insert-nothing = insert-nothing
+{-# WARNING_ON_USAGE Any-insert-nothing
+"Warning: Any-insert-nothing was deprecated in v2.4.
+Please use insert-nothing instead."
+#-}
+Any-insert-just = insert-just
+{-# WARNING_ON_USAGE Any-insert-just
+"Warning: Any-insert-just was deprecated in v2.4.
+Please use insert-just instead."
+#-}

From 07c1a5b35c37e242d8cb53e29840e5510328b905 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 14:47:46 +0000
Subject: [PATCH 12/13] refactor: use type synonyms; tidy up `variable`s; tidy
 uo `module`-level parameterisation; fix ref. to `lookup`

---
 .../Relation/Unary/Any/Properties.agda        | 219 +++++++++---------
 1 file changed, 104 insertions(+), 115 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 322b7daac3..5a14794b09 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -26,7 +26,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable.Core as Dec using (Dec; yes; no)
 open import Relation.Unary using (Pred; _∩_)
 
-open import Data.Tree.AVL.Indexed sto as AVL
+open import Data.Tree.AVL.Indexed sto as AVL hiding (lookup)
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
 open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
 
@@ -40,38 +40,40 @@ private
     k : Key
     V : Value v
     l u : Key⁺
-    n : ℕ
+    hˡ hʳ h : ℕ
     P Q : Pred (K& V) p
 
 ------------------------------------------------------------------------
--- Any.lookup
+-- lookup
 
-lookup-result : {t : Tree V l u n} (p : Any P t) → P (Any.lookup p)
+lookup-result : {t : Tree V l u h} (p : Any P t) → P (lookup p)
 lookup-result (here p)  = p
 lookup-result (left p)  = lookup-result p
 lookup-result (right p) = lookup-result p
 
-lookup-bounded : {t : Tree V l u n} (p : Any P t) → l < Any.lookup p .key < u
+lookup-bounded : {t : Tree V l u h} (p : Any P t) → l < lookupKey p < u
 lookup-bounded {t = node kv lk ku bal} (here p)  = ordered lk , ordered ku
 lookup-bounded {t = node kv lk ku bal} (left p)  =
   Prod.map₂ (flip (trans⁺ _) (ordered ku)) (lookup-bounded p)
 lookup-bounded {t = node kv lk ku bal} (right p) =
   Prod.map₁ (trans⁺ _ (ordered lk)) (lookup-bounded p)
 
-lookup-rebuild : {t : Tree V l u n} (p : Any P t) → Q (Any.lookup p) → Any Q t
+lookup-rebuild : {t : Tree V l u h} (p : Any P t) → Q (lookup p) → Any Q t
 lookup-rebuild (here _)  q = here q
 lookup-rebuild (left p)  q = left (lookup-rebuild p q)
 lookup-rebuild (right p) q = right (lookup-rebuild p q)
 
-lookup-rebuild-accum : {t : Tree V l u n} (p : Any P t) → Q (Any.lookup p) → Any (Q ∩ P) t
+lookup-rebuild-accum : {t : Tree V l u h} (p : Any P t) → Q (lookup p) → Any (Q ∩ P) t
 lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)
 
-joinˡ⁺-here⁺ : ∀ {l u hˡ hʳ h} →
-             (kv : K& V) →
-             (l : ∃ λ i → Tree V l [ kv .key ] (i ⊕ hˡ)) →
-             (r : Tree V [ kv .key ] u hʳ) →
-             (bal : hˡ ∼ hʳ ⊔ h) →
-             P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
+------------------------------------------------------------------------
+-- joinˡ⁺
+
+joinˡ⁺-here⁺ : (kv@(k , _) : K& V) →
+               (l : Tree⁺ V l [ k ] hˡ) →
+               (r : Tree V [ k ] u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
 joinˡ⁺-here⁺ k₂ (0# , t₁)                       t₃ bal p = here p
 joinˡ⁺-here⁺ k₂ (1# , t₁)                       t₃ ∼0  p = here p
 joinˡ⁺-here⁺ k₂ (1# , t₁)                       t₃ ∼+  p = here p
@@ -79,12 +81,11 @@ joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  p = ri
 joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  p = right (here p)
 joinˡ⁺-here⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  p = right (here p)
 
-joinˡ⁺-left⁺ : ∀ {l u hˡ hʳ h} →
-             (k : K& V) →
-             (l : ∃ λ i → Tree V l [ k .key ] (i ⊕ hˡ)) →
-             (r : Tree V [ k .key ] u hʳ) →
-             (bal : hˡ ∼ hʳ ⊔ h) →
-             Any P (proj₂ l) → Any P (proj₂ (joinˡ⁺ k l r bal))
+joinˡ⁺-left⁺ : (kv@(k , _) : K& V) →
+               (l@(_ , t) : Tree⁺ V l [ k ] hˡ) →
+               (r : Tree V [ k ] u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P t → Any P (proj₂ (joinˡ⁺ kv l r bal))
 joinˡ⁺-left⁺ k₂ (0# , t₁)                       t₃ bal p                 = left p
 joinˡ⁺-left⁺ k₂ (1# , t₁)                       t₃ ∼0  p                 = left p
 joinˡ⁺-left⁺ k₂ (1# , t₁)                       t₃ ∼+  p                 = left p
@@ -100,9 +101,8 @@ joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (r
 joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (right (left p))  = left (right p)
 joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (right (right p)) = right (left p)
 
-joinˡ⁺-right⁺ : ∀ {l u hˡ hʳ h} →
-                (kv@(k , v) : K& V) →
-                (l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
+joinˡ⁺-right⁺ : (kv@(k , _) : K& V) →
+                (l : Tree⁺ V l [ k ] hˡ) →
                 (r : Tree V [ k ] u hʳ) →
                 (bal : hˡ ∼ hʳ ⊔ h) →
                 Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
@@ -113,10 +113,42 @@ joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  p = r
 joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  p = right (right p)
 joinˡ⁺-right⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  p = right (right p)
 
-joinʳ⁺-here⁺ : ∀ {l u hˡ hʳ h} →
-               (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
+joinˡ⁺⁻ : (kv@(k , v) : K& V) →
+          (l@(_ , t) : Tree⁺ V l [ k ] hˡ) →
+          (r : Tree V [ k ] u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinˡ⁺ kv l r bal)) →
+          P kv ⊎ Any P t ⊎ Any P r
+joinˡ⁺⁻ k₂ (0# , t₁)                       t₃ ba = Any.toSum
+joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼0 = Any.toSum
+joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼+ = Any.toSum
+joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼- = λ where
+  (left p)          → inj₂ (inj₁ (left p))
+  (here p)          → inj₂ (inj₁ (here p))
+  (right (left p))  → inj₂ (inj₁ (right p))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼- = λ where
+  (left p)          → inj₂ (inj₁ (left p))
+  (here p)          → inj₂ (inj₁ (here p))
+  (right (left p))  → inj₂ (inj₁ (right p))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+joinˡ⁺⁻ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- = λ where
+  (left (left p))   → inj₂ (inj₁ (left p))
+  (left (here p))   → inj₂ (inj₁ (here p))
+  (left (right p))  → inj₂ (inj₁ (right (left p)))
+  (here p)          → inj₂ (inj₁ (right (here p)))
+  (right (left p))  → inj₂ (inj₁ (right (right p)))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+
+------------------------------------------------------------------------
+-- joinʳ⁺
+
+joinʳ⁺-here⁺ : (kv@(k , _) : K& V) →
+               (l : Tree V l [ k ] hˡ) →
+               (r : Tree⁺ V [ k ] u hʳ) →
                (bal : hˡ ∼ hʳ ⊔ h) →
                P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
 joinʳ⁺-here⁺ k₂ t₁ (0# , t₃)                       bal p = here p
@@ -126,12 +158,11 @@ joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  p = le
 joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  p = left (here p)
 joinʳ⁺-here⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  p = left (here p)
 
-joinʳ⁺-left⁺ : ∀ {l u hˡ hʳ h} →
-              (kv : K& V) →
-              (l : Tree V l [ kv .key ] hˡ) →
-              (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
-              (bal : hˡ ∼ hʳ ⊔ h) →
-              Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-left⁺ : (kv@(k , _) : K& V) →
+               (l : Tree V l [ k ] hˡ) →
+               (r : Tree⁺ V [ k ] u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
 joinʳ⁺-left⁺ k₂ t₁ (0# , t₃)                       bal p = left p
 joinʳ⁺-left⁺ k₂ t₁ (1# , t₃)                       ∼0  p = left p
 joinʳ⁺-left⁺ k₂ t₁ (1# , t₃)                       ∼-  p = left p
@@ -139,12 +170,11 @@ joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  p = le
 joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  p = left (left p)
 joinʳ⁺-left⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  p = left (left p)
 
-joinʳ⁺-right⁺ : ∀ {l u hˡ hʳ h} →
-                (kv : K& V) →
-                (l : Tree V l [ kv .key ] hˡ) →
-                (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
+joinʳ⁺-right⁺ : (kv@(k , _) : K& V) →
+                (l : Tree V l [ k ] hˡ) →
+                (r@(_ , t) : Tree⁺ V [ k ] u hʳ) →
                 (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
+                Any P t → Any P (proj₂ (joinʳ⁺ kv l r bal))
 joinʳ⁺-right⁺ k₂ t₁ (0# , t₃)                       bal p                = right p
 joinʳ⁺-right⁺ k₂ t₁ (1# , t₃)                       ∼0  p                = right p
 joinʳ⁺-right⁺ k₂ t₁ (1# , t₃)                       ∼-  p                = right p
@@ -160,44 +190,12 @@ joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (
 joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (left (right p)) = right (left p)
 joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (right p)        = right (right p)
 
-joinˡ⁺⁻ : ∀ {l u hˡ hʳ h} →
-            (kv@(k , v) : K& V) →
-            (l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
-            (r : Tree V [ k ] u hʳ) →
-            (bal : hˡ ∼ hʳ ⊔ h) →
-            Any P (proj₂ (joinˡ⁺ kv l r bal)) →
-            P kv ⊎ Any P (proj₂ l) ⊎ Any P r
-joinˡ⁺⁻ k₂ (0# , t₁)                       t₃ ba = Any.toSum
-joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼0 = Any.toSum
-joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼+ = Any.toSum
-joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼- = λ where
-  (left p)          → inj₂ (inj₁ (left p))
-  (here p)          → inj₂ (inj₁ (here p))
-  (right (left p))  → inj₂ (inj₁ (right p))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼- = λ where
-  (left p)          → inj₂ (inj₁ (left p))
-  (here p)          → inj₂ (inj₁ (here p))
-  (right (left p))  → inj₂ (inj₁ (right p))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-joinˡ⁺⁻ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- = λ where
-  (left (left p))   → inj₂ (inj₁ (left p))
-  (left (here p))   → inj₂ (inj₁ (here p))
-  (left (right p))  → inj₂ (inj₁ (right (left p)))
-  (here p)          → inj₂ (inj₁ (right (here p)))
-  (right (left p))  → inj₂ (inj₁ (right (right p)))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-
-joinʳ⁺⁻ : ∀ {l u hˡ hʳ h} →
-            (kv : K& V) →
-            (l : Tree V l [ kv .key ] hˡ) →
-            (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
-            (bal : hˡ ∼ hʳ ⊔ h) →
-            Any P (proj₂ (joinʳ⁺ kv l r bal)) →
-            P kv ⊎ Any P l ⊎ Any P (proj₂ r)
+joinʳ⁺⁻ : (kv@(k , _) : K& V) →
+          (l : Tree V l [ k ] hˡ) →
+          (r@(_ , t) : Tree⁺ V [ k ] u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinʳ⁺ kv l r bal)) →
+          P kv ⊎ Any P l ⊎ Any P t
 joinʳ⁺⁻ k₂ t₁ (0# , t₃)                       bal = Any.toSum
 joinʳ⁺⁻ k₂ t₁ (1# , t₃)                       ∼0  = Any.toSum
 joinʳ⁺⁻ k₂ t₁ (1# , t₃)                       ∼-  = Any.toSum
@@ -222,23 +220,19 @@ joinʳ⁺⁻ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  = λ wh
   (right (here p))  → inj₂ (inj₂ (here p))
   (right (right p)) → inj₂ (inj₂ (right p))
 
-module _ {V : Value v} where
+----------------------------------------------------------------------
+-- Properties of tree construction operations
+
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
-  private
-    Val  = Value.family V
-    Val≈ = Value.respects V
+  ----------------------------------------------------------------------
+  -- singleton
 
-  singleton⁺ : {P : Pred (K& V) p} →
-               (k : Key) →
-               (v : Val k) →
-               (l<k<u : l < k < u) →
+  singleton⁺ : (k : Key) (v : Val k) (l<k<u : l < k < u) →
                P (k , v) → Any P (singleton k v l<k<u)
   singleton⁺ k v l<k<u Pkv = here Pkv
 
-  singleton⁻ : {P : Pred (K& V) p} →
-               (k : Key) →
-               (v : Val k) →
-               (l<k<u : l < k < u) →
+  singleton⁻ : (k : Key) (v : Val k) (l<k<u : l < k < u) →
                Any P (singleton k v l<k<u) → P (k , v)
   singleton⁻ k v l<k<u (here Pkv) = Pkv
 
@@ -249,7 +243,7 @@ module _ {V : Value v} where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
+    insertWith-nothing : (t : Tree V l u h) (seg : l < k < u) →
                          P (k , f nothing) →
                          ¬ (Any ((k ≈_) ∘′ key) t) →
                          Any P (proj₂ (insertWith k f t seg))
@@ -264,9 +258,9 @@ module _ {V : Value v} where
                               ih = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
                           in joinʳ⁺-right⁺ kv lk ku′ bal ih
 
-    insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
+    insertWith-just : (t : Tree V l u h) (seg : l < k < u) →
                       (pr : ∀ k′ v → (eq : k ≈ k′) →
-                            P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
+                            P (k′ , respects eq (f (just (respects (sym eq) v))))) →
                       Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
     insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
@@ -311,19 +305,7 @@ module _ {V : Value v} where
       [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
       [ k  ] ∎
 
-  module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
-
-    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
-                     Any P (proj₂ (insert k v t seg))
-    insert-nothing = insertWith-nothing k (F.const v) t seg
-
-    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
-                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
-
-  module _ (k : Key) (f : Maybe (Val k) → Val k) where
-
-    insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
+    insertWith⁺ : (t : Tree V l u h) (seg : l < k < u) →
                   (p : Any P t) → k ≉ lookupKey p →
                   Any P (proj₂ (insertWith k f t seg))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
@@ -350,18 +332,27 @@ module _ {V : Value v} where
                               ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
-  insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
-            (p : Any P t) → k ≉ lookupKey p →
-            Any P (proj₂ (insert k v t seg))
-  insert⁺ k v = insertWith⁺ k (F.const v)
+  module _ (k : Key) (v : Val k) (t : Tree V l u h) (seg : l < k < u) where
+
+    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
+                     Any P (proj₂ (insert k v t seg))
+    insert-nothing = insertWith-nothing k (F.const v) t seg
+
+    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , respects eq v)) →
+                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
+    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+
+    insert⁺ : (p : Any P t) → k ≉ lookupKey p →
+              Any P (proj₂ (insert k v t seg))
+    insert⁺ = insertWith⁺ k (F.const v) t seg
 
   module _
     {P : Pred (K& V) p}
-    (P-Resp : ∀ {k k′ v} → (k≈k′ : k ≈ k′) → P (k′ , Val≈ k≈k′ v) → P (k , v))
+    (P-Resp : ∀ {k k′ v} → (k≈k′ : k ≈ k′) → P (k′ , respects k≈k′ v) → P (k , v))
     (k : Key) (v : Val k)
     where
 
-    insert⁻ : (t : Tree V l u n) (seg : l < k < u) →
+    insert⁻ : (t : Tree V l u h) (seg : l < k < u) →
               Any P (proj₂ (insert k v t seg)) →
               P (k , v) ⊎ Any (λ{ (k′ , v′) → k ≉ k′ × P (k′ , v′)}) t
     insert⁻ (leaf l<u) seg (here p) = inj₁ p
@@ -394,9 +385,9 @@ module _ {V : Value v} where
       k′<p = [<]-injective (proj₁ (lookup-bounded p))
       k≉p = λ k≈p → irrefl (trans (sym k≈k′) k≈p) k′<p
 
-  lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
+  lookup⁺ : (t : Tree V l u h) (k : Key) (seg : l < k < u) →
             (p : Any P t) →
-            lookupKey p ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
+            lookupKey p ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (respects p≈k (value (Any.lookup p)))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p
   ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
@@ -413,17 +404,15 @@ module _ {V : Value v} where
   ... | tri> _ _ k<k′ | right p = inj₁ (λ p≈k → irrefl (sym p≈k) (<-trans k<k′ k′<p))
     where k′<p = [<]-injective (proj₁ (lookup-bounded p))
 
-  lookup⁻ : (t : Tree V l u n) (k : Key) (v : Val k) (seg : l < k < u) →
+  lookup⁻ : (t : Tree V l u h) (k : Key) (v : Val k) (seg : l < k < u) →
             AVL.lookup t k seg ≡ just v →
-            Any (λ{ (k′ , v′) → ∃ λ k′≈k → Val≈ k′≈k v′ ≡ v}) t
+            Any (λ{ (k′ , v′) → ∃ λ k′≈k → respects k′≈k v′ ≡ v}) t
   lookup⁻ (node (k′ , v′) l r bal) k v (l<k , k<u) eq with compare k′ k
   ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
   ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
   ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
 
 
-
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

From 12986bf0d3b60c9f5f0615806abf2808ef0ce55e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 15:41:34 +0000
Subject: [PATCH 13/13] TODO: fix unsolved metas

---
 .../Tree/AVL/Map/Membership/Propositional/Properties.agda     | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index 5e472cfe2b..d576c3bfa7 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -72,10 +72,10 @@ private
 -- singleton
 
 ∈ₖᵥ-singleton⁺ : (k , x) ∈ₖᵥ singleton k x
-∈ₖᵥ-singleton⁺ = tree (IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl))
+∈ₖᵥ-singleton⁺ = tree {!IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl)!}
 
 ∈ₖᵥ-singleton⁻ : (k , x) ∈ₖᵥ singleton k′ x′ → k ≈ k′ × x ≡ x′
-∈ₖᵥ-singleton⁻ (tree p) = IAnyₚ.singleton⁻ _ _ _ p
+∈ₖᵥ-singleton⁻ (tree p) = {!IAnyₚ.singleton⁻ _ _ _ p!}
 
 private
   ≈-lookup : (p : (k , x) ∈ₖᵥ m) → k ≈ Any.lookupKey p