Bogus commits have entered the picture.

Revert "added `CommutativeRing` to the tally"

This reverts commit 5baffde.

Author: jamesmckinna

CHANGELOG.md

@@ -1602,9 +1602,7 @@ Other minor changes
   zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
   distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
   isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
-  isCommutativeRing : IsCommutativeRing ≈ + * - 0# 1# → IsCommutativeRing ≈ + (flip *) - 0# 1#
   ring : Ring a ℓ → Ring a ℓ
-  commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
   ```
 
 * Added new definition to `Algebra.Definitions`:

src/Algebra/Construct/Flip/Op.agda

@@ -200,14 +200,6 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
     where
       module r = IsRing r
 
-  isCommutativeRing : IsCommutativeRing + * - 0# 1# → IsCommutativeRing + (flip *) - 0# 1#
-  isCommutativeRing r = record
-    { isRing = isRing r.isRing
-    ; *-comm = commutative r.*-comm
-    }
-    where
-      module r = IsCommutativeRing r
-
 
 ------------------------------------------------------------------------
 -- Bundles
@@ -290,7 +282,3 @@ ring : Ring a ℓ → Ring a ℓ
 ring r = record { isRing = isRing r.isRing }
   where module r = Ring r
 
-commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
-commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing }
-  where module r = CommutativeRing r
-