rebase

merge

Author: jmougeot

CHANGELOG.md

@@ -183,9 +183,13 @@ New modules
 
 * `Relation.Nullary.Recomputable.Core`
 
-* `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+Additions to existing modules
 -----------------------------
 
+* `Algebra.Properties.Monoid` adding consequences for identity for monoids
+
+* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+
 * In `Algebra.Consequences.Base`:
   ```agda
   module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)