summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Helium/Algebra/Ordered/Definitions.agda29
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda437
-rw-r--r--src/Helium/Algebra/Ordered/StrictTotal/Structures.agda250
3 files changed, 716 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/Definitions.agda b/src/Helium/Algebra/Ordered/Definitions.agda
new file mode 100644
index 0000000..4ac1070
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/Definitions.agda
@@ -0,0 +1,29 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Ordering properties of functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Helium.Algebra.Ordered.Definitions
+ {a ℓ} {A : Set a} -- The underlying set
+ (_≤_ : Rel A ℓ) -- The underlying order
+ where
+
+open import Algebra.Core
+open import Data.Product using (_×_)
+
+LeftInvariant : Op₂ A → Set _
+LeftInvariant _∙_ = ∀ {x y} z → x ≤ y → (z ∙ x) ≤ (z ∙ y)
+
+RightInvariant : Op₂ A → Set _
+RightInvariant _∙_ = ∀ {x y} z → x ≤ y → (x ∙ z) ≤ (y ∙ z)
+
+Invariant : Op₂ A → Set _
+Invariant ∙ = LeftInvariant ∙ × RightInvariant ∙
+
+PreservesPositive : A → Op₂ A → Set _
+PreservesPositive 0# _∙_ = ∀ {x y} → 0# ≤ x → 0# ≤ y → 0# ≤ (x ∙ y)
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
new file mode 100644
index 0000000..6904bfb
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
@@ -0,0 +1,437 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of ordered algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+
+module Helium.Algebra.Ordered.StrictTotal.Bundles where
+
+import Algebra.Bundles as Unordered
+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)
+open import Helium.Algebra.Ordered.StrictTotal.Structures
+open import Level using (suc; _⊔_)
+open import Relation.Binary
+open import Relation.Nullary as N
+
+record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+
+ infix 4 _≉_ _≤_ _>_ _≥_
+ _≉_ : Rel Carrier _
+ x ≉ y = N.¬ x ≈ y
+
+ _≤_ : Rel Carrier _
+ x ≤ y = x < y ⊎ x ≈ y
+
+ _>_ : Rel Carrier _
+ _>_ = flip _<_
+
+ _≥_ : Rel Carrier _
+ _≥_ = flip _≤_
+
+record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ isMagma : IsMagma _≈_ _<_ _∙_
+
+ open IsMagma isMagma public
+
+ rawMagma : RawMagma _ _ _
+ rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
+
+ open RawMagma rawMagma public
+ using (_≉_; _≤_; _>_; _≥_)
+
+record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ isSemigroup : IsSemigroup _≈_ _<_ _∙_
+
+ open IsSemigroup isSemigroup public
+
+ magma : Magma c ℓ₁ ℓ₂
+ magma = record { isMagma = isMagma }
+
+ open Magma magma public
+ using (_≉_; _≤_; _>_; _≥_; rawMagma)
+
+record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+
+ rawMagma : RawMagma c ℓ₁ ℓ₂
+ rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
+
+ open RawMagma rawMagma public
+ using (_≉_; _≤_; _>_; _≥_)
+
+record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ isMonoid : IsMonoid _≈_ _<_ _∙_ ε
+
+ open IsMonoid isMonoid public
+
+ semigroup : Semigroup _ _ _
+ semigroup = record { isSemigroup = isSemigroup }
+
+ open Semigroup semigroup public
+ using (_≉_; _≤_; _>_; _≥_; rawMagma; magma)
+
+ rawMonoid : RawMonoid _ _ _
+ rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε}
+
+record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ _⁻¹ : Op₁ Carrier
+
+ rawMonoid : RawMonoid c ℓ₁ ℓ₂
+ rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε }
+
+ open RawMonoid rawMonoid public
+ using (_≉_; _≤_; _>_; _≥_; rawMagma)
+
+
+record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ _⁻¹ : Op₁ Carrier
+ isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹
+
+ open IsGroup isGroup public
+
+ rawGroup : RawGroup _ _ _
+ rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
+
+ monoid : Monoid _ _ _
+ monoid = record { isMonoid = isMonoid }
+
+ open Monoid monoid public
+ using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid)
+
+record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ _⁻¹ : Op₁ Carrier
+ isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹
+
+ open IsAbelianGroup isAbelianGroup public
+
+ group : Group _ _ _
+ group = record { isGroup = isGroup }
+
+ open Group group public
+ using
+ ( _≉_; _≤_; _>_; _≥_
+ ; magma; semigroup; monoid
+ ; rawMagma; rawMonoid; rawGroup
+ )
+
+record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+
+ +-rawGroup : RawGroup c ℓ₁ ℓ₂
+ +-rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _+_; ε = 0#; _⁻¹ = -_ }
+
+ open RawGroup +-rawGroup public
+ using ( _≉_; _≤_; _>_; _≥_ )
+ renaming
+ ( rawMagma to +-rawMagma
+ ; rawMonoid to +-rawMonoid
+ )
+
+ *-rawMonoid : Unordered.RawMonoid c ℓ₁
+ *-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# }
+
+ open Unordered.RawMonoid *-rawMonoid public
+ using ()
+ renaming ( rawMagma to *-rawMagma )
+
+record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isRing : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1#
+
+ open IsRing isRing public
+
+ rawRing : RawRing c ℓ₁ ℓ₂
+ rawRing = record
+ { _≈_ = _≈_
+ ; _<_ = _<_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ }
+
+ +-abelianGroup : AbelianGroup _ _ _
+ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
+
+ open AbelianGroup +-abelianGroup public
+ using ( _≉_; _≤_; _>_; _≥_ )
+ renaming
+ ( rawMagma to +-rawMagma
+ ; rawMonoid to +-rawMonoid
+ ; rawGroup to +-rawGroup
+ ; magma to +-magma
+ ; semigroup to +-semigroup
+ ; monoid to +-monoid
+ ; group to +-group
+ )
+
+ *-monoid : Unordered.Monoid _ _
+ *-monoid = record { isMonoid = *-isMonoid }
+
+ open Unordered.Monoid *-monoid public
+ using ()
+ renaming
+ ( rawMagma to *-rawMagma
+ ; rawMonoid to *-rawMonoid
+ ; magma to *-magma
+ ; semigroup to *-semigroup
+ )
+
+record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isCommutativeRing : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1#
+
+ open IsCommutativeRing isCommutativeRing public
+
+ ring : Ring _ _ _
+ ring = record { isRing = isRing }
+
+ open Ring ring public
+ using
+ ( _≉_; _≤_; _>_; _≥_
+ ; +-rawMagma; +-rawMonoid; +-rawGroup
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; *-rawMagma; *-rawMonoid
+ ; *-magma; *-semigroup; *-monoid
+ )
+
+record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 9 _⁻¹
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+
+ infixl 7 _/_
+ _/_ : AlmostOp₂ _≈_ 0#
+ x / y≉0 = x * y≉0 ⁻¹
+
+ rawRing : RawRing c ℓ₁ ℓ₂
+ rawRing = record
+ { _≈_ = _≈_
+ ; _<_ = _<_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ }
+
+ open RawRing rawRing public
+ using
+ ( _≉_; _≤_; _>_; _≥_
+ ; +-rawMagma; +-rawMonoid; +-rawGroup
+ ; *-rawMagma; *-rawMonoid
+ )
+
+ *-rawAlmostGroup : RawAlmostGroup c ℓ₁
+ *-rawAlmostGroup = record
+ { _≈_ = _≈_
+ ; _∙_ = _*_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; _⁻¹ = _⁻¹
+ }
+
+record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 9 _⁻¹
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+ isDivisionRing : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
+
+ open IsDivisionRing isDivisionRing public
+
+ rawField : RawField c ℓ₁ ℓ₂
+ rawField = record
+ { _≈_ = _≈_
+ ; _<_ = _<_
+ ; _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ ; _⁻¹ = _⁻¹
+ }
+
+ ring : Ring c ℓ₁ ℓ₂
+ ring = record { isRing = isRing }
+
+ open Ring ring public
+ using
+ ( _≉_; _≤_; _>_; _≥_
+ ; rawRing
+ ; +-rawMagma; +-rawMonoid; +-rawGroup
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; *-rawMagma; *-rawMonoid
+ ; *-magma; *-semigroup; *-monoid
+ )
+
+ *-almostGroup : AlmostGroup _ _
+ *-almostGroup = record { isAlmostGroup = *-isAlmostGroup }
+
+ open AlmostGroup *-almostGroup public
+ using ()
+ renaming (rawAlmostGroup to *-rawAlmostGroup)
+
+record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 9 _⁻¹
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ _⁻¹ : AlmostOp₁ _≈_ 0#
+ isField : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
+
+ open IsField isField public
+
+ divisionRing : DivisionRing c ℓ₁ ℓ₂
+ divisionRing = record { isDivisionRing = isDivisionRing }
+
+ open DivisionRing divisionRing
+ using
+ ( _≉_; _≤_; _>_; _≥_
+ ; +-rawMagma; +-rawMonoid; +-rawGroup
+ ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+ ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup
+ ; *-magma; *-semigroup; *-monoid; *-almostGroup
+ )
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
new file mode 100644
index 0000000..9dc0043
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
@@ -0,0 +1,250 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Some ordered algebraic structures (not packed up with sets,
+-- operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Helium.Algebra.Ordered.StrictTotal.Structures
+ {a ℓ₁ ℓ₂} {A : Set a} -- The underlying set
+ (_≈_ : Rel A ℓ₁) -- The underlying equality
+ (_<_ : Rel A ℓ₂) -- The underlying order
+ where
+
+import Algebra.Consequences.Setoid as Consequences
+open import Algebra.Core
+open import Algebra.Definitions _≈_
+import Algebra.Structures _≈_ as Unordered
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Helium.Algebra.Core
+open import Helium.Algebra.Definitions _≈_
+open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup)
+open import Helium.Algebra.Ordered.Definitions _<_
+open import Level using (_⊔_)
+
+record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
+ ∙-cong : Congruent₂ ∙
+ ∙-invariant : Invariant ∙
+
+ open IsStrictTotalOrder isStrictTotalOrder public
+
+ strictTotalOrder : StrictTotalOrder _ _ _
+ strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }
+
+ open module strictTotalOrder = StrictTotalOrder strictTotalOrder public
+ using (strictPartialOrder)
+
+ ∙-congˡ : LeftCongruent ∙
+ ∙-congˡ y≈z = ∙-cong Eq.refl y≈z
+
+ ∙-congʳ : RightCongruent ∙
+ ∙-congʳ y≈z = ∙-cong y≈z Eq.refl
+
+ ∙-invariantˡ : LeftInvariant ∙
+ ∙-invariantˡ = proj₁ ∙-invariant
+
+ ∙-invariantʳ : RightInvariant ∙
+ ∙-invariantʳ = proj₂ ∙-invariant
+
+record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isMagma : IsMagma ∙
+ assoc : Associative ∙
+
+ open IsMagma isMagma public
+
+record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isSemigroup : IsSemigroup ∙
+ identity : Identity ε ∙
+
+ open IsSemigroup isSemigroup public
+
+ identityˡ : LeftIdentity ε ∙
+ identityˡ = proj₁ identity
+
+ identityʳ : RightIdentity ε ∙
+ identityʳ = proj₂ identity
+
+record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isMonoid : IsMonoid _∙_ ε
+ inverse : Inverse ε _⁻¹ _∙_
+ ⁻¹-cong : Congruent₁ _⁻¹
+
+ open IsMonoid isMonoid public
+
+ infixl 6 _-_
+ _-_ : Op₂ A
+ x - y = x ∙ (y ⁻¹)
+
+ inverseˡ : LeftInverse ε _⁻¹ _∙_
+ inverseˡ = proj₁ inverse
+
+ inverseʳ : RightInverse ε _⁻¹ _∙_
+ inverseʳ = proj₂ inverse
+
+ uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
+ uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique
+ strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseʳ
+
+ uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
+ uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
+ strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ
+
+record IsAbelianGroup (∙ : Op₂ A)
+ (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isGroup : IsGroup ∙ ε ⁻¹
+ comm : Commutative ∙
+
+ open IsGroup isGroup public
+
+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# *
+
+ open IsAbelianGroup +-isAbelianGroup public
+ renaming
+ ( assoc to +-assoc
+ ; ∙-cong to +-cong
+ ; ∙-congˡ to +-congˡ
+ ; ∙-congʳ to +-congʳ
+ ; identity to +-identity
+ ; identityˡ to +-identityˡ
+ ; identityʳ to +-identityʳ
+ ; inverse to -‿inverse
+ ; inverseˡ to -‿inverseˡ
+ ; inverseʳ to -‿inverseʳ
+ ; ⁻¹-cong to -‿cong
+ ; comm to +-comm
+ ; isMagma to +-isMagma
+ ; isSemigroup to +-isSemigroup
+ ; isMonoid to +-isMonoid
+ ; isGroup to +-isGroup
+ )
+
+ open Unordered.IsMonoid *-isMonoid public
+ using ()
+ renaming
+ ( assoc to *-assoc
+ ; ∙-cong to *-cong
+ ; ∙-congˡ to *-congˡ
+ ; ∙-congʳ to *-congʳ
+ ; identity to *-identity
+ ; identityˡ to *-identityˡ
+ ; identityʳ to *-identityʳ
+ ; isMagma to *-isMagma
+ ; isSemigroup to *-isSemigroup
+ )
+
+ distribˡ : * DistributesOverˡ +
+ distribˡ = proj₁ distrib
+
+ distribʳ : * DistributesOverʳ +
+ distribʳ = proj₂ distrib
+
+ zeroˡ : LeftZero 0# *
+ zeroˡ = proj₁ zero
+
+ zeroʳ : RightZero 0# *
+ zeroʳ = proj₂ zero
+
+record IsCommutativeRing
+ (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isRing : IsRing + * - 0# 1#
+ *-comm : Commutative *
+
+ open IsRing isRing public
+
+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# _*_
+
+ infixl 7 _/_
+ _/_ : AlmostOp₂ _≈_ 0#
+ x / y≉0 = x * (y≉0 ⁻¹)
+
+ open IsAbelianGroup +-isAbelianGroup public
+ renaming
+ ( assoc to +-assoc
+ ; ∙-cong to +-cong
+ ; ∙-congˡ to +-congˡ
+ ; ∙-congʳ to +-congʳ
+ ; identity to +-identity
+ ; identityˡ to +-identityˡ
+ ; identityʳ to +-identityʳ
+ ; inverse to -‿inverse
+ ; inverseˡ to -‿inverseˡ
+ ; inverseʳ to -‿inverseʳ
+ ; ⁻¹-cong to -‿cong
+ ; uniqueˡ-⁻¹ to uniqueˡ‿-
+ ; uniqueʳ-⁻¹ to uniqueʳ‿-
+ ; comm to +-comm
+ ; isMagma to +-isMagma
+ ; isSemigroup to +-isSemigroup
+ ; isMonoid to +-isMonoid
+ ; isGroup to +-isGroup
+ )
+
+ open IsAlmostGroup *-isAlmostGroup public
+ using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
+ renaming
+ ( assoc to *-assoc
+ ; ∙-cong to *-cong
+ ; ∙-congˡ to *-congˡ
+ ; ∙-congʳ to *-congʳ
+ ; identity to *-identity
+ ; identityˡ to *-identityˡ
+ ; identityʳ to *-identityʳ
+ ; inverse to ⁻¹-inverse
+ ; inverseˡ to ⁻¹-inverseˡ
+ ; inverseʳ to ⁻¹-inverseʳ
+ ; isMagma to *-isMagma
+ ; isSemigroup to *-isSemigroup
+ ; isMonoid to *-isMonoid
+ )
+
+ isRing : IsRing + _*_ -_ 0# 1#
+ isRing = record
+ { +-isAbelianGroup = +-isAbelianGroup
+ ; *-isMonoid = *-isMonoid
+ ; distrib = distrib
+ ; zero = zero
+ ; preservesPositive = preservesPositive
+ }
+
+ open IsRing isRing public
+ using (distribˡ ; distribʳ ; zeroˡ ; zeroʳ)
+
+record IsField
+ (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
+ (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isDivisionRing : IsDivisionRing + * -_ 0# 1# ⁻¹
+ *-comm : Commutative *
+
+ open IsDivisionRing isDivisionRing public
+
+ isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
+ isCommutativeRing = record
+ { isRing = isRing
+ ; *-comm = *-comm
+ }
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 05:55:56 +0000