    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An implementation of merge sort
    ------------------------------------------------------------------------

    -- Unless you are need a particular property of MergeSort, you should
    -- import and use the sorting algorithm from `Data.List.Sort` instead
    -- of this file.

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

    open import Relation.Binary.Bundles using (DecTotalOrder)

    module Data.List.Sort.MergeSort.Base
      {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where

    open import Data.List.Base
      using (List; []; _∷_; merge; length; map; [_])

    open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
    open import Data.Nat.Induction
    open import Data.Nat.Properties using (m<n⇒m<1+n)

    open DecTotalOrder O renaming (Carrier to A)

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

    mergePairs : List (List A) → List (List A)
    mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
    mergePairs xss             = xss

    private
      length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in
                          length (mergePairs zss) < length zss
      length-mergePairs _ _ []              = s<s z<s
      length-mergePairs _ _ (xs ∷ [])       = s<s (s<s z<s)
      length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))

    mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
    mergeAll []        _               = []
    mergeAll (xs ∷ []) _               = xs
    mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
      (mergePairs xss) (rec (length-mergePairs xs ys yss))

    sort : List A → List A
    sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)