    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An implementation of insertion sort and its properties
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (DecTotalOrder)

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

    open import Data.List.Sort.InsertionSort.Base O public
    open import Data.List.Sort.InsertionSort.Properties O using (insertionSort) public