summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Ordered/StrictTotal
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal')
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda182
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Structures.agda160
2 files changed, 306 insertions, 36 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
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
index 9dc0043..6f6b38d 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
@@ -18,11 +18,11 @@ module Helium.Algebra.Ordered.StrictTotal.Structures
import Algebra.Consequences.Setoid as Consequences
open import Algebra.Core
open import Algebra.Definitions _≈_
-import Algebra.Structures _≈_ as Unordered
+import Algebra.Structures _≈_ as NoOrder
open import Data.Product using (_,_; proj₁; proj₂)
open import Helium.Algebra.Core
open import Helium.Algebra.Definitions _≈_
-open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup)
+import Helium.Algebra.Structures _≈_ as NoOrder′
open import Helium.Algebra.Ordered.Definitions _<_
open import Level using (_⊔_)
@@ -52,26 +52,55 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
∙-invariantʳ : RightInvariant ∙
∙-invariantʳ = proj₂ ∙-invariant
+ module Unordered where
+ isMagma : NoOrder.IsMagma ∙
+ isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMagma : IsMagma ∙
assoc : Associative ∙
open IsMagma isMagma public
+ hiding (module Unordered)
+
+ module Unordered where
+ isSemigroup : NoOrder.IsSemigroup ∙
+ isSemigroup = record
+ { isMagma = IsMagma.Unordered.isMagma isMagma
+ ; assoc = assoc
+ }
+
+ open NoOrder.IsSemigroup isSemigroup public
+ using (isMagma)
-record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsMonoid (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
- isSemigroup : IsSemigroup ∙
- identity : Identity ε ∙
+ isSemigroup : IsSemigroup _∙_
+ identity : Identity ε _∙_
open IsSemigroup isSemigroup public
+ hiding (module Unordered)
- identityˡ : LeftIdentity ε ∙
+ identityˡ : LeftIdentity ε _∙_
identityˡ = proj₁ identity
- identityʳ : RightIdentity ε ∙
+ identityʳ : RightIdentity ε _∙_
identityʳ = proj₂ identity
+ identity² : (ε ∙ ε) ≈ ε
+ identity² = identityˡ ε
+
+ module Unordered where
+ isMonoid : NoOrder.IsMonoid _∙_ ε
+ isMonoid = record
+ { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup
+ ; identity = identity
+ }
+
+ open NoOrder.IsMonoid isMonoid public
+ using (isMagma; isSemigroup)
+
record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMonoid : IsMonoid _∙_ ε
@@ -79,6 +108,7 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
⁻¹-cong : Congruent₁ _⁻¹
open IsMonoid isMonoid public
+ hiding (module Unordered)
infixl 6 _-_
_-_ : Op₂ A
@@ -98,6 +128,17 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ
+ module Unordered where
+ isGroup : NoOrder.IsGroup _∙_ ε _⁻¹
+ isGroup = record
+ { isMonoid = IsMonoid.Unordered.isMonoid isMonoid
+ ; inverse = inverse
+ ; ⁻¹-cong = ⁻¹-cong
+ }
+
+ open NoOrder.IsGroup isGroup public
+ using (isMagma; isSemigroup; isMonoid)
+
record IsAbelianGroup (∙ : Op₂ A)
(ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
@@ -105,14 +146,25 @@ record IsAbelianGroup (∙ : Op₂ A)
comm : Commutative ∙
open IsGroup isGroup public
+ hiding (module Unordered)
+
+ module Unordered where
+ isAbelianGroup : NoOrder.IsAbelianGroup ∙ ε ⁻¹
+ isAbelianGroup = record
+ { isGroup = IsGroup.Unordered.isGroup isGroup
+ ; comm = comm
+ }
-record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ open NoOrder.IsAbelianGroup isAbelianGroup public
+ using (isMagma; isSemigroup; isMonoid; isGroup)
+
+record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
- +-isAbelianGroup : IsAbelianGroup + 0# -_
- *-isMonoid : Unordered.IsMonoid * 1#
- distrib : * DistributesOver +
- zero : Zero 0# *
- preservesPositive : PreservesPositive 0# *
+ +-isAbelianGroup : IsAbelianGroup + 0# -_
+ *-isMonoid : NoOrder.IsMonoid _*_ 1#
+ distrib : _*_ DistributesOver +
+ zero : Zero 0# _*_
+ 0<a+0<b⇒0<ab : PreservesPositive 0# _*_
open IsAbelianGroup +-isAbelianGroup public
renaming
@@ -120,9 +172,13 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
; ∙-cong to +-cong
; ∙-congˡ to +-congˡ
; ∙-congʳ to +-congʳ
+ ; ∙-invariant to +-invariant
+ ; ∙-invariantˡ to +-invariantˡ
+ ; ∙-invariantʳ to +-invariantʳ
; identity to +-identity
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
+ ; identity² to +-identity²
; inverse to -‿inverse
; inverseˡ to -‿inverseˡ
; inverseʳ to -‿inverseʳ
@@ -133,8 +189,9 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
; isMonoid to +-isMonoid
; isGroup to +-isGroup
)
+ hiding (module Unordered)
- open Unordered.IsMonoid *-isMonoid public
+ open NoOrder.IsMonoid *-isMonoid public
using ()
renaming
( assoc to *-assoc
@@ -148,18 +205,33 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
; isSemigroup to *-isSemigroup
)
- distribˡ : * DistributesOverˡ +
+ *-identity² : (1# * 1#) ≈ 1#
+ *-identity² = *-identityˡ 1#
+
+ distribˡ : _*_ DistributesOverˡ +
distribˡ = proj₁ distrib
- distribʳ : * DistributesOverʳ +
+ distribʳ : _*_ DistributesOverʳ +
distribʳ = proj₂ distrib
- zeroˡ : LeftZero 0# *
+ zeroˡ : LeftZero 0# _*_
zeroˡ = proj₁ zero
- zeroʳ : RightZero 0# *
+ zeroʳ : RightZero 0# _*_
zeroʳ = proj₂ zero
+ module Unordered where
+ isRing : NoOrder.IsRing + _*_ -_ 0# 1#
+ isRing = record
+ { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+ ; *-isMonoid = *-isMonoid
+ ; distrib = distrib
+ ; zero = zero
+ }
+
+ open NoOrder.IsRing isRing
+ using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup)
+
record IsCommutativeRing
(+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
@@ -167,16 +239,27 @@ record IsCommutativeRing
*-comm : Commutative *
open IsRing isRing public
+ hiding (module Unordered)
+
+ module Unordered where
+ isCommutativeRing : NoOrder.IsCommutativeRing + * (-) 0# 1#
+ isCommutativeRing = record
+ { isRing = IsRing.Unordered.isRing isRing
+ ; *-comm = *-comm
+ }
+
+ open NoOrder.IsCommutativeRing isCommutativeRing public
+ using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
record IsDivisionRing
(+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
(_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
- +-isAbelianGroup : IsAbelianGroup + 0# -_
- *-isAlmostGroup : IsAlmostGroup _*_ 0# 1# _⁻¹
- distrib : _*_ DistributesOver +
- zero : Zero 0# _*_
- preservesPositive : PreservesPositive 0# _*_
+ +-isAbelianGroup : IsAbelianGroup + 0# -_
+ *-isAlmostGroup : NoOrder′.IsAlmostGroup _*_ 0# 1# _⁻¹
+ distrib : _*_ DistributesOver +
+ zero : Zero 0# _*_
+ 0<a+0<b⇒0<ab : PreservesPositive 0# _*_
infixl 7 _/_
_/_ : AlmostOp₂ _≈_ 0#
@@ -203,8 +286,9 @@ record IsDivisionRing
; isMonoid to +-isMonoid
; isGroup to +-isGroup
)
+ hiding (module Unordered)
- open IsAlmostGroup *-isAlmostGroup public
+ open NoOrder′.IsAlmostGroup *-isAlmostGroup public
using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
renaming
( assoc to *-assoc
@@ -228,12 +312,24 @@ record IsDivisionRing
; *-isMonoid = *-isMonoid
; distrib = distrib
; zero = zero
- ; preservesPositive = preservesPositive
+ ; 0<a+0<b⇒0<ab = 0<a+0<b⇒0<ab
}
open IsRing isRing public
using (distribˡ ; distribʳ ; zeroˡ ; zeroʳ)
+ module Unordered where
+ isDivisionRing : NoOrder′.IsDivisionRing + _*_ -_ 0# 1# _⁻¹
+ isDivisionRing = record
+ { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+ ; *-isAlmostGroup = *-isAlmostGroup
+ ; distrib = distrib
+ ; zero = zero
+ }
+
+ open NoOrder′.IsDivisionRing isDivisionRing
+ using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
+
record IsField
(+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
(⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -242,9 +338,23 @@ record IsField
*-comm : Commutative *
open IsDivisionRing isDivisionRing public
+ hiding (module Unordered)
isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
isCommutativeRing = record
{ isRing = isRing
; *-comm = *-comm
}
+
+ module Unordered where
+ isField : NoOrder′.IsField + * -_ 0# 1# ⁻¹
+ isField = record
+ { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing
+ ; *-comm = *-comm
+ }
+
+ open NoOrder′.IsField isField
+ using
+ ( +-isMagma; +-isSemigroup; +-isMonoid; +-isGroup
+ ; isRing; isDivisionRing
+ )
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 12:27:39 +0000