Minor tidying up of CHANGELOG and prep for v2.2-rc1 (#2540)

* Minor changes to CHANGELOG and prep for v2.2-rc1

* Fix James' comment

Author: MatthewDaggitt

CHANGELOG.md

@@ -1,41 +1,41 @@
-Version 2.2-dev
-===============
+Version 2.2
+===========
 
-The library has been tested using Agda 2.7.0.
+The library has been tested using Agda 2.7.0 and 2.7.0.1.
 
 Highlights
 ----------
 
+* Added missing morphisms between the more advanced algebraic structures.
+
+* Added many missing lemmas about positive and negative rational numbers.
+
 Bug-fixes
 ---------
 
-* Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`.
+* Made the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality` more general.
   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.
+  `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily required
+  `x` and `y` to have the same type, making them unusable in many situations.
 
 * Removed unnecessary parameter `#-trans : Transitive _#_` from
   `Relation.Binary.Reasoning.Base.Apartness`.
 
+* The `IsSemiringWithoutOne` record no longer incorrectly exposes the `Carrier` field
+  inherited from `Setoid` when opening the record publicly.
+
 Non-backwards compatible changes
 --------------------------------
 
-* 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
-  better correspond to other algebraic structures. In particular:
-  * `Carrier` is no longer exposed.
-  * Several laws have been re-exposed from `IsCommutativeMonoid +` renaming
-    them to name the operation `+`.
-  * `distribˡ` and `distribʳ` are defined in the record.
+* 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 majority of uses, and would only be non-backwards compatible if for some reason you were explicitly supplying these implicit parameters when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.
 
-* [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.
+* [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. This should be a backwards compatible change for the majority of uses, but the change in parametrisation means that these patterns are *not* necessarily well-formed if the old implicit arguments `m`,`n` are supplied explicitly.
 
 Minor improvements
 ------------------
 
+* 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.
+
 Deprecated modules
 ------------------
 
@@ -111,7 +111,7 @@ New modules
 -----------
 
 * Consequences of module monomorphisms
-  ```agda
+  ```
   Algebra.Module.Morphism.BimoduleMonomorphism
   Algebra.Module.Morphism.BisemimoduleMonomorphism
   Algebra.Module.Morphism.LeftModuleMonomorphism
@@ -128,36 +128,28 @@ New modules
   ```
 
 * 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:
-  ```agda
+  ```
   Algebra.Solver.CommutativeMonoid.Normal
   Algebra.Solver.IdempotentCommutativeMonoid.Normal
   Algebra.Solver.Monoid.Expression
   Algebra.Solver.Monoid.Normal
   Algebra.Solver.Monoid.Solver
   ```
-
   NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
 
-* `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 _↭_ ⟶ _≡_
-  ```
 
-* 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
+* Properties of list permutations that require the `--with-K` flag:
+  ```
+  Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK
   ```
 
 * Refactored `Data.Refinement` into:
@@ -166,15 +158,17 @@ New modules
   Data.Refinement.Properties
   ```
 
-* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`
-
-* `Effect.Foldable`: implementation of haskell-like `Foldable`
+* Added implementation of Haskell-like `Foldable`:
+  ```agda
+  Effect.Foldable
+  Data.List.Effectful.Foldable
+  Data.Vec.Effectful.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`.
 
 Additions to existing modules
 -----------------------------
@@ -271,6 +265,19 @@ Additions to existing modules
   isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
   ```
 
+* In `Algebra.Structures.IsSemiringWithoutOne`:
+  ```agda
+  distribˡ : * DistributesOverˡ +
+  distribʳ : * DistributesOverʳ +
+  +-cong : Congruent +
+  +-congˡ : LeftCongruent +
+  +-congʳ : RightCongruent +
+  +-assoc : Associative +
+  +-identity : Identity 0# +
+  +-identityˡ : LeftIdentity 0# +
+  +-identityʳ : RightIdentity 0# +
+  ```
+
 * Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
@@ -338,9 +345,7 @@ Additions to existing modules
   concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   filter-≐     : P ≐ Q → filter P? ≗ filter Q?
 
-  partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then Product.map₁ (x ∷_)
-                                                                  else Product.map₂ (x ∷_))
-                                            ([] , [])
+  partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then map₁ (x ∷_) else map₂ (x ∷_)) ([] , [])
   ```
 
 * In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
@@ -386,6 +391,7 @@ Additions to existing modules
   ∈-resp-[σ∘σ⁻¹]   : (σ : xs ↭ ys) (iy : y ∈ ys) →
                      ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
   product-↭        : product Preserves _↭_ ⟶ _≡_
+  sum-↭ : sum Preserves _↭_ ⟶ _≡_
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
@@ -595,6 +601,8 @@ Additions to existing modules
   ```
   plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure.
 
+* In `Relation.Binary.Bundles` added `rawX` (e.g. `RawSetoid`) fields to each bundle.
+
 * In `Relation.Nullary.Decidable`:
   ```agda
   does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?

LICENCE

@@ -1,4 +1,4 @@
-Copyright (c) 2007-2024 Nils Anders Danielsson, Ulf Norell, Shin-Cheng
+Copyright (c) 2007-2025 Nils Anders Danielsson, Ulf Norell, Shin-Cheng
 Mu, Bradley Hardy, Samuel Bronson, Dan Doel, Patrik Jansson,
 Liang-Ting Chen, Jean-Philippe Bernardy, Andrés Sicard-Ramírez,
 Nicolas Pouillard, Darin Morrison, Peter Berry, Daniel Brown,

doc/installation-guide.md

@@ -3,19 +3,19 @@ Installation instructions
 
 Note: the full story on installing Agda libraries can be found at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html).
 
-Use version v2.1.1 of the standard library with Agda 2.7.0. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
+Use version v2.2 of the standard library with Agda v2.7.0 or v2.7.0.1. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where
    you would like to install the library.
 
-2. Download the tarball of v2.1.1 of the standard library. This can either be
+2. Download the tarball of v2.2 of the standard library. This can either be
    done manually by visiting the Github repository for the library, or via the
    command line as follows:
    ```
-   wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.1.1.tar.gz
+   wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.2.tar.gz
    ```
    Note that you can replace `wget` with other popular tools such as `curl` and that
-   you can replace `2.1.1` with any other version of the library you desire.
+   you can replace `2.2` with any other version of the library you desire.
 
 3. Extract the standard library from the tarball. Again this can either be
    done manually or via the command line as follows:
@@ -26,7 +26,7 @@ Use version v2.1.1 of the standard library with Agda 2.7.0. You can find the cor
 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run
    the commands to install via cabal:
    ```
-   cd agda-stdlib-2.1.1
+   cd agda-stdlib-2.2
    cabal install
    ```
 
@@ -42,7 +42,7 @@ Use version v2.1.1 of the standard library with Agda 2.7.0. You can find the cor
 6. Register the standard library with Agda's package system by adding
    the following line to `$AGDA_DIR/libraries`:
    ```
-   $HERE/agda-stdlib-2.1.1/standard-library.agda-lib
+   $HERE/agda-stdlib-2.2/standard-library.agda-lib
    ```
 
 Now, the standard library is ready to be used either: