summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda')
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda182
1 files changed, 171 insertions, 11 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
index 6904bfb..a9430e9 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
@@ -10,13 +10,12 @@
module Helium.Algebra.Ordered.StrictTotal.Bundles where
-import Algebra.Bundles as Unordered
+import Algebra.Bundles as NoOrder
open import Algebra.Core
open import Data.Sum using (_⊎_)
open import Function using (flip)
open import Helium.Algebra.Core
-open import Helium.Algebra.Bundles using
- (RawAlmostGroup; AlmostGroup; AlmostAbelianGroup)
+import Helium.Algebra.Bundles as NoOrder′
open import Helium.Algebra.Ordered.StrictTotal.Structures
open import Level using (suc; _⊔_)
open import Relation.Binary
@@ -44,6 +43,10 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
_≥_ : Rel Carrier _
_≥_ = flip _≤_
+ module Unordered where
+ rawMagma : NoOrder.RawMagma c ℓ₁
+ rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ }
+
record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -55,6 +58,7 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isMagma : IsMagma _≈_ _<_ _∙_
open IsMagma isMagma public
+ hiding (module Unordered)
rawMagma : RawMagma _ _ _
rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
@@ -62,6 +66,15 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open RawMagma rawMagma public
using (_≉_; _≤_; _>_; _≥_)
+ module Unordered where
+ magma : NoOrder.Magma c ℓ₁
+ magma = record { isMagma = IsMagma.Unordered.isMagma isMagma }
+
+ open NoOrder.Magma magma public
+ using (rawMagma)
+
+ open IsMagma.Unordered isMagma public
+
record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -73,6 +86,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isSemigroup : IsSemigroup _≈_ _<_ _∙_
open IsSemigroup isSemigroup public
+ hiding (module Unordered)
magma : Magma c ℓ₁ ℓ₂
magma = record { isMagma = isMagma }
@@ -80,6 +94,16 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open Magma magma public
using (_≉_; _≤_; _>_; _≥_; rawMagma)
+ module Unordered where
+ semigroup : NoOrder.Semigroup c ℓ₁
+ semigroup =
+ record { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup }
+
+ open NoOrder.Semigroup semigroup public
+ using (rawMagma; magma)
+
+ open IsSemigroup.Unordered isSemigroup public
+
record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -96,6 +120,13 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open RawMagma rawMagma public
using (_≉_; _≤_; _>_; _≥_)
+ module Unordered where
+ rawMonoid : NoOrder.RawMonoid c ℓ₁
+ rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε }
+
+ open NoOrder.RawMonoid rawMonoid public
+ using (rawMagma)
+
record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infixl 7 _∙_
infix 4 _≈_ _<_
@@ -108,6 +139,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isMonoid : IsMonoid _≈_ _<_ _∙_ ε
open IsMonoid isMonoid public
+ hiding (module Unordered)
semigroup : Semigroup _ _ _
semigroup = record { isSemigroup = isSemigroup }
@@ -118,6 +150,15 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
rawMonoid : RawMonoid _ _ _
rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε}
+ module Unordered where
+ monoid : NoOrder.Monoid c ℓ₁
+ monoid = record { isMonoid = IsMonoid.Unordered.isMonoid isMonoid }
+
+ open NoOrder.Monoid monoid public
+ using (rawMagma; rawMonoid; magma; semigroup)
+
+ open IsMonoid.Unordered isMonoid public
+
record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 _⁻¹
infixl 7 _∙_
@@ -136,6 +177,12 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open RawMonoid rawMonoid public
using (_≉_; _≤_; _>_; _≥_; rawMagma)
+ module Unordered where
+ rawGroup : NoOrder.RawGroup c ℓ₁
+ rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹ }
+
+ open NoOrder.RawGroup rawGroup public
+ using (rawMagma; rawMonoid)
record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 _⁻¹
@@ -151,6 +198,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹
open IsGroup isGroup public
+ hiding (module Unordered)
rawGroup : RawGroup _ _ _
rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
@@ -161,6 +209,15 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
open Monoid monoid public
using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid)
+ module Unordered where
+ group : NoOrder.Group c ℓ₁
+ group = record { isGroup = IsGroup.Unordered.isGroup isGroup }
+
+ open NoOrder.Group group public
+ using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid)
+
+ open IsGroup.Unordered isGroup public
+
record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 _⁻¹
infixl 7 _∙_
@@ -175,6 +232,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹
open IsAbelianGroup isAbelianGroup public
+ hiding (module Unordered)
group : Group _ _ _
group = record { isGroup = isGroup }
@@ -186,6 +244,16 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; rawMagma; rawMonoid; rawGroup
)
+ module Unordered where
+ abelianGroup : NoOrder.AbelianGroup c ℓ₁
+ abelianGroup =
+ record { isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup isAbelianGroup }
+
+ open NoOrder.AbelianGroup abelianGroup public
+ using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; group)
+
+ open IsAbelianGroup.Unordered isAbelianGroup public
+
record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
@@ -211,13 +279,21 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; rawMonoid to +-rawMonoid
)
- *-rawMonoid : Unordered.RawMonoid c ℓ₁
+ *-rawMonoid : NoOrder.RawMonoid c ℓ₁
*-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# }
- open Unordered.RawMonoid *-rawMonoid public
+ open NoOrder.RawMonoid *-rawMonoid public
using ()
renaming ( rawMagma to *-rawMagma )
+ module Unordered where
+ rawRing : NoOrder.RawRing c ℓ₁
+ rawRing =
+ record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# }
+
+ open NoOrder.RawRing rawRing public
+ using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring)
+
record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
@@ -235,6 +311,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isRing : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1#
open IsRing isRing public
+ hiding (module Unordered)
rawRing : RawRing c ℓ₁ ℓ₂
rawRing = record
@@ -262,10 +339,10 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; group to +-group
)
- *-monoid : Unordered.Monoid _ _
+ *-monoid : NoOrder.Monoid _ _
*-monoid = record { isMonoid = *-isMonoid }
- open Unordered.Monoid *-monoid public
+ open NoOrder.Monoid *-monoid public
using ()
renaming
( rawMagma to *-rawMagma
@@ -274,6 +351,19 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; semigroup to *-semigroup
)
+ module Unordered where
+ ring : NoOrder.Ring c ℓ₁
+ ring = record { isRing = IsRing.Unordered.isRing isRing }
+
+ open NoOrder.Ring ring public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawRing; semiring
+ )
+
+ open IsRing.Unordered isRing public
+
record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
@@ -291,6 +381,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
isCommutativeRing : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1#
open IsCommutativeRing isCommutativeRing public
+ hiding (module Unordered)
ring : Ring _ _ _
ring = record { isRing = isRing }
@@ -298,12 +389,30 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
open Ring ring public
using
( _≉_; _≤_; _>_; _≥_
+ ; rawRing
; +-rawMagma; +-rawMonoid; +-rawGroup
; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
; *-rawMagma; *-rawMonoid
; *-magma; *-semigroup; *-monoid
)
+ module Unordered where
+ commutativeRing : NoOrder.CommutativeRing c ℓ₁
+ commutativeRing =
+ record { isCommutativeRing = IsCommutativeRing.Unordered.isCommutativeRing isCommutativeRing }
+
+ open NoOrder.CommutativeRing commutativeRing public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawRing; semiring; ring
+ )
+
+ open NoOrder.Semiring semiring public
+ using (rawSemiring)
+
+ open IsCommutativeRing.Unordered isCommutativeRing public
+
record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 9 _⁻¹
infix 8 -_
@@ -343,7 +452,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; *-rawMagma; *-rawMonoid
)
- *-rawAlmostGroup : RawAlmostGroup c ℓ₁
+ *-rawAlmostGroup : NoOrder′.RawAlmostGroup c ℓ₁
*-rawAlmostGroup = record
{ _≈_ = _≈_
; _∙_ = _*_
@@ -352,6 +461,21 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; _⁻¹ = _⁻¹
}
+ module Unordered where
+ rawField : NoOrder′.RawField c ℓ₁
+ rawField = record
+ { _≈_ = _≈_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; _⁻¹ = _⁻¹
+ }
+
+ open NoOrder′.RawField rawField public
+ using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring; rawRing)
+
record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 9 _⁻¹
infix 8 -_
@@ -371,6 +495,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isDivisionRing : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
open IsDivisionRing isDivisionRing public
+ hiding (module Unordered)
rawField : RawField c ℓ₁ ℓ₂
rawField = record
@@ -397,13 +522,28 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
; *-magma; *-semigroup; *-monoid
)
- *-almostGroup : AlmostGroup _ _
+ *-almostGroup : NoOrder′.AlmostGroup _ _
*-almostGroup = record { isAlmostGroup = *-isAlmostGroup }
- open AlmostGroup *-almostGroup public
+ open NoOrder′.AlmostGroup *-almostGroup public
using ()
renaming (rawAlmostGroup to *-rawAlmostGroup)
+ module Unordered where
+ divisionRing : NoOrder′.DivisionRing c ℓ₁
+ divisionRing =
+ record { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing }
+
+ open NoOrder′.DivisionRing divisionRing public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawSemiring; rawRing
+ ; semiring; ring
+ )
+
+ open IsDivisionRing.Unordered isDivisionRing public
+
record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 9 _⁻¹
infix 8 -_
@@ -423,15 +563,35 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
isField : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
open IsField isField public
+ hiding (module Unordered)
divisionRing : DivisionRing c ℓ₁ ℓ₂
divisionRing = record { isDivisionRing = isDivisionRing }
- open DivisionRing divisionRing
+ open DivisionRing divisionRing public
using
( _≉_; _≤_; _>_; _≥_
+ ; rawRing; rawField; ring
; +-rawMagma; +-rawMonoid; +-rawGroup
; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
; *-rawMagma; *-rawMonoid; *-rawAlmostGroup
; *-magma; *-semigroup; *-monoid; *-almostGroup
)
+
+ commutativeRing : CommutativeRing c ℓ₁ ℓ₂
+ commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+ module Unordered where
+ field′ : NoOrder′.Field c ℓ₁
+ field′ =
+ record { isField = IsField.Unordered.isField isField }
+
+ open NoOrder′.Field field′ public
+ using
+ ( +-rawMagma; +-rawMonoid
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; rawSemiring; rawRing
+ ; semiring; ring; divisionRing
+ )
+
+ open IsField.Unordered isField public
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 10:15:13 +0000