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

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

    open import Relation.Binary.Bundles using (DecTotalOrder)

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

    open import Data.Bool.Base using (if_then_else_)
    open import Data.List.Base using (List; []; _∷_)
    open import Relation.Nullary.Decidable.Core using (does)

    open DecTotalOrder O renaming (Carrier to A)

    ------------------------------------------------------------------------
    -- Definitions

    insert : A → List A → List A
    insert x [] = x ∷ []
    insert x (y ∷ xs) = if does (x ≤? y)
      then x ∷ y ∷ xs
      else y ∷ insert x xs

    sort : List A → List A
    sort [] = []
    sort (x ∷ xs) = insert x (sort xs)