{-# 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
record SortingAlgorithm : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
sort : List A → List A
sort-↭ : ∀ xs → sort xs ↭ xs
sort-↗ : ∀ xs → Sorted (sort xs)
sort-↭ₛ : ∀ xs → sort xs S.↭ xs
sort-↭ₛ xs = Homo.map Eq.reflexive (↭⇒↭ₛ (sort-↭ xs))