    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Sorted lists
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (TotalOrder)

    module Data.List.Relation.Unary.Sorted.TotalOrder
      {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where

    open TotalOrder totalOrder renaming (Carrier to A)

    open import Data.List.Base using (List; []; _∷_)
    open import Data.List.Relation.Unary.Linked as Linked using (Linked)
    open import Level using (_⊔_)
    open import Relation.Unary as U using (Pred; _⊆_)
    open import Relation.Binary.Definitions as B

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

    Sorted : Pred (List A) (a ⊔ ℓ₂)
    Sorted xs = Linked _≤_ xs

    ------------------------------------------------------------------------
    -- Operations

    module _ {x y xs} where

      head : Sorted (x ∷ y ∷ xs) → x ≤ y
      head = Linked.head

      tail : Sorted (x ∷ xs) → Sorted xs
      tail = Linked.tail

    ------------------------------------------------------------------------
    -- Properties of predicates preserved by Sorted

    sorted? : B.Decidable _≤_ → U.Decidable Sorted
    sorted? = Linked.linked?

    irrelevant : B.Irrelevant _≤_ → U.Irrelevant Sorted
    irrelevant = Linked.irrelevant

    satisfiable : U.Satisfiable Sorted
    satisfiable = Linked.satisfiable