fixes issue #1688 (#2254)

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`:

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 -_