Move raw bundles from Data.X.Properties to Data.X.Base

CHANGELOG.md

@@ -75,6 +75,32 @@ Non-backwards compatible changes
   (highly specific) mode of use. Correspondingly, modules grouped under `*.Categorical.*`
   which exploited these structures for effectful programming have been renamed `*.Effectful`.
 
+#### 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.
+
 ### Improvements to pretty printing and regexes
 
 * In `Text.Pretty`, `Doc` is now a record rather than a type alias. This

src/Algebra/Bundles.agda

@@ -11,6 +11,7 @@
 
 module Algebra.Bundles where
 
+open import Algebra.Bundles.Raw public
 open import Algebra.Core
 open import Algebra.Structures
 open import Relation.Binary
@@ -22,19 +23,6 @@ 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
-
-  infix 4 _≉_
-  _≉_ : Rel Carrier _
-  x ≉ y = N.¬ (x ≈ y)
-
-
 record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infix  4 _≈_
@@ -232,27 +220,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 +326,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 +432,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 +543,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 +825,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 +908,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 +999,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 +1031,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 _\\_