Move raw bundles from Data.X.Properties to Data.X.Base (#1810)

Author: 5xy1

CHANGELOG.md

@@ -671,6 +671,32 @@ Major improvements
 * Beneficieries of this change include `Data.Rational.Unnormalised.Base` whose
   dependencies are now significantly smaller.
 
+### Moved raw bundles from Data.X.Properties to Data.X.Base
+
+* As mentioned by MatthewDaggitt in Issue #1755, Raw bundles defined in Data.X.Properties
+  should be defined in Data.X.Base as they don't require any properties.
+  * Moved raw bundles From `Data.Nat.Properties` to `Data.Nat.Base`
+  * Moved raw bundles From `Data.Nat.Binary.Properties` to `Data.Nat.Binary.Base`
+  * Moved raw bundles From `Data.Rational.Properties` to `Data.Rational.Base`
+  * Moved raw bundles From `Data.Rational.Unnormalised.Properties` to `Data.Rational.Unnormalised.Base`
+
+### Moved the definition of RawX from `Algebra.X.Bundles` to `Algebra.X.Bundles.Raw`
+
+* A new module `Algebra.Bundles.Raw` containing the definitions of the raw bundles
+  can be imported at much lower cost from `Data.X.Base`.
+  The following definitions have been moved:
+  * `RawMagma`
+  * `RawMonoid`
+  * `RawGroup`
+  * `RawNearSemiring`
+  * `RawSemiring`
+  * `RawRingWithoutOne`
+  * `RawRing`
+  * `RawQuasigroup`
+  * `RawLoop`
+* A new module `Algebra.Lattice.Bundles.Raw` is also introduced.
+  * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module.
+
 Deprecated modules
 ------------------
 

README/Design/Hierarchies.agda

@@ -42,6 +42,7 @@ private
 -- all four of which are publicly re-exported by `X` itself.
 --
 -- Additionally a hierarchy `X` may contain additional files
+--   ∙ X.Bundles.Raw
 --   ∙ X.Consequences
 --   ∙ X.Constructs
 --   ∙ X.Properties
@@ -252,6 +253,33 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 -- Other hierarchy modules
 ------------------------------------------------------------------------
 
+------------------------------------------------------------------------
+-- X.Bundles.Raw
+
+-- Sometimes it is useful to have the bundles without any accompanying
+-- laws. These correspond more or less to what the definitions would
+-- be in non-dependently typed languages like Haskell.
+
+-- Each bundle thereofre has a corresponding raw bundle that only
+-- include the laws but not the operations.
+
+record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+
+record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    ε       : Carrier
+
 ------------------------------------------------------------------------
 -- X.Consequences
 

src/Algebra/Bundles.agda

@@ -11,6 +11,7 @@
 
 module Algebra.Bundles where
 
+import Algebra.Bundles.Raw as Raw
 open import Algebra.Core
 open import Algebra.Structures
 open import Relation.Binary
@@ -19,21 +20,17 @@ import Relation.Nullary as N
 open import Level
 
 ------------------------------------------------------------------------
--- Bundles with 1 binary operation
-------------------------------------------------------------------------
-
-record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _∙_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _∙_     : Op₂ Carrier
+-- Re-export definitions of 'raw' bundles
 
-  infix 4 _≉_
-  _≉_ : Rel Carrier _
-  x ≉ y = N.¬ (x ≈ y)
+open Raw public
+  using (RawMagma; RawMonoid; RawGroup
+        ; RawNearSemiring; RawSemiring
+        ; RawRingWithoutOne; RawRing
+        ; RawQuasigroup; RawLoop)
 
+------------------------------------------------------------------------
+-- Bundles with 1 binary operation
+------------------------------------------------------------------------
 
 record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -232,27 +229,6 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Bundles with 1 binary operation & 1 element
 ------------------------------------------------------------------------
 
--- A raw monoid is a monoid without any laws.
-
-record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _∙_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _∙_     : Op₂ Carrier
-    ε       : Carrier
-
-  rawMagma : RawMagma c ℓ
-  rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    }
-
-  open RawMagma rawMagma public
-    using (_≉_)
-
-
 record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infix  4 _≈_
@@ -359,28 +335,6 @@ module BoundedLattice {c ℓ} (idemCommMonoid : IdempotentCommutativeMonoid c 
 -- Bundles with 1 binary operation, 1 unary operation & 1 element
 ------------------------------------------------------------------------
 
-record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
-  infix  8 _⁻¹
-  infixl 7 _∙_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _∙_     : Op₂ Carrier
-    ε       : Carrier
-    _⁻¹     : Op₁ Carrier
-
-  rawMonoid : RawMonoid c ℓ
-  rawMonoid = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    ; ε   = ε
-    }
-
-  open RawMonoid rawMonoid public
-    using (_≉_; rawMagma)
-
-
 record InvertibleMagma c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⁻¹
   infixl 7 _∙_
@@ -487,34 +441,6 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Bundles with 2 binary operations & 1 element
 ------------------------------------------------------------------------
 
-record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _*_
-  infixl 6 _+_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _+_     : Op₂ Carrier
-    _*_     : Op₂ Carrier
-    0#      : Carrier
-
-  +-rawMonoid : RawMonoid c ℓ
-  +-rawMonoid = record
-    { _≈_ = _≈_
-    ; _∙_ = _+_
-    ;  ε  = 0#
-    }
-
-  open RawMonoid +-rawMonoid public
-    using (_≉_) renaming (rawMagma to +-rawMagma)
-
-  *-rawMagma : RawMagma c ℓ
-  *-rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _*_
-    }
-
-
 record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
   infixl 6 _+_
@@ -626,37 +552,6 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Bundles with 2 binary operations & 2 elements
 ------------------------------------------------------------------------
 
-record RawSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _*_
-  infixl 6 _+_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _+_     : Op₂ Carrier
-    _*_     : Op₂ Carrier
-    0#      : Carrier
-    1#      : Carrier
-
-  rawNearSemiring : RawNearSemiring c ℓ
-  rawNearSemiring = record
-    { _≈_ = _≈_
-    ; _+_ = _+_
-    ; _*_ = _*_
-    ; 0#  = 0#
-    }
-
-  open RawNearSemiring rawNearSemiring public
-    using (_≉_; +-rawMonoid; +-rawMagma; *-rawMagma)
-
-  *-rawMonoid : RawMonoid c ℓ
-  *-rawMonoid = record
-    { _≈_ = _≈_
-    ; _∙_ = _*_
-    ; ε   = 1#
-    }
-
-
 record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
   infixl 6 _+_
@@ -939,37 +834,6 @@ record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Bundles with 2 binary operations, 1 unary operation & 1 element
 ------------------------------------------------------------------------
 
-record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
-  infix  8 -_
-  infixl 7 _*_
-  infixl 6 _+_
-  infix  4 _≈_
-  field
-    Carrier           : Set c
-    _≈_               : Rel Carrier ℓ
-    _+_               : Op₂ Carrier
-    _*_               : Op₂ Carrier
-    -_                : Op₁ Carrier
-    0#                : Carrier
-
-  +-rawGroup : RawGroup c ℓ
-  +-rawGroup = record
-    { _≈_ = _≈_
-    ; _∙_ = _+_
-    ; ε   = 0#
-    ; _⁻¹ = -_
-    }
-
-  open RawGroup +-rawGroup public
-    using (_≉_) renaming (rawMagma to +-rawMagma; rawMonoid to +-rawMonoid)
-
-  *-rawMagma : RawMagma c ℓ
-  *-rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _*_
-    }
-
-
 record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 -_
   infixl 7 _*_
@@ -1053,46 +917,6 @@ record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where
     ;*-rawMagma; *-magma; *-semigroup; *-monoid
     )
 
--- A raw ring is a ring without any laws.
-
-record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
-  infix  8 -_
-  infixl 7 _*_
-  infixl 6 _+_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _+_     : Op₂ Carrier
-    _*_     : Op₂ Carrier
-    -_      : Op₁ Carrier
-    0#      : Carrier
-    1#      : Carrier
-
-  rawSemiring : RawSemiring c ℓ
-  rawSemiring = record
-    { _≈_ = _≈_
-    ; _+_ = _+_
-    ; _*_ = _*_
-    ; 0#  = 0#
-    ; 1#  = 1#
-    }
-
-  open RawSemiring rawSemiring public
-    using
-    ( _≉_
-    ; +-rawMagma; +-rawMonoid
-    ; *-rawMagma; *-rawMonoid
-    )
-
-  +-rawGroup : RawGroup c ℓ
-  +-rawGroup = record
-    { _≈_ = _≈_
-    ; _∙_ = _+_
-    ; ε   = 0#
-    ; _⁻¹ = -_
-    }
-
 
 record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 -_
@@ -1184,39 +1008,6 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Bundles with 3 binary operations
 ------------------------------------------------------------------------
 
-record RawQuasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _∙_
-  infixl 7 _\\_
-  infixl 7 _//_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _∙_     : Op₂ Carrier
-    _\\_    : Op₂ Carrier
-    _//_    : Op₂ Carrier
-
-  ∙-rawMagma : RawMagma c ℓ
-  ∙-rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    }
-
-  \\-rawMagma : RawMagma c ℓ
-  \\-rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _\\_
-    }
-
-  //-rawMagma : RawMagma c ℓ
-  //-rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _//_
-    }
-
-  open RawMagma \\-rawMagma public
-    using (_≉_)
-
 record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infixl 7 _\\_
@@ -1249,30 +1040,6 @@ record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   open RawQuasigroup rawQuasigroup public
     using (//-rawMagma; \\-rawMagma; ∙-rawMagma)
 
-record RawLoop  c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _∙_
-  infixl 7 _\\_
-  infixl 7 _//_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _∙_     : Op₂ Carrier
-    _\\_    : Op₂ Carrier
-    _//_    : Op₂ Carrier
-    ε       : Carrier
-
-  rawQuasigroup : RawQuasigroup c ℓ
-  rawQuasigroup = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    ; _\\_ = _\\_
-    ; _//_ = _//_
-    }
-
-  open RawQuasigroup rawQuasigroup public
-    using (_≉_ ; ∙-rawMagma; \\-rawMagma; //-rawMagma)
-
 record Loop  c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infixl 7 _\\_