    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Values for AVL trees
    -- Values must respect the underlying equivalence on keys
    ------------------------------------------------------------------------

    {-# 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)

    ------------------------------------------------------------------------
    -- A Value

    record Value v : Set (a ⊔ ℓ ⊔ suc v) where
      constructor MkValue
      field
        family   : Key → Set v
        respects : family Respects _≈_

    ------------------------------------------------------------------------
    -- A Key together with its value

    record K&_ {v} (V : Value v) : Set (a ⊔ v) where
      constructor _,_
      field
        key   : Key
        value : Value.family V key
    infixr 4 _,_
    open K&_ public

    module _ {v} {V : Value v} where

      toPair : K& V → Σ Key (Value.family V)
      toPair (k , v) = k , v

      fromPair : Σ Key (Value.family V) → K& V
      fromPair (k , v) = k , v

    ------------------------------------------------------------------------
    -- The constant family of values

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