consistency between sources

Author: jamesmckinna

src/Algebra/Construct/Terminal.agda

@@ -18,6 +18,9 @@ open import Algebra.Bundles
 open import Data.Unit.Polymorphic
 open import Relation.Binary.Core using (Rel)
 
+------------------------------------------------------------------------
+-- gather all the functionality in one place
+
 private module 𝕆ne where
 
   infix  4 _≈_

src/Algebra/Construct/Zero.agda

@@ -23,6 +23,10 @@ open import Algebra.Bundles.Raw
   using (RawMagma)
 open import Algebra.Bundles
   using (Magma; Semigroup; Band)
+
+------------------------------------------------------------------------
+-- re-export those algebras which are both initial and terminal
+
 open import Algebra.Construct.Terminal public
   hiding (rawMagma; magma; semigroup; band)
 

src/Algebra/Module/Construct/Zero.agda

@@ -23,6 +23,9 @@ private
   variable
     r s ℓr ℓs : Level
 
+------------------------------------------------------------------------
+-- gather all the functionality in one place
+
 private module ℤero where
 
   infix  4 _≈_
@@ -34,6 +37,15 @@ private module ℤero where
 
 open ℤero
 
+------------------------------------------------------------------------
+-- Raw bundles NOT YET IMPLEMENTED issue #1828
+{-
+rawModule : RawModule c ℓ
+rawModule = record { Carrier = Carrier ; _≈_ = _≈_ }
+-}
+------------------------------------------------------------------------
+-- Bundles
+
 leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ
 leftSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }