diff --git a/CHANGELOG.md b/CHANGELOG.md
index 14e75e9ca5..f77e525b85 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -163,6 +163,10 @@ New modules
 
 * `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
 
+* `Data.List.Sort.InsertionSort.{agda|Base|Properties}` defines insertion sort and proves properties of insertion sort such as Sorted and Permutation properties.
+
+* `Data.List.Sort.MergenSort.{agda|Base|Properties}` is a refactor of the previous `Data.List.Sort.MergenSort`.
+
 * `Data.Sign.Show` to show a sign.
 
 * `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`.
diff --git a/src/Data/List/Sort/InsertionSort.agda b/src/Data/List/Sort/InsertionSort.agda
new file mode 100644
index 0000000000..29c3795d5b
--- /dev/null
+++ b/src/Data/List/Sort/InsertionSort.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- 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
diff --git a/src/Data/List/Sort/InsertionSort/Base.agda b/src/Data/List/Sort/InsertionSort/Base.agda
new file mode 100644
index 0000000000..e153beda08
--- /dev/null
+++ b/src/Data/List/Sort/InsertionSort/Base.agda
@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- 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)
diff --git a/src/Data/List/Sort/InsertionSort/Properties.agda b/src/Data/List/Sort/InsertionSort/Properties.agda
new file mode 100644
index 0000000000..dc8c146344
--- /dev/null
+++ b/src/Data/List/Sort/InsertionSort/Properties.agda
@@ -0,0 +1,155 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of insertion sort
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (DecTotalOrder)
+
+module Data.List.Sort.InsertionSort.Properties
+  {a ℓ₁ ℓ₂}
+  (O : DecTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Bool.Base using (true; false; if_then_else_)
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise using ([]; _∷_; decidable; setoid)
+open import Data.List.Relation.Binary.Permutation.Propositional
+import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
+open import Data.List.Relation.Unary.Linked using ([]; [-]; _∷_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Properties.DecTotalOrder O using (≰⇒≥)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
+
+open DecTotalOrder O renaming (Carrier to A; trans to ≤-trans)
+  using (totalOrder; _≤?_; _≤_; module Eq; _≈_; ≤-respʳ-≈; ≤-respˡ-≈; antisym)
+
+open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid
+  using (_≋_; ≋-refl; ≋-sym; ≋-trans)
+open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted)
+open import Data.List.Sort.Base totalOrder using (SortingAlgorithm)
+open import Data.List.Sort.InsertionSort.Base O
+import Relation.Binary.Reasoning.Setoid (setoid Eq.setoid) as ≋-Reasoning
+
+------------------------------------------------------------------------
+-- Permutation property
+
+insert-↭ : ∀ x xs → insert x xs ↭ x ∷ xs
+insert-↭ x [] = ↭-refl
+insert-↭ x (y ∷ xs) with does (x ≤? y)
+... | true  = ↭-refl
+... | false = begin
+  y ∷ insert x xs ↭⟨ prep y (insert-↭ x xs) ⟩
+  y ∷ x ∷ xs      ↭⟨ swap y x refl ⟩
+  x ∷ y ∷ xs ∎
+  where open PermutationReasoning
+
+insert-cong-↭ : ∀ {x xs ys} → xs ↭ ys → insert x xs ↭ x ∷ ys
+insert-cong-↭ {x} {xs} {ys} eq = begin
+  insert x xs ↭⟨ insert-↭ x xs ⟩
+  x ∷ xs      ↭⟨ prep x eq ⟩
+  x ∷ ys ∎
+  where open PermutationReasoning
+
+sort-↭ : ∀ (xs : List A) → sort xs ↭ xs
+sort-↭ [] = ↭-refl
+sort-↭ (x ∷ xs) = insert-cong-↭ (sort-↭ xs)
+
+------------------------------------------------------------------------
+-- Sorted property
+
+insert-↗ : ∀ x {xs} → Sorted xs → Sorted (insert x xs)
+insert-↗ x [] = [-]
+insert-↗ x ([-] {y}) with x ≤? y
+... | yes x≤y = x≤y ∷ [-]
+... | no  x≰y = ≰⇒≥ x≰y ∷ [-]
+insert-↗ x (_∷_ {y} {z} {ys} y≤z z≤ys) with x ≤? y
+... | yes x≤y = x≤y ∷ y≤z ∷ z≤ys
+... | no  x≰y with ih ← insert-↗ x z≤ys | x ≤? z
+... | yes _ = ≰⇒≥ x≰y ∷ ih
+... | no  _ = y≤z ∷ ih
+
+sort-↗ : ∀ xs → Sorted (sort xs)
+sort-↗ [] = []
+sort-↗ (x ∷ xs) = insert-↗ x (sort-↗ xs)
+
+------------------------------------------------------------------------
+-- Algorithm
+
+insertionSort : SortingAlgorithm
+insertionSort = record
+  { sort   = sort
+  ; sort-↭ = sort-↭
+  ; sort-↗ = sort-↗
+  }
+
+------------------------------------------------------------------------
+-- Congruence properties
+
+insert-congʳ : ∀ z {xs ys} → xs ≋ ys → insert z xs ≋ insert z ys
+insert-congʳ z [] = ≋-refl
+insert-congʳ z (_∷_ {x} {y} {xs} {ys} x∼y eq) with z ≤? x | z ≤? y
+... | yes  _  | yes  _  = Eq.refl ∷ x∼y ∷ eq
+... | no  z≰x | yes z≤y = contradiction (≤-respʳ-≈ (Eq.sym x∼y) z≤y) z≰x
+... | yes z≤x | no  z≰y = contradiction (≤-respʳ-≈ x∼y z≤x) z≰y
+... | no   _  | no   _  = x∼y ∷ insert-congʳ z eq
+
+insert-congˡ : ∀ {x y} xs → x ≈ y → insert x xs ≋ insert y xs
+insert-congˡ {x} {y} [] eq = eq ∷ []
+insert-congˡ {x} {y} (z ∷ xs) eq with x ≤? z | y ≤? z
+... | yes  _  | yes  _  = eq ∷ ≋-refl
+... | no  x≰z | yes y≤z = contradiction (≤-respˡ-≈ (Eq.sym eq) y≤z) x≰z
+... | yes x≤z | no  y≰z = contradiction (≤-respˡ-≈ eq x≤z) y≰z
+... | no   _  | no   _  = Eq.refl ∷ insert-congˡ xs eq
+
+insert-cong : ∀ {x y xs ys} → x ≈ y → xs ≋ ys → insert x xs ≋ insert y ys
+insert-cong {y = y} {xs} eq₁ eq₂ = ≋-trans (insert-congˡ xs eq₁) (insert-congʳ y eq₂)
+
+sort-cong : ∀ {xs ys} → xs ≋ ys → sort xs ≋ sort ys
+sort-cong [] = []
+sort-cong (x∼y ∷ eq) = insert-cong x∼y (sort-cong eq)
+
+private
+  insert-swap-≤ : ∀ {x y} xs → x ≤ y → insert x (insert y xs) ≋ insert y (insert x xs)
+  insert-swap-≤ {x} {y} [] x≤y with x ≤? y
+  ... | no  xy = contradiction x≤y xy
+  ... | yes xy with y ≤? x
+  ... | yes yx = Eq.sym eq ∷ eq ∷ [] where eq = antisym yx xy
+  ... | no  _  = ≋-refl
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y with y ≤? z
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz with x ≤? y
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy with x ≤? z
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz with y ≤? x
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | yes yx =
+    Eq.sym eq ∷ eq ∷ ≋-refl where eq = antisym yx xy
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | no yx with y ≤? z
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | no yx | yes yz' = ≋-refl
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | yes xz | no yx | no  yz' = contradiction yz yz'
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | yes xy | no xz = contradiction (≤-trans xy yz) xz
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | yes yz | no xy = contradiction x≤y xy
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz with x ≤? z
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | yes xz with y ≤? x
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | yes xz | yes yx = contradiction (≤-trans yx xz) yz
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | yes xz | no  yx with y ≤? z
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | yes xz | no  yx | yes yz' = contradiction yz' yz
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | yes xz | no  yx | no yz' = ≋-refl
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | no  xz with y ≤? z
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | no  xz | yes yz' = contradiction yz' yz
+  insert-swap-≤ {x} {y} (z ∷ xs) x≤y | no  yz | no  xz | no  yz' = Eq.refl ∷ (insert-swap-≤ xs x≤y)
+
+insert-swap : ∀ x y xs → insert x (insert y xs) ≋ insert y (insert x xs)
+insert-swap x y xs with x ≤? y
+... | yes x≤y = insert-swap-≤ xs x≤y
+... | no  x≰y = ≋-sym (insert-swap-≤ xs (≰⇒≥ x≰y))
+
+insert-swap-cong : ∀ {x y x′ y′ xs ys} → x ≈ x′ → y ≈ y′ → xs ≋ ys →
+                   insert x (insert y xs) ≋ insert y′ (insert x′ ys)
+insert-swap-cong {x} {y} {x′} {y′} {xs} {ys} eq₁ eq₂ eq₃ = begin
+  insert x (insert y xs)   ≈⟨ insert-cong eq₁ (insert-cong eq₂ eq₃) ⟩
+  insert x′ (insert y′ ys) ≈⟨ insert-swap x′ y′ ys ⟩
+  insert y′ (insert x′ ys) ∎
+  where open ≋-Reasoning
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index 2c4a67b951..f3c1f64d6d 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -15,104 +15,5 @@ open import Relation.Binary.Bundles using (DecTotalOrder)
 module Data.List.Sort.MergeSort
   {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
 
-open import Data.Bool.Base using (true; false)
-open import Data.List.Base
-  using (List; []; _∷_; merge; length; map; [_]; concat; _++_)
-open import Data.List.Properties using (length-partition; ++-assoc; concat-map-[_])
-open import Data.List.Relation.Unary.Linked using ([]; [-])
-import Data.List.Relation.Unary.Sorted.TotalOrder.Properties as Sorted
-open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
-import Data.List.Relation.Unary.All.Properties as All
-open import Data.List.Relation.Binary.Permutation.Propositional
-import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
-open import Data.Maybe.Base using (just)
-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 import Data.Product.Base as Product using (_,_)
-open import Function.Base using (_∘_)
-open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Nullary.Decidable.Core using (does)
-
-open DecTotalOrder O renaming (Carrier to A)
-
-open import Data.List.Sort.Base totalOrder
-open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder hiding (head)
-open import Relation.Binary.Properties.DecTotalOrder O using (≰⇒≥; ≰-respˡ-≈)
-
-open PermutationReasoning
-
-------------------------------------------------------------------------
--- 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 _)
-
-------------------------------------------------------------------------
--- Permutation property
-
-mergePairs-↭ : ∀ xss → concat (mergePairs xss) ↭ concat xss
-mergePairs-↭ []              = ↭-refl
-mergePairs-↭ (xs ∷ [])       = ↭-refl
-mergePairs-↭ (xs ∷ ys ∷ xss) = begin
-  merge _ xs ys ++ concat (mergePairs xss) ↭⟨ Perm.++⁺ (Perm.merge-↭ _ xs ys) (mergePairs-↭ xss) ⟩
-  (xs ++ ys)    ++ concat xss              ≡⟨ ++-assoc xs ys (concat xss) ⟩
-  xs ++ ys      ++ concat xss              ∎
-
-mergeAll-↭ : ∀ xss (rec : Acc _<_ (length xss)) → mergeAll xss rec ↭ concat xss
-mergeAll-↭ []              _ = ↭-refl
-mergeAll-↭ (xs ∷ [])       _ = ↭-sym (Perm.++-identityʳ xs)
-mergeAll-↭ (xs ∷ ys ∷ xss) (acc rec) = begin
-  mergeAll (mergePairs (xs ∷ ys ∷ xss)) _ ↭⟨ mergeAll-↭ (mergePairs (xs ∷ ys ∷ xss)) _ ⟩
-  concat   (mergePairs (xs ∷ ys ∷ xss))   ↭⟨ mergePairs-↭ (xs ∷ ys ∷ xss) ⟩
-  concat   (xs ∷ ys ∷ xss)                ∎
-
-sort-↭ : ∀ xs → sort xs ↭ xs
-sort-↭ xs = begin
-  mergeAll (map [_] xs) _ ↭⟨ mergeAll-↭ (map [_] xs) _ ⟩
-  concat (map [_] xs)     ≡⟨ concat-map-[ xs ] ⟩
-  xs                      ∎
-
-------------------------------------------------------------------------
--- Sorted property
-
-mergePairs-↗ : ∀ {xss} → All Sorted xss → All Sorted (mergePairs xss)
-mergePairs-↗ []                 = []
-mergePairs-↗ (xs↗ ∷ [])         = xs↗ ∷ []
-mergePairs-↗ (xs↗ ∷ ys↗ ∷ xss↗) = Sorted.merge⁺ O xs↗ ys↗ ∷ mergePairs-↗ xss↗
-
-mergeAll-↗ : ∀ {xss} (rec : Acc _<_ (length xss)) →
-             All Sorted xss → Sorted (mergeAll xss rec)
-mergeAll-↗ rec       []                 = []
-mergeAll-↗ rec       (xs↗ ∷ [])         = xs↗
-mergeAll-↗ (acc rec) (xs↗ ∷ ys↗ ∷ xss↗) = mergeAll-↗ _ (mergePairs-↗ (xs↗ ∷ ys↗ ∷ xss↗))
-
-sort-↗ : ∀ xs → Sorted (sort xs)
-sort-↗ xs = mergeAll-↗ _ (All.map⁺ (All.universal (λ _ → [-]) xs))
-
-------------------------------------------------------------------------
--- Algorithm
-
-mergeSort : SortingAlgorithm
-mergeSort = record
-  { sort   = sort
-  ; sort-↭ = sort-↭
-  ; sort-↗ = sort-↗
-  }
+open import Data.List.Sort.MergeSort.Base O public
+open import Data.List.Sort.MergeSort.Properties O using (mergeSort) public
diff --git a/src/Data/List/Sort/MergeSort/Base.agda b/src/Data/List/Sort/MergeSort/Base.agda
new file mode 100644
index 0000000000..c81695fc1f
--- /dev/null
+++ b/src/Data/List/Sort/MergeSort/Base.agda
@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- 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 _)
diff --git a/src/Data/List/Sort/MergeSort/Properties.agda b/src/Data/List/Sort/MergeSort/Properties.agda
new file mode 100644
index 0000000000..c94e5b7eb0
--- /dev/null
+++ b/src/Data/List/Sort/MergeSort/Properties.agda
@@ -0,0 +1,96 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An implementation of merge sort along with proofs of correctness.
+------------------------------------------------------------------------
+
+-- 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.Properties
+  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
+
+open import Data.Bool.Base using (true; false)
+open import Data.List.Base
+  using (List; []; _∷_; merge; length; map; [_]; concat; _++_)
+open import Data.List.Properties using (length-partition; ++-assoc; concat-map-[_])
+open import Data.List.Relation.Unary.Linked using ([]; [-])
+import Data.List.Relation.Unary.Sorted.TotalOrder.Properties as Sorted
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+import Data.List.Relation.Unary.All.Properties as All
+open import Data.List.Relation.Binary.Permutation.Propositional
+import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
+open import Data.Maybe.Base using (just)
+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 import Data.Product.Base as Product using (_,_)
+open import Function.Base using (_∘_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core using (does)
+
+open DecTotalOrder O renaming (Carrier to A)
+
+open import Data.List.Sort.Base totalOrder
+open import Data.List.Sort.MergeSort.Base O
+open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder hiding (head)
+open import Relation.Binary.Properties.DecTotalOrder O using (≰⇒≥; ≰-respˡ-≈)
+
+open PermutationReasoning
+
+------------------------------------------------------------------------
+-- Permutation property
+
+mergePairs-↭ : ∀ xss → concat (mergePairs xss) ↭ concat xss
+mergePairs-↭ []              = ↭-refl
+mergePairs-↭ (xs ∷ [])       = ↭-refl
+mergePairs-↭ (xs ∷ ys ∷ xss) = begin
+  merge _ xs ys ++ concat (mergePairs xss) ↭⟨ Perm.++⁺ (Perm.merge-↭ _ xs ys) (mergePairs-↭ xss) ⟩
+  (xs ++ ys)    ++ concat xss              ≡⟨ ++-assoc xs ys (concat xss) ⟩
+  xs ++ ys      ++ concat xss              ∎
+
+mergeAll-↭ : ∀ xss (rec : Acc _<_ (length xss)) → mergeAll xss rec ↭ concat xss
+mergeAll-↭ []              _ = ↭-refl
+mergeAll-↭ (xs ∷ [])       _ = ↭-sym (Perm.++-identityʳ xs)
+mergeAll-↭ (xs ∷ ys ∷ xss) (acc rec) = begin
+  mergeAll (mergePairs (xs ∷ ys ∷ xss)) _ ↭⟨ mergeAll-↭ (mergePairs (xs ∷ ys ∷ xss)) _ ⟩
+  concat   (mergePairs (xs ∷ ys ∷ xss))   ↭⟨ mergePairs-↭ (xs ∷ ys ∷ xss) ⟩
+  concat   (xs ∷ ys ∷ xss)                ∎
+
+sort-↭ : ∀ xs → sort xs ↭ xs
+sort-↭ xs = begin
+  mergeAll (map [_] xs) _ ↭⟨ mergeAll-↭ (map [_] xs) _ ⟩
+  concat (map [_] xs)     ≡⟨ concat-map-[ xs ] ⟩
+  xs                      ∎
+
+------------------------------------------------------------------------
+-- Sorted property
+
+mergePairs-↗ : ∀ {xss} → All Sorted xss → All Sorted (mergePairs xss)
+mergePairs-↗ []                 = []
+mergePairs-↗ (xs↗ ∷ [])         = xs↗ ∷ []
+mergePairs-↗ (xs↗ ∷ ys↗ ∷ xss↗) = Sorted.merge⁺ O xs↗ ys↗ ∷ mergePairs-↗ xss↗
+
+mergeAll-↗ : ∀ {xss} (rec : Acc _<_ (length xss)) →
+             All Sorted xss → Sorted (mergeAll xss rec)
+mergeAll-↗ rec       []                 = []
+mergeAll-↗ rec       (xs↗ ∷ [])         = xs↗
+mergeAll-↗ (acc rec) (xs↗ ∷ ys↗ ∷ xss↗) = mergeAll-↗ _ (mergePairs-↗ (xs↗ ∷ ys↗ ∷ xss↗))
+
+sort-↗ : ∀ xs → Sorted (sort xs)
+sort-↗ xs = mergeAll-↗ _ (All.map⁺ (All.universal (λ _ → [-]) xs))
+
+------------------------------------------------------------------------
+-- Algorithm
+
+mergeSort : SortingAlgorithm
+mergeSort = record
+  { sort   = sort
+  ; sort-↭ = sort-↭
+  ; sort-↗ = sort-↗
+  }