    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The core definition of a sorting algorithm
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (TotalOrder)

    module Data.List.Sort.Base
      {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂)
      where

    open import Data.List.Base using (List)
    open import Data.List.Relation.Binary.Permutation.Propositional
      using (_↭_; ↭⇒↭ₛ)
    import Data.List.Relation.Binary.Permutation.Homogeneous as Homo
    open import Level using (_⊔_)

    open TotalOrder totalOrder renaming (Carrier to A)
    open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder
    import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid as S

    ------------------------------------------------------------------------
    -- Definition of a sorting algorithm

    record SortingAlgorithm : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        sort   : List A → List A

        -- The output of `sort` is a propositional permutation of the input.
        -- Note that the choice of using a propositional equality here
        -- is very deliberate. A sorting algorithm should only be capable
        -- of altering the order of the elements of the list, and should not
        -- be capable of altering the elements themselves in any way.
        sort-↭ : ∀ xs → sort xs ↭ xs

        -- The output of `sort` is sorted.
        sort-↗ : ∀ xs → Sorted (sort xs)

      -- Lists are also permutations under the setoid versions of
      -- permutation.
      sort-↭ₛ : ∀ xs → sort xs S.↭ xs
      sort-↭ₛ xs = Homo.map Eq.reflexive (↭⇒↭ₛ (sort-↭ xs))