Fixed commutativeSemigroup re-exports (#1174)

Author: MatthewDaggitt

CHANGELOG.md

@@ -15,6 +15,9 @@ Highlights
 Bug-fixes
 ---------
 
+* Fixed various algebraic bundles not correctly re-exporting
+  `commutativeSemigroup` proofs.
+
 Non-backwards compatible changes
 --------------------------------
 

src/Algebra/Bundles.agda

@@ -166,11 +166,11 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   semigroup : Semigroup _ _
   semigroup = record { isSemigroup = isSemigroup }
 
+  open Semigroup semigroup public using (rawMagma; magma)
+
   rawMonoid : RawMonoid _ _
   rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}
 
-  open Semigroup semigroup public using (rawMagma; magma)
-
 
 record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -187,11 +187,11 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
 
+  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
+
   commutativeSemigroup : CommutativeSemigroup _ _
   commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
 
-  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
-
 
 record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -291,8 +291,10 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
     using (rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
 
   commutativeMonoid : CommutativeMonoid _ _
-  commutativeMonoid =
-    record { isCommutativeMonoid = isCommutativeMonoid }
+  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+
+  open CommutativeMonoid commutativeMonoid public
+    using (commutativeSemigroup)
 
 
 ------------------------------------------------------------------------
@@ -357,8 +359,7 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   +-monoid = record { isMonoid = +-isMonoid }
 
   open Monoid +-monoid public
-    using ()
-    renaming
+    using () renaming
     ( rawMagma  to +-rawMagma
     ; magma     to +-magma
     ; semigroup to +-semigroup
@@ -369,8 +370,7 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   *-semigroup = record { isSemigroup = *-isSemigroup }
 
   open Semigroup *-semigroup public
-    using ()
-    renaming
+    using () renaming
     ( rawMagma to *-rawMagma
     ; magma    to *-magma
     )
@@ -395,13 +395,16 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open NearSemiring nearSemiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup; +-rawMonoid; +-monoid
+    ( +-rawMagma; +-magma; +-semigroup
+    ; +-rawMonoid; +-monoid
     ; *-rawMagma; *-magma; *-semigroup
     )
 
   +-commutativeMonoid : CommutativeMonoid _ _
-  +-commutativeMonoid =
-    record { isCommutativeMonoid = +-isCommutativeMonoid }
+  +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid }
+
+  open CommutativeMonoid +-commutativeMonoid public
+    using () renaming (commutativeSemigroup to +-commutativeSemigroup)
 
 
 record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -426,7 +429,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open SemiringWithoutOne semiringWithoutOne public
     using
-    ( +-rawMagma; +-magma; +-semigroup
+    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; nearSemiring
@@ -471,13 +474,13 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
     record { isCommutativeMonoid = +-isCommutativeMonoid }
 
   open CommutativeMonoid +-commutativeMonoid public
-    using ()
-    renaming
-    ( rawMagma  to +-rawMagma
-    ; magma     to +-magma
-    ; semigroup to +-semigroup
-    ; rawMonoid to +-rawMonoid
-    ; monoid    to +-monoid
+    using () renaming
+    ( rawMagma             to +-rawMagma
+    ; magma                to +-magma
+    ; semigroup            to +-semigroup
+    ; commutativeSemigroup to +-commutativeSemigroup
+    ; rawMonoid            to +-rawMonoid
+    ; monoid               to +-monoid
     )
 
   *-monoid : Monoid _ _
@@ -526,7 +529,7 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
   open SemiringWithoutAnnihilatingZero
          semiringWithoutAnnihilatingZero public
     using
-    ( +-rawMagma;  +-magma;  +-semigroup
+    ( +-rawMagma;  +-magma;  +-semigroup; +-commutativeSemigroup
     ; *-rawMagma;  *-magma;  *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -560,7 +563,7 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup
+    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -645,7 +648,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup
+    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid ; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -694,8 +697,8 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
   open Ring ring public using (rawRing; +-group; +-abelianGroup)
   open CommutativeSemiring commutativeSemiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup
-    ; *-rawMagma; *-magma; *-semigroup
+    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-semigroup; *-commutativeSemigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid; *-commutativeMonoid
     ; nearSemiring; semiringWithoutOne