diff --git a/CHANGELOG.md b/CHANGELOG.md index 988355bd5a..6bfd659aa9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1832,13 +1832,6 @@ New modules Algebra.Morphism.Construct.Identity ``` -* Ordered algebraic structures (pomonoids, posemigroups, etc.) - ``` - Algebra.Ordered - Algebra.Ordered.Bundles - Algebra.Ordered.Structures - ``` - * 'Optimised' tail-recursive exponentiation properties: ``` Algebra.Properties.Semiring.Exp.TailRecursiveOptimised diff --git a/src/Algebra/Ordered.agda b/src/Algebra/Ordered.agda deleted file mode 100644 index 5eb99aec36..0000000000 --- a/src/Algebra/Ordered.agda +++ /dev/null @@ -1,14 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Definitions of ordered algebraic structures like promonoids and --- posemigroups (packed in records together with sets, orders, --- operations, etc.) ------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -module Algebra.Ordered where - -open import Algebra.Ordered.Structures public -open import Algebra.Ordered.Bundles public diff --git a/src/Algebra/Ordered/Bundles.agda b/src/Algebra/Ordered/Bundles.agda deleted file mode 100644 index 896f9d4d1f..0000000000 --- a/src/Algebra/Ordered/Bundles.agda +++ /dev/null @@ -1,438 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Definitions of ordered algebraic structures like promonoids and --- posemigroups (packed in records together with sets, orders, --- operations, etc.) ------------------------------------------------------------------------- - --- The contents of this module should be accessed via `Algebra.Order`. - -{-# OPTIONS --cubical-compatible --safe #-} - -module Algebra.Ordered.Bundles where - -open import Algebra.Core -open import Algebra.Bundles -open import Algebra.Ordered.Structures -open import Level using (suc; _⊔_) -open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Bundles using (Preorder; Poset) - ------------------------------------------------------------------------- --- Bundles of preordered structures - --- Preordered magmas (promagmas) - -record Promagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The preorder. - _∙_ : Op₂ Carrier -- Multiplication. - isPromagma : IsPromagma _≈_ _≤_ _∙_ - - open IsPromagma isPromagma public - - preorder : Preorder c ℓ₁ ℓ₂ - preorder = record { isPreorder = isPreorder } - - magma : Magma c ℓ₁ - magma = record { isMagma = isMagma } - --- Preordered semigroups (prosemigroups) - -record Prosemigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The preorder. - _∙_ : Op₂ Carrier -- Multiplication. - isProsemigroup : IsProsemigroup _≈_ _≤_ _∙_ - - open IsProsemigroup isProsemigroup public - - promagma : Promagma c ℓ₁ ℓ₂ - promagma = record { isPromagma = isPromagma } - - open Promagma promagma public using (preorder; magma) - - semigroup : Semigroup c ℓ₁ - semigroup = record { isSemigroup = isSemigroup } - --- Preordered monoids (promonoids) - -record Promonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The preorder. - _∙_ : Op₂ Carrier -- The monoid multiplication. - ε : Carrier -- The monoid unit. - isPromonoid : IsPromonoid _≈_ _≤_ _∙_ ε - - open IsPromonoid isPromonoid public - - prosemigroup : Prosemigroup c ℓ₁ ℓ₂ - prosemigroup = record { isProsemigroup = isProsemigroup } - - open Prosemigroup prosemigroup public - using (preorder; magma; promagma; semigroup) - - monoid : Monoid c ℓ₁ - monoid = record { isMonoid = isMonoid } - --- Preordered commutative monoids (commutative promonoids) - -record CommutativePromonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The preorder. - _∙_ : Op₂ Carrier -- The monoid multiplication. - ε : Carrier -- The monoid unit. - isCommutativePromonoid : IsCommutativePromonoid _≈_ _≤_ _∙_ ε - - open IsCommutativePromonoid isCommutativePromonoid public - - promonoid : Promonoid c ℓ₁ ℓ₂ - promonoid = record { isPromonoid = isPromonoid } - - open Promonoid promonoid public - using (preorder; magma; promagma; semigroup; prosemigroup; monoid) - - commutativeMonoid : CommutativeMonoid c ℓ₁ - commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } - - open CommutativeMonoid commutativeMonoid public using (commutativeSemigroup) - --- Preordered semirings (prosemirings) - -record Prosemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _*_ - infixl 6 _+_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - 0# : Carrier - 1# : Carrier - isProsemiring : IsProsemiring _≈_ _≤_ _+_ _*_ 0# 1# - - open IsProsemiring isProsemiring public - - +-commutativePromonoid : CommutativePromonoid c ℓ₁ ℓ₂ - +-commutativePromonoid = record - { isCommutativePromonoid = +-isCommutativePromonoid } - - open CommutativePromonoid +-commutativePromonoid public - using (preorder) - renaming - ( magma to +-magma - ; promagma to +-promagma - ; semigroup to +-semigroup - ; prosemigroup to +-prosemigroup - ; monoid to +-monoid - ; promonoid to +-promonoid - ; commutativeSemigroup to +-commutativeSemigroup - ; commutativeMonoid to +-commutativeMonoid - ) - - *-promonoid : Promonoid c ℓ₁ ℓ₂ - *-promonoid = record { isPromonoid = *-isPromonoid } - - open Promonoid *-promonoid public - using () - renaming - ( magma to *-magma - ; promagma to *-promagma - ; semigroup to *-semigroup - ; prosemigroup to *-prosemigroup - ; monoid to *-monoid - ) - - semiring : Semiring c ℓ₁ - semiring = record { isSemiring = isSemiring } - --- Preordered IdempotentSemiring (IdempotentProsemiring) - -record IdempotentProsemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _*_ - infixl 6 _+_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - 0# : Carrier - 1# : Carrier - isIdempotentProsemiring : IsIdempotentProsemiring _≈_ _≤_ _+_ _*_ 0# 1# - - open IsIdempotentProsemiring isIdempotentProsemiring public - - idempotentSemiring : IdempotentSemiring c ℓ₁ - idempotentSemiring = record { isIdempotentSemiring = isIdempotentSemiring } - --- Preordered KleeneAlgebra (proKleeneAlgebra) - -record ProKleeneAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infix 8 _⋆ - infixl 7 _*_ - infixl 6 _+_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - _⋆ : Op₁ Carrier - 0# : Carrier - 1# : Carrier - isProKleeneAlgebra : IsProKleeneAlgebra _≈_ _≤_ _+_ _*_ _⋆ 0# 1# - - open IsProKleeneAlgebra isProKleeneAlgebra public - - kleeneAlgebra : KleeneAlgebra c ℓ₁ - kleeneAlgebra = record { isKleeneAlgebra = isKleeneAlgebra } - ------------------------------------------------------------------------- --- Bundles of partially ordered structures - --- Partially ordered magmas (pomagmas) - -record Pomagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The partial order. - _∙_ : Op₂ Carrier -- Multiplication. - isPomagma : IsPomagma _≈_ _≤_ _∙_ - - open IsPomagma isPomagma public - - poset : Poset c ℓ₁ ℓ₂ - poset = record { isPartialOrder = isPartialOrder } - - promagma : Promagma c ℓ₁ ℓ₂ - promagma = record { isPromagma = isPromagma } - - open Promagma promagma public using (preorder; magma) - --- Partially ordered semigroups (posemigroups) - -record Posemigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The partial order. - _∙_ : Op₂ Carrier -- Multiplication. - isPosemigroup : IsPosemigroup _≈_ _≤_ _∙_ - - open IsPosemigroup isPosemigroup public - - pomagma : Pomagma c ℓ₁ ℓ₂ - pomagma = record { isPomagma = isPomagma } - - open Pomagma pomagma public using (preorder; poset; magma; promagma) - - prosemigroup : Prosemigroup c ℓ₁ ℓ₂ - prosemigroup = record { isProsemigroup = isProsemigroup } - - open Prosemigroup prosemigroup public using (semigroup) - --- Partially ordered monoids (pomonoids) - -record Pomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The partial order. - _∙_ : Op₂ Carrier -- The monoid multiplication. - ε : Carrier -- The monoid unit. - isPomonoid : IsPomonoid _≈_ _≤_ _∙_ ε - - open IsPomonoid isPomonoid public - - posemigroup : Posemigroup c ℓ₁ ℓ₂ - posemigroup = record { isPosemigroup = isPosemigroup } - - open Posemigroup posemigroup public using - ( preorder - ; poset - ; magma - ; promagma - ; pomagma - ; semigroup - ; prosemigroup - ) - - promonoid : Promonoid c ℓ₁ ℓ₂ - promonoid = record { isPromonoid = isPromonoid } - - open Promonoid promonoid public using (monoid) - --- Partially ordered commutative monoids (commutative pomonoids) - -record CommutativePomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _∙_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ -- The underlying equality. - _≤_ : Rel Carrier ℓ₂ -- The partial order. - _∙_ : Op₂ Carrier -- The monoid multiplication. - ε : Carrier -- The monoid unit. - isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∙_ ε - - open IsCommutativePomonoid isCommutativePomonoid public - - pomonoid : Pomonoid c ℓ₁ ℓ₂ - pomonoid = record { isPomonoid = isPomonoid } - - open Pomonoid pomonoid public using - ( preorder - ; poset - ; magma - ; promagma - ; pomagma - ; semigroup - ; prosemigroup - ; posemigroup - ; monoid - ; promonoid - ) - - commutativePromonoid : CommutativePromonoid c ℓ₁ ℓ₂ - commutativePromonoid = - record { isCommutativePromonoid = isCommutativePromonoid } - - open CommutativePromonoid commutativePromonoid public - using (commutativeSemigroup; commutativeMonoid) - --- Partially ordered semirings (posemirings) - -record Posemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _*_ - infixl 6 _+_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - 0# : Carrier - 1# : Carrier - isPosemiring : IsPosemiring _≈_ _≤_ _+_ _*_ 0# 1# - - open IsPosemiring isPosemiring public - - +-commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂ - +-commutativePomonoid = record - { isCommutativePomonoid = +-isCommutativePomonoid } - - open CommutativePomonoid +-commutativePomonoid public - using (preorder) - renaming - ( magma to +-magma - ; promagma to +-promagma - ; pomagma to +-pomagma - ; semigroup to +-semigroup - ; prosemigroup to +-prosemigroup - ; posemigroup to +-posemigroup - ; monoid to +-monoid - ; promonoid to +-promonoid - ; pomonoid to +-pomonoid - ; commutativeSemigroup to +-commutativeSemigroup - ; commutativeMonoid to +-commutativeMonoid - ; commutativePromonoid to +-commutativePromonoid - ) - - *-pomonoid : Pomonoid c ℓ₁ ℓ₂ - *-pomonoid = record { isPomonoid = *-isPomonoid } - - open Pomonoid *-pomonoid public - using () - renaming - ( magma to *-magma - ; promagma to *-promagma - ; pomagma to *-pomagma - ; semigroup to *-semigroup - ; prosemigroup to *-prosemigroup - ; posemigroup to *-posemigroup - ; monoid to *-monoid - ; promonoid to *-promonoid - ) - - prosemiring : Prosemiring c ℓ₁ ℓ₂ - prosemiring = record { isProsemiring = isProsemiring } - - open Prosemiring prosemiring public using (semiring) - --- Partially ordered idempotentSemiring (IdempotentPosemiring) - -record IdempotentPosemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infixl 7 _*_ - infixl 6 _+_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - 0# : Carrier - 1# : Carrier - isIdempotentPosemiring : IsIdempotentPosemiring _≈_ _≤_ _+_ _*_ 0# 1# - - open IsIdempotentPosemiring isIdempotentPosemiring public - - idempotentProsemiring : IdempotentProsemiring c ℓ₁ ℓ₂ - idempotentProsemiring = record { isIdempotentProsemiring = isIdempotentProsemiring } - - open IdempotentProsemiring idempotentProsemiring public using (idempotentSemiring; +-idem) - --- Partially ordered KleeneAlgebra (PoKleeneAlgebra) - -record PoKleeneAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where - infix 4 _≈_ _≤_ - infix 8 _⋆ - infixl 7 _*_ - infixl 6 _+_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ₁ - _≤_ : Rel Carrier ℓ₂ - _+_ : Op₂ Carrier - _*_ : Op₂ Carrier - _⋆ : Op₁ Carrier - 0# : Carrier - 1# : Carrier - isPoKleeneAlgebra : IsPoKleeneAlgebra _≈_ _≤_ _+_ _*_ _⋆ 0# 1# - - open IsPoKleeneAlgebra isPoKleeneAlgebra public - - proKleeneAlgebra : ProKleeneAlgebra c ℓ₁ ℓ₂ - proKleeneAlgebra = record { isProKleeneAlgebra = isProKleeneAlgebra } - - open ProKleeneAlgebra proKleeneAlgebra public using (starExpansive; starDestructive) diff --git a/src/Algebra/Ordered/Structures.agda b/src/Algebra/Ordered/Structures.agda deleted file mode 100644 index 638d8783f0..0000000000 --- a/src/Algebra/Ordered/Structures.agda +++ /dev/null @@ -1,391 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Ordered algebraic structures (not packed up with sets, orders, --- operations, etc.) ------------------------------------------------------------------------- - --- The contents of this module should be accessed via --- `Algebra.Ordered`. - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Relation.Binary.Core using (Rel; _⇒_) - -module Algebra.Ordered.Structures - {a ℓ₁ ℓ₂} {A : Set a} -- The underlying set - (_≈_ : Rel A ℓ₁) -- The underlying equality relation - (_≤_ : Rel A ℓ₂) -- The order - where - -open import Algebra.Core -open import Algebra.Definitions _≈_ -open import Algebra.Structures _≈_ -open import Data.Product.Base using (proj₁; proj₂) -open import Function.Base using (flip) -open import Level using (_⊔_) -open import Relation.Binary.Definitions using (Transitive; Monotonic₁; Monotonic₂) -open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) -open import Relation.Binary.Consequences using (mono₂⇒cong₂) - ------------------------------------------------------------------------- --- Preordered structures - --- Preordered magmas (promagmas) - -record IsPromagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPreorder : IsPreorder _≈_ _≤_ - ∙-cong : Congruent₂ ∙ - mono : Monotonic₂ _≤_ _≤_ _≤_ ∙ - - open IsPreorder isPreorder public - - mono₁ : ∀ {x} → Monotonic₁ _≤_ _≤_ (flip ∙ x) - mono₁ y≈z = mono y≈z refl - - mono₂ : ∀ {x} → Monotonic₁ _≤_ _≤_ (∙ x) - mono₂ y≈z = mono refl y≈z - - isMagma : IsMagma ∙ - isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong } - - open IsMagma isMagma public using (setoid; ∙-congˡ; ∙-congʳ) - --- Preordered semigroups (prosemigroups) - -record IsProsemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPromagma : IsPromagma ∙ - assoc : Associative ∙ - - open IsPromagma isPromagma public - - isSemigroup : IsSemigroup ∙ - isSemigroup = record { isMagma = isMagma ; assoc = assoc } - --- Preordered monoids (promonoids) - -record IsPromonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isProsemigroup : IsProsemigroup ∙ - identity : Identity ε ∙ - - open IsProsemigroup isProsemigroup public - - isMonoid : IsMonoid ∙ ε - isMonoid = record { isSemigroup = isSemigroup ; identity = identity } - - open IsMonoid isMonoid public using (identityˡ; identityʳ) - --- Preordered commutative monoids (commutative promonoids) - -record IsCommutativePromonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPromonoid : IsPromonoid ∙ ε - comm : Commutative ∙ - - open IsPromonoid isPromonoid public - - isCommutativeMonoid : IsCommutativeMonoid ∙ ε - isCommutativeMonoid = record { isMonoid = isMonoid ; comm = comm } - - open IsCommutativeMonoid isCommutativeMonoid public - using (isCommutativeSemigroup) - --- Preordered semirings (prosemirings) - -record IsProsemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - +-isCommutativePromonoid : IsCommutativePromonoid + 0# - *-cong : Congruent₂ * - *-mono : Monotonic₂ _≤_ _≤_ _≤_ * - *-assoc : Associative * - *-identity : Identity 1# * - distrib : * DistributesOver + - zero : Zero 0# * - - open IsCommutativePromonoid +-isCommutativePromonoid public - renaming - ( assoc to +-assoc - ; ∙-cong to +-cong - ; ∙-congˡ to +-congˡ - ; ∙-congʳ to +-congʳ - ; mono to +-mono - ; mono₁ to +-mono₁ - ; mono₂ to +-mono₂ - ; identity to +-identity - ; identityˡ to +-identityˡ - ; identityʳ to +-identityʳ - ; comm to +-comm - ; isMagma to +-isMagma - ; isSemigroup to +-isSemigroup - ; isMonoid to +-isMonoid - ; isCommutativeSemigroup to +-isCommutativeSemigroup - ; isCommutativeMonoid to +-isCommutativeMonoid - ) - - *-isPromonoid : IsPromonoid * 1# - *-isPromonoid = record - { isProsemigroup = record - { isPromagma = record - { isPreorder = isPreorder - ; ∙-cong = *-cong - ; mono = *-mono - } - ; assoc = *-assoc - } - ; identity = *-identity - } - - open IsPromonoid *-isPromonoid public - using () - renaming - ( ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ - ; mono₁ to *-mono₁ - ; mono₂ to *-mono₂ - ; identityˡ to *-identityˡ - ; identityʳ to *-identityʳ - ; isMagma to *-isMagma - ; isSemigroup to *-isSemigroup - ; isMonoid to *-isMonoid - ) - - isSemiring : IsSemiring + * 0# 1# - isSemiring = record - { isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = +-isCommutativeMonoid - ; *-cong = *-cong - ; *-assoc = *-assoc - ; *-identity = *-identity - ; distrib = distrib - } - ; zero = zero - } - - open IsSemiring isSemiring public using (distribˡ; distribʳ; zeroˡ; zeroʳ) - --- Preordered IdempotentSemiring (IdempotentProsemiring) - -record IsIdempotentProsemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isProsemiring : IsProsemiring + * 0# 1# - +-idem : Idempotent + - - open IsProsemiring isProsemiring public - - isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# - isIdempotentSemiring = record { isSemiring = isSemiring ; +-idem = +-idem } - - open IsIdempotentSemiring isIdempotentSemiring public using (+-idem) - --- Preordered KleeneAlgebra (proKleeneAlgebra) - -record IsProKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isIdempotentProsemiring : IsIdempotentProsemiring + * 0# 1# - starExpansive : StarExpansive 1# + * ⋆ - starDestructive : StarDestructive + * ⋆ - - open IsIdempotentProsemiring isIdempotentProsemiring public - - isKleeneAlgebra : IsKleeneAlgebra + * ⋆ 0# 1# - isKleeneAlgebra = record - { isIdempotentSemiring = isIdempotentSemiring - ; starExpansive = starExpansive - ; starDestructive = starDestructive - } - - open IsKleeneAlgebra isKleeneAlgebra public using (starExpansive; starDestructive) - ------------------------------------------------------------------------- --- Partially ordered structures - --- Partially ordered magmas (pomagmas) - -record IsPomagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPartialOrder : IsPartialOrder _≈_ _≤_ - mono : Monotonic₂ _≤_ _≤_ _≤_ ∙ - - open IsPartialOrder isPartialOrder public - - ∙-cong : Congruent₂ ∙ - ∙-cong = mono₂⇒cong₂ _≈_ _≈_ Eq.sym reflexive antisym mono - - isPromagma : IsPromagma ∙ - isPromagma = record - { isPreorder = isPreorder - ; ∙-cong = ∙-cong - ; mono = mono - } - - open IsPromagma isPromagma public - using (setoid; ∙-congˡ; ∙-congʳ; mono₁; mono₂; isMagma) - --- Partially ordered semigroups (posemigroups) - -record IsPosemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPomagma : IsPomagma ∙ - assoc : Associative ∙ - - open IsPomagma isPomagma public - - isProsemigroup : IsProsemigroup ∙ - isProsemigroup = record { isPromagma = isPromagma ; assoc = assoc } - - open IsProsemigroup isProsemigroup public using (isSemigroup) - --- Partially ordered monoids (pomonoids) - -record IsPomonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPosemigroup : IsPosemigroup ∙ - identity : Identity ε ∙ - - open IsPosemigroup isPosemigroup public - - isPromonoid : IsPromonoid ∙ ε - isPromonoid = record - { isProsemigroup = isProsemigroup - ; identity = identity - } - - open IsPromonoid isPromonoid public - using (isMonoid; identityˡ; identityʳ) - --- Partially ordered commutative monoids (commutative pomonoids) - -record IsCommutativePomonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPomonoid : IsPomonoid ∙ ε - comm : Commutative ∙ - - open IsPomonoid isPomonoid public - - isCommutativePromonoid : IsCommutativePromonoid ∙ ε - isCommutativePromonoid = record { isPromonoid = isPromonoid ; comm = comm } - - open IsCommutativePromonoid isCommutativePromonoid public - using (isCommutativeMonoid; isCommutativeSemigroup) - --- Partially ordered semirings (posemirings) - -record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - +-isCommutativePomonoid : IsCommutativePomonoid + 0# - *-mono : Monotonic₂ _≤_ _≤_ _≤_ * - *-assoc : Associative * - *-identity : Identity 1# * - distrib : * DistributesOver + - zero : Zero 0# * - - open IsCommutativePomonoid +-isCommutativePomonoid public - renaming - ( assoc to +-assoc - ; ∙-cong to +-cong - ; ∙-congˡ to +-congˡ - ; ∙-congʳ to +-congʳ - ; mono to +-mono - ; mono₁ to +-mono₁ - ; mono₂ to +-mono₂ - ; identity to +-identity - ; identityˡ to +-identityˡ - ; identityʳ to +-identityʳ - ; comm to +-comm - ; isMagma to +-isMagma - ; isPromagma to +-isPromagma - ; isPomagma to +-isPomagma - ; isSemigroup to +-isSemigroup - ; isProsemigroup to +-isProsemigroup - ; isPosemigroup to +-isPosemigroup - ; isMonoid to +-isMonoid - ; isPromonoid to +-isPromonoid - ; isPomonoid to +-isPomonoid - ; isCommutativeSemigroup to +-isCommutativeSemigroup - ; isCommutativeMonoid to +-isCommutativeMonoid - ; isCommutativePromonoid to +-isCommutativePromonoid - ) - - *-isPomonoid : IsPomonoid * 1# - *-isPomonoid = record - { isPosemigroup = record - { isPomagma = record - { isPartialOrder = isPartialOrder - ; mono = *-mono - } - ; assoc = *-assoc - } - ; identity = *-identity - } - - open IsPomonoid *-isPomonoid public - using () - renaming - ( ∙-cong to *-cong - ; ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ - ; mono₁ to *-mono₁ - ; mono₂ to *-mono₂ - ; identityˡ to *-identityˡ - ; identityʳ to *-identityʳ - ; isMagma to *-isMagma - ; isPromagma to *-isPromagma - ; isPomagma to *-isPomagma - ; isSemigroup to *-isSemigroup - ; isProsemigroup to *-isProsemigroup - ; isPosemigroup to *-isPosemigroup - ; isMonoid to *-isMonoid - ; isPromonoid to *-isPromonoid - ) - - isProsemiring : IsProsemiring + * 0# 1# - isProsemiring = record - { +-isCommutativePromonoid = +-isCommutativePromonoid - ; *-cong = *-cong - ; *-mono = *-mono - ; *-assoc = *-assoc - ; *-identity = *-identity - ; distrib = distrib - ; zero = zero - } - - open IsProsemiring isProsemiring public - using (isSemiring; distribˡ; distribʳ; zeroˡ; zeroʳ) - --- Partially ordered idempotentSemiring (IdempotentPosemiring) - -record IsIdempotentPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isPosemiring : IsPosemiring + * 0# 1# - +-idem : Idempotent + - - open IsPosemiring isPosemiring public - - isIdempotentProsemiring : IsIdempotentProsemiring + * 0# 1# - isIdempotentProsemiring = record { isProsemiring = isProsemiring ; +-idem = +-idem } - - open IsIdempotentProsemiring isIdempotentProsemiring public - using (isIdempotentSemiring; +-idem) - --- Partially ordered KleeneAlgebra (PoKleeneAlgebra) - -record IsPoKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - isIdempotentPosemiring : IsIdempotentPosemiring + * 0# 1# - starExpansive : StarExpansive 1# + * ⋆ - starDestructive : StarDestructive + * ⋆ - - open IsIdempotentPosemiring isIdempotentPosemiring public - - isProKleeneAlgebra : IsProKleeneAlgebra + * ⋆ 0# 1# - isProKleeneAlgebra = record - { isIdempotentProsemiring = isIdempotentProsemiring - ; starExpansive = starExpansive - ; starDestructive = starDestructive - } - - open IsProKleeneAlgebra isProKleeneAlgebra public - using (isKleeneAlgebra; starExpansive; starDestructive) diff --git a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda index 276e3a9705..4d089b6b0f 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda @@ -14,13 +14,11 @@ module Relation.Binary.Lattice.Properties.BoundedJoinSemilattice open BoundedJoinSemilattice J open import Algebra.Definitions _≈_ -open import Algebra.Ordered.Structures using (IsCommutativePomonoid) -open import Algebra.Ordered.Bundles using (CommutativePomonoid) open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; flip) open import Relation.Binary.Properties.Poset poset open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice - using (isPosemigroup; ∨-comm) + using (∨-comm) -- Bottom is an identity of the meet operation. @@ -54,24 +52,3 @@ dualBoundedMeetSemilattice = record { ⊤ = ⊥ ; isBoundedMeetSemilattice = dualIsBoundedMeetSemilattice } - --- Every bounded semilattice gives rise to a commutative pomonoid - -isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∨_ ⊥ -isCommutativePomonoid = record - { isPomonoid = record - { isPosemigroup = isPosemigroup - ; identity = identity - } - ; comm = ∨-comm - } - -commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂ -commutativePomonoid = record - { Carrier = Carrier - ; _≈_ = _≈_ - ; _≤_ = _≤_ - ; _∙_ = _∨_ - ; ε = ⊥ - ; isCommutativePomonoid = isCommutativePomonoid - } diff --git a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda index c68467f577..c94c3bad16 100644 --- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda @@ -16,8 +16,6 @@ open JoinSemilattice J import Algebra.Lattice as Alg import Algebra.Structures as Alg open import Algebra.Definitions _≈_ -open import Algebra.Ordered.Structures using (IsPosemigroup) -open import Algebra.Ordered.Bundles using (Posemigroup) open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; flip) open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_) @@ -97,26 +95,6 @@ isAlgSemilattice = record algSemilattice : Alg.Semilattice c ℓ₁ algSemilattice = record { isSemilattice = isAlgSemilattice } --- Every semilattice gives rise to a posemigroup - -isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_ -isPosemigroup = record - { isPomagma = record - { isPartialOrder = isPartialOrder - ; mono = ∨-monotonic - } - ; assoc = ∨-assoc - } - -posemigroup : Posemigroup c ℓ₁ ℓ₂ -posemigroup = record - { Carrier = Carrier - ; _≈_ = _≈_ - ; _≤_ = _≤_ - ; _∙_ = _∨_ - ; isPosemigroup = isPosemigroup - } - ------------------------------------------------------------------------ -- The dual construction is a meet semilattice. diff --git a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda index a78d4fea6a..f8fca492b7 100644 --- a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda @@ -35,7 +35,7 @@ dualJoinSemilattice = record } open J dualJoinSemilattice public - using (isAlgSemilattice; algSemilattice; isPosemigroup; posemigroup) + using (isAlgSemilattice; algSemilattice) renaming ( ∨-monotonic to ∧-monotonic ; ∨-cong to ∧-cong