[ doc ] changelog

Author: laMudri

CHANGELOG.md

@@ -20,6 +20,62 @@ Non-backwards compatible changes
   Definitions that are sensitive to the behaviour of these lemmas, rather than
   just their existence, may need to be revised.
 
+* The following record definitions in `Algebra.Structures` have been changed.
+
+  - `IsCommutativeMonoid`
+  - `IsCommutativeSemiring`
+  - `IsRing`
+
+  In all of these cases, the change has been to give each of these structures
+  access to *all* of the fields of structures below (weaker) in the hierarchy.
+  For example, consider `IsCommutativeMonoid`. The old definition effectively
+  required the following fields.
+
+  - Associativity
+  - Left identity
+  - Commutativity
+
+  The new definition also requires:
+
+  - Right identity.
+
+  The justification for not including a right identity proof was that, given
+  left identity and commutativity, right identity can be proven. However,
+  omitting the right identity proof caused problems:
+
+  1. It made the definition longer and more complex, as less code was reused.
+  2. The forgetful map turning a commutative monoid into a monoid was not a
+     retraction of all maps which augment a monoid with commutativity. To see
+     that the forgetful map was not a retraction, notice that the augmentation
+     must have discarded the right identity proof as there was no field for it
+     in `IsCommutativeMonoid`.
+  3. There was no easy way to give only the right identity proof, and have
+     the left identity proof be generically derived.
+
+  Point 2, and in particular the fact that it did not hold definitionally,
+  caused problems when indexing over monoids and commutative monoids and
+  requiring some compatibility between the two indexings.
+
+  With the new definition, we address point 3 and recover the convenience of
+  the old definition simultaneously. We do this by introducing *biased*
+  structures, found in `Algebra.Structures.Biased`. In particular, one can
+  generally convert old instances of `IsCommutativeMonoid` to new instances
+  using the `IsCommutativeMonoidˡ` biased structure. This is introduced by
+  the function `isCommutativeMonoidˡ`, so old instances can be converted as
+  follows.
+
+  ```agda
+  --    Add this part:  ↓----↓----↓----↓----↓
+  isCommutativeMonoid = isCommutativeMonoidˡ record
+    { isSemigroup = ...  -- Everything
+    ; identityˡ   = ...  -- else is
+    ; comm        = ...  -- the same.
+    }
+  ```
+
+  For `IsCommutativeSemiring`, we have `IsCommutativeSemiringˡ`, and for
+  `IsRing`, we have `IsRingWithoutAnnihilatingZero`.
+
 Other major additions
 ---------------------