diff --git a/CHANGELOG.md b/CHANGELOG.md index d5cd767374..d0316c05b6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -800,6 +800,13 @@ 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 @@ -1549,10 +1556,18 @@ Other minor changes * Added new proofs to `Relation.Binary.Lattice.Properties.{Join,Meet}Semilattice`: ```agda + isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_ + posemigroup : Posemigroup c ℓ₁ ℓ₂ ≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_ ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_ ``` +* Added new proofs to `Relation.Binary.Lattice.Properties.Bounded{Join,Meet}Semilattice`: + ```agda + isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∨_ ⊥ + commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂ + ``` + * Added new proofs to `Relation.Binary.Properties.Poset`: ```agda ≤-dec⇒≈-dec : Decidable _≤_ → Decidable _≈_ @@ -1649,6 +1664,14 @@ Other minor changes ``` Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y) Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y) + + Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_ + Antitonic₁ _≤_ _⊑_ f = f Preserves (flip _≤_) ⟶ _⊑_ + Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_ + MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_ + AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_ + Antitonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_ + Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y) ``` * Added new definitions in `Relation.Binary.Bundles`: @@ -1666,6 +1689,9 @@ Other minor changes sym⇒¬-sym : Symmetric _∼_ → Symmetric _≁_ cotrans⇒¬-trans : Cotransitive _∼_ → Transitive _≁_ irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive _≁_ + mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → + f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ → + f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂ ``` * Added new operations in `Relation.Binary.PropositionalEquality.Properties`: @@ -1945,4 +1971,4 @@ This is a full list of proofs that have changed form to use irrelevant instance ```agda Inverse⇒Injection : Inverse S T → Injection S T ↔⇒↣ : A ↔ B → A ↣ B - ``` \ No newline at end of file + ``` diff --git a/src/Algebra/Ordered.agda b/src/Algebra/Ordered.agda new file mode 100644 index 0000000000..69e726aec0 --- /dev/null +++ b/src/Algebra/Ordered.agda @@ -0,0 +1,14 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions of ordered algebraic structures like promonoids and +-- posemigroups (packed in records together with sets, orders, +-- operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --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 new file mode 100644 index 0000000000..0443c5a6cf --- /dev/null +++ b/src/Algebra/Ordered/Bundles.agda @@ -0,0 +1,346 @@ +------------------------------------------------------------------------ +-- 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 --without-K --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 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 } + +------------------------------------------------------------------------ +-- 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) diff --git a/src/Algebra/Ordered/Structures.agda b/src/Algebra/Ordered/Structures.agda new file mode 100644 index 0000000000..34a64e6519 --- /dev/null +++ b/src/Algebra/Ordered/Structures.agda @@ -0,0 +1,323 @@ +------------------------------------------------------------------------ +-- 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 --without-K --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 using (proj₁; proj₂) +open import Function 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ʳ) + +------------------------------------------------------------------------ +-- 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ʳ) diff --git a/src/Codata/Guarded/M.agda b/src/Codata/Guarded/M.agda index 28c9892241..8bcab3209b 100644 --- a/src/Codata/Guarded/M.agda +++ b/src/Codata/Guarded/M.agda @@ -20,7 +20,7 @@ record M {s p} (C : Container s p) : Set (s ⊔ p) where constructor inf open Container C - + field head : Shape tail : Position head → M C diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda index 2e622d0b12..fa8e09132c 100644 --- a/src/Relation/Binary/Consequences.agda +++ b/src/Relation/Binary/Consequences.agda @@ -98,6 +98,13 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃} (antimono (reflexive (sym p≈q))) (antimono (reflexive p≈q)) + mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → + f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ → + f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂ + mono₂⇒cong₂ sym reflexive antisym mono x≈y u≈v = antisym + (mono (reflexive x≈y) (reflexive u≈v)) + (mono (reflexive (sym x≈y)) (reflexive (sym u≈v))) + ------------------------------------------------------------------------ -- Proofs for strict orders diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index c4aa9ba9ac..2cec4ded8b 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/src/Relation/Binary/Definitions.agda @@ -139,6 +139,29 @@ Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y) Tight : Rel A ℓ₁ → Rel A ℓ₂ → Set _ Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y) +-- Properties of order morphisms, aka order-preserving maps + +Monotonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _ +Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_ + +Antitonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _ +Antitonic₁ _≤_ _⊑_ f = f Preserves (flip _≤_) ⟶ _⊑_ + +Monotonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _ +Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_ + +MonotonicAntitonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _ +MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_ + +AntitonicMonotonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _ +AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_ + +Antitonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _ +Antitonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_ + +Adjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _ +Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y) + -- Unary relations respecting a binary relation. _⟶_Respects_ : (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _ diff --git a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda index b8b49f93bc..86ad2e0881 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda @@ -14,10 +14,14 @@ 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 open import Function.Base using (_∘_; flip) open import Relation.Binary open import Relation.Binary.Properties.Poset poset +open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice + using (isPosemigroup; ∨-comm) -- Bottom is an identity of the meet operation. @@ -51,3 +55,24 @@ 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 018574df40..42904add48 100644 --- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda @@ -16,6 +16,8 @@ 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 open import Function.Base using (_∘_; flip) open import Relation.Binary @@ -93,6 +95,26 @@ 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 eb423ec1fd..532bba46f6 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) + using (isAlgSemilattice; algSemilattice; isPosemigroup; posemigroup) renaming ( ∨-monotonic to ∧-monotonic ; ∨-cong to ∧-cong