    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- AVL trees where at least one element satisfies a given property
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Bundles using (StrictTotalOrder)

    module Data.Tree.AVL.Indexed.Relation.Unary.Any
      {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
      where

    open import Data.Nat.Base using (ℕ)
    open import Data.Product.Base using (_,_; ∃; -,_; proj₁; proj₂)
    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′; _⊎-dec_)
    open import Relation.Unary

    open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
    open import Data.Tree.AVL.Indexed strictTotalOrder
      using (Tree; Value; Key⁺; [_]; _<⁺_; K&_; _,_; key; _∼_⊔_; ∼0; leaf; node)

    private
      variable
        v p q : Level
        V : Value v
        P : Pred (K& V) p
        Q : Pred (K& V) q
        l u : Key⁺
        n : ℕ
        t : Tree V l u n

    ------------------------------------------------------------------------
    -- Definition

    -- Given a predicate P, Any P t describes a path in t to an element that
    -- 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 →
              {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}
              {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}
              {lk : Tree V l [ kv .key ] hˡ}
              {ku : Tree V [ kv .key ] u hʳ} →
              Any P ku →
              {bal : hˡ ∼ hʳ ⊔ h} →
              Any P (node kv lk ku bal)

    ------------------------------------------------------------------------
    -- Operations on Any

    map : P ⊆ Q → Any P t → Any Q t
    map f (here  p) = here (f p)
    map f (left  p) = left (map f p)
    map f (right p) = right (map f p)

    lookup : Any {V = V} P t → K& V
    lookup (here {kv = kv} _) = kv
    lookup (left  p)          = lookup p
    lookup (right p)          = lookup p

    lookupKey : Any P t → Key
    lookupKey = key ∘′ lookup

    -- If any element satisfies P, then P is satisfied.

    satisfied : Any P t → ∃ P
    satisfied (here  p) = -, p
    satisfied (left  p) = satisfied p
    satisfied (right p) = satisfied p

    module _ {hˡ hʳ h} {kv : K& V}
      {lk : Tree V l [ kv .key ] hˡ}
      {ku : Tree V [ kv .key ] u hʳ}
      {bal : hˡ ∼ hʳ ⊔ h}
      where

      toSum : Any P (node kv lk ku bal) → P kv ⊎ Any P lk ⊎ Any P ku
      toSum (here p)  = inj₁ p
      toSum (left p)  = inj₂ (inj₁ p)
      toSum (right p) = inj₂ (inj₂ p)

      fromSum : P kv ⊎ Any P lk ⊎ Any P ku → Any P (node kv lk ku bal)
      fromSum (inj₁ p)        = here p
      fromSum (inj₂ (inj₁ p)) = left p
      fromSum (inj₂ (inj₂ p)) = right p

    ------------------------------------------------------------------------
    -- 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 ⊎-dec any? P? l ⊎-dec any? P? r)

    satisfiable : ∀ {k l u} → 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)