[ fix ] tidy up alphabetical ordering in CHANGELOG (agda#2538)

* tidy up alphabetical ordering

* refactor: more comprehensive overhaul

Author: jamesmckinna

CHANGELOG.md

@@ -9,18 +9,17 @@ Highlights
 Bug-fixes
 ---------
 
-* Removed unnecessary parameter `#-trans : Transitive _#_` from
-  `Relation.Binary.Reasoning.Base.Apartness`.
 * Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`.
   These operators are used for equational reasoning of heterogeneous equality
   `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
   `x` and `y` to have the same type, making them unusable in most situations.
 
+* Removed unnecessary parameter `#-trans : Transitive _#_` from
+  `Relation.Binary.Reasoning.Base.Apartness`.
+
 Non-backwards compatible changes
 --------------------------------
 
-* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
-
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.
 
 * The names exposed by the `IsSemiringWithoutOne` record have been altered to
@@ -32,6 +31,8 @@ Non-backwards compatible changes
 
 * [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) and [issue #2519](https://github.com/agda/agda-stdlib/issues/2510) In `Data.Nat.Base` the definitions of `_≤′_` and `_≤‴_` have been modified to make the witness to equality explicit in new constructors `≤′-reflexive` and `≤‴-reflexive`; pattern synonyms `≤′-refl` and `≤‴-refl` have been added for backwards compatibility but NB. the change in parametrisation means that these patterns are *not* necessarily well-formed if the old implicit arguments `m`,`n` are supplied explicitly.
 
+* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
+
 Minor improvements
 ------------------
 
@@ -109,16 +110,6 @@ Deprecated names
 New modules
 -----------
 
-* Bundled morphisms between (raw) algebraic structures:
-  ```
-  Algebra.Morphism.Bundles
-  ```
-
-* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
-  ```agda
-  Algebra.Properties.IdempotentCommutativeMonoid
-  ```
-
 * Consequences of module monomorphisms
   ```agda
   Algebra.Module.Morphism.BimoduleMonomorphism
@@ -131,6 +122,16 @@ New modules
   Algebra.Module.Morphism.SemimoduleMonomorphism
   ```
 
+* Bundled morphisms between (raw) algebraic structures:
+  ```
+  Algebra.Morphism.Bundles
+  ```
+
+* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
+  ```agda
+  Algebra.Properties.IdempotentCommutativeMonoid
+  ```
+
 * Refactoring of the `Algebra.Solver.*Monoid` implementations, via
   a single `Solver` module API based on the existing `Expr`, and
   a common `Normal`-form API:
@@ -144,37 +145,37 @@ New modules
 
   NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
 
-* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
-  ```agda
-  Data.List.Relation.Unary.All.Properties.Core
-  ```
+* `Data.List.Effectful.Foldable`: `List` is `Foldable`
 
 * `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
   Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
   ```agda
   sum-↭ : sum Preserves _↭_ ⟶ _≡_
   ```
 
-* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
+* Added `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
+
+* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  Data.List.Relation.Unary.All.Properties.Core
+  ```
 
 * Refactored `Data.Refinement` into:
   ```agda
   Data.Refinement.Base
   Data.Refinement.Properties
   ```
 
+* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`
+
+* `Effect.Foldable`: implementation of haskell-like `Foldable`
+
 * Raw bundles for the `Relation.Binary.Bundles` hierarchy:
   ```agda
   Relation.Binary.Bundles.Raw
   ```
   plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.
 
-* `Data.List.Effectful.Foldable`: `List` is `Foldable`
-
-* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`
-
-* `Effect.Foldable`: implementation of haskell-like `Foldable`
-
 Additions to existing modules
 -----------------------------
 
@@ -292,22 +293,6 @@ Additions to existing modules
   isNearSemiring      : IsNearSemiring _ _
  ```
 
-* In `Data.List.Membership.Setoid.Properties`:
-  ```agda
-  ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs
-  All[≉]⇒∉       : All (x ≉_) xs → x ∉ xs
-  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
-  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
-  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
-  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
-                   ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
-                   y ∈₂ map f (filter P? xs)
-  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
-  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
-  ∉[]            : x ∉ []
-  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
-  ```
-
 * In `Data.List.Membership.Propositional.Properties`:
   ```agda
   ∈-AllPairs₂    : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
@@ -329,6 +314,22 @@ Additions to existing modules
   unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
   ```
 
+* In `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs
+  All[≉]⇒∉       : All (x ≉_) xs → x ∉ xs
+  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
+  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
+  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
+  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
+                   ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
+                   y ∈₂ map f (filter P? xs)
+  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   product≢0    : All NonZero ns → NonZero (product ns)
@@ -342,37 +343,14 @@ Additions to existing modules
                                             ([] , [])
   ```
 
-* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
-  ```agda
-  ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
-  ```agda
-  concat⁺    : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
-  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
-  ```
-
-* In `Data.List.Relation.Unary.All.Properties`:
-  ```agda
-  all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
-  all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
-  ```
-
-* In `Data.List.Relation.Unary.Any.Properties`:
-  ```agda
-  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
-  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
-  ```
-
-* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
+* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
   ```agda
-  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
+  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
   ```
 
-* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
+* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
   ```agda
-  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
+  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
   ```
 
 * In `Data.List.Relation.Binary.Equality.Setoid`:
@@ -410,6 +388,12 @@ Additions to existing modules
   product-↭        : product Preserves _↭_ ⟶ _≡_
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
+  ```agda
+  dedup-++-↭ : Disjoint xs ys →
+               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Setoid`:
   ```agda
   ↭-reflexive-≋ : _≋_  ⇒ _↭_
@@ -431,60 +415,71 @@ Additions to existing modules
   ++⁺ʳ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
-* In `Data.List.Relation.Unary.All`:
+* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
   ```agda
-  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
- ```
+  Sublist-[]-universal : Universal (Sublist R [])
+  ```
 
-* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
+* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
   ```agda
-  ∷⊈[]   : x ∷ xs ⊈ []
-  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+  ```agda
+  []⊆-universal : Universal ([] ⊆_)
+
+  concat⁺    : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
+  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
   ```
 
 * In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
   ∷⊈[]   : x ∷ xs ⊈ []
   ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
   ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+
+  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
   ```
 
-* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda
-  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+  ∷⊈[]   : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
   ```
 
-* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
+* In `Data.List.Relation.Unary.First.Properties`:
   ```agda
-  Sublist-[]-universal : Universal (Sublist R [])
+  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
+  ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
   ```
 
-* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+* In `Data.List.Relation.Unary.All`:
   ```agda
-  []⊆-universal : Universal ([] ⊆_)
+  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
   ```
 
-* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
+* In `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
+  all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
   ```
 
-* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+* In `Data.List.Relation.Unary.Any.Properties`:
   ```agda
-  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
+  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
   ```
 
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
+* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
   ```agda
-  dedup-++-↭ : Disjoint xs ys →
-               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
+  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
   ```
 
-* In `Data.List.Relation.Unary.First.Properties`:
+* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
   ```agda
-  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
-  ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
   ```
 
 * In `Data.Maybe.Properties`:
@@ -503,7 +498,7 @@ Additions to existing modules
   ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
   ```
 
-  adjunction between `suc` and `pred`
+  Added adjunction between `suc` and `pred`
   ```agda
   suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
   m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n