    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Lexicographic ordering of lists
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Binary.Lex.Core where

    open import Data.Empty using (⊥)
    open import Data.Unit.Base using (⊤)
    open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
    open import Data.List.Base using (List; []; _∷_)
    open import Function.Base using (_∘_; flip; id)
    open import Level using (Level; _⊔_)
    open import Relation.Nullary.Negation.Core using (¬_)
    open import Relation.Binary.Core using (Rel)
    open import Data.List.Relation.Binary.Pointwise.Base
       using (Pointwise; []; _∷_; head; tail)

    private
      variable
        a ℓ₁ ℓ₂ : Level

    -- The lexicographic ordering itself can be either strict or non-strict,
    -- depending on whether type P is inhabited.

    data Lex {A : Set a} (P : Set)
             (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) :
             Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂) where
      base : P                             → Lex P _≈_ _≺_ []       []
      halt : ∀ {y ys}                      → Lex P _≈_ _≺_ []       (y ∷ ys)
      this : ∀ {x xs y ys} (x≺y : x ≺ y)   → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
      next : ∀ {x xs y ys} (x≈y : x ≈ y)
             (xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)

    ------------------------------------------------------------------------
    -- Lexicographic orderings, using a strict ordering as the base

    Lex-< : {A : Set a} (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
            Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
    Lex-< = Lex ⊥

    Lex-≤ : {A : Set a} (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
            Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
    Lex-≤ = Lex ⊤