Skip to content

Fixed commutativeSemigroup re-exports in Algebra.Bundles #1174

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 3, 2020
Merged

Fixed commutativeSemigroup re-exports in Algebra.Bundles #1174

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,9 @@ Highlights
Bug-fixes
---------

* Fixed various algebraic bundles not correctly re-exporting
`commutativeSemigroup` proofs.

Non-backwards compatible changes
--------------------------------

Expand Down
55 changes: 29 additions & 26 deletions src/Algebra/Bundles.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _∙_
Expand All @@ -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 _∙_
Expand Down Expand Up @@ -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)


------------------------------------------------------------------------
Expand Down Expand Up @@ -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
Expand All @@ -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
)
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 _ _
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down