diff --git a/CHANGELOG.md b/CHANGELOG.md index e8f0a568f2..6c87780afe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -46,6 +46,12 @@ New modules Additions to existing modules ----------------------------- +* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: + ```agda + rawNearSemiring : RawNearSemiring _ _ + rawRingWithoutOne : RawRingWithoutOne _ _ + +-rawGroup : RawGroup _ _ + * In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. * In `Algebra.Module.Construct.DirectProduct`: diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 6b6384458a..1a31d16496 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -961,6 +961,9 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where ; semiringWithoutAnnihilatingZero ) + open NearSemiring nearSemiring public + using (rawNearSemiring) + open AbelianGroup +-abelianGroup public using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) @@ -974,6 +977,9 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where ; 1# = 1# } + open RawRing rawRing public + using (rawRingWithoutOne; +-rawGroup) + record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_