```------------------------------------------------------------------------
-- The Agda standard library
--
-- Keys for AVL trees -- the original key type extended with a new
-- minimum and maximum.
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles
using (StrictTotalOrder; StrictPartialOrder)
open import Relation.Binary.Definitions using (Reflexive)

module Data.Tree.AVL.Key
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
where

open import Level
open import Data.Empty
open import Data.Unit
open import Data.Product.Base using (_×_; _,_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
open import Relation.Nullary.Negation using (¬_)

open StrictTotalOrder sto renaming (Carrier to Key)
using (_≈_; _<_; trans; irrefl; module Eq)

------------------------------------------------------------------------
-- Keys are augmented with new extrema (i.e. an artificial minimum and
-- maximum)

Key⁺ : Set a
Key⁺ = Key ±

using ([_]; [_]-injective)
renaming
( ⊥± to ⊥⁺
; ⊤± to ⊤⁺
)

------------------------------------------------------------------------
-- The equality is extended in a corresponding manner

using ()
renaming
( _≈±_ to _≈⁺_
; [_]  to [_]ᴱ
)

------------------------------------------------------------------------
-- The order is extended in a corresponding manner

using () renaming
(_<±_    to _<⁺_
; [_]    to [_]ᴿ
; ⊥±<⊤±  to ⊥⁺<⊤⁺
; [_]<⊤± to [_]<⊤⁺
; ⊥±<[_] to ⊥⁺<[_]
)

-- A pair of ordering constraints.

infix 4 _<_<_

_<_<_ : Key⁺ → Key → Key⁺ → Set (a ⊔ ℓ₂)
l < x < u = l <⁺ [ x ] × [ x ] <⁺ u

-- Properties

⊥⁺<[_]<⊤⁺ : ∀ k → ⊥⁺ < k < ⊤⁺
⊥⁺<[ k ]<⊤⁺ = ⊥⁺<[ k ] , [ k ]<⊤⁺

refl⁺ : Reflexive _≈⁺_

sym⁺ : ∀ {l u} → l ≈⁺ u → u ≈⁺ l

trans⁺ : ∀ l {m u} → l <⁺ m → m <⁺ u → l <⁺ u
trans⁺ l = AddExtremaToOrder.<±-trans _<_ trans

irrefl⁺ : ∀ k → ¬ (k <⁺ k)
irrefl⁺ k = AddExtremaToOrder.<±-irrefl _<_ irrefl refl⁺

-- Bundle

strictPartialOrder : StrictPartialOrder _ _ _
strictPartialOrder = record
{ isStrictPartialOrder = AddExtremaToOrder.<±-isStrictPartialOrder STO._<_ STO.isStrictPartialOrder
} where module STO = StrictTotalOrder sto

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
{ isStrictTotalOrder = AddExtremaToOrder.<±-isStrictTotalOrder STO._<_ STO.isStrictTotalOrder
} where module STO = StrictTotalOrder sto
```