From 09f740926b147506466f3f28b5e70f7dcec20395 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 5 Jan 2023 11:31:39 +0000 Subject: [PATCH 01/20] construction of the opposite of a ring: `IsRing` proofs --- src/Algebra/Construct/Flip/Op.agda | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 471722cbd4..52860d9126 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -53,6 +53,14 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙) inverse inv = Prod.swap inv + zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + zero zer = Prod.swap zer + + module _ (+ : Op₂ A) where + + distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + distributes distrib = Prod.swap distrib + ------------------------------------------------------------------------ -- Structures @@ -163,6 +171,23 @@ module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where } where module g = IsAbelianGroup g +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where + + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + isRing r = record + { +-isAbelianGroup = r-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative ≈ * sym r.*-assoc + ; *-identity = identity ≈ * r.*-identity + ; distrib = distributes ≈ * + r.distrib + ; zero = zero ≈ * r.zero + } + where + module r = IsRing r + r-isAbelianGroup = r.+-isAbelianGroup + open IsAbelianGroup r-isAbelianGroup using (sym) + + ------------------------------------------------------------------------ -- Bundles From a681dc7447727a0217f102ad14d7848d1d2f1356 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 5 Jan 2023 11:37:19 +0000 Subject: [PATCH 02/20] `CHANGELOG` --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0cdb36f8c6..5dee17fe99 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1587,6 +1587,13 @@ Other minor changes moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` +* Added new proofs to `Algebra.Construct.Flip.Op`: + ```agda + zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + ``` + * Added new definition to `Algebra.Definitions`: ```agda LeftDividesˡ : Op₂ A → Op₂ A → Set _ From 2b93bbfb7b84419f1e45a7f981f761d56573c182 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 5 Jan 2023 11:40:34 +0000 Subject: [PATCH 03/20] bundle --- CHANGELOG.md | 3 ++- src/Algebra/Construct/Flip/Op.agda | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5dee17fe99..53a1acc6f8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1587,11 +1587,12 @@ Other minor changes moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` -* Added new proofs to `Algebra.Construct.Flip.Op`: +* Added new functions and proofs to `Algebra.Construct.Flip.Op`: ```agda zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + ring : Ring a ℓ → Ring a ℓ ``` * Added new definition to `Algebra.Definitions`: diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 52860d9126..0bf8192fc6 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -264,3 +264,7 @@ group g = record { isGroup = isGroup g.isGroup } abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } where module g = AbelianGroup g + +ring : Ring a ℓ → Ring a ℓ +ring r = record { isRing = isRing r.isRing } + where module r = Ring r From 69d0dffb1dca9c5c57d49186e786a860647159d2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 7 Jan 2023 18:33:15 +0000 Subject: [PATCH 04/20] refactored `Algebra.Construct.Zero` into `Initial` and `Terminal` --- src/Algebra/Construct/Zero.agda | 72 ++++++++++++++++++--------------- 1 file changed, 40 insertions(+), 32 deletions(-) diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index 12f5c87ffe..76eb4e08c6 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -2,13 +2,15 @@ -- The Agda standard library -- -- Instances of algebraic structures where the carrier is ⊤. --- In mathematics, this is usually called 0. +-- In mathematics, this is usually called 0 (1 in the case of Group). -- -- From monoids up, these are are zero-objects – i.e, both the initial -- and the terminal object in the relevant category. --- For structures without an identity element, we can't necessarily --- produce a homomorphism out of 0, because there is an instance of such --- a structure with an empty Carrier. +-- +-- For structures without an identity element, the terminal algebra is +-- *not* initial, because there is an instance of such a structure +-- with an empty Carrier. Accordingly, such definitions are now deprecated +-- in favour of those defined in `Algebra.Construct.Terminal`. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -17,47 +19,53 @@ open import Level using (Level) module Algebra.Construct.Zero {c ℓ : Level} where +open import Algebra.Bundles.Raw + using (RawMagma) open import Algebra.Bundles -open import Data.Unit.Polymorphic + using (Magma; Semigroup; Band) +open import Algebra.Construct.Terminal public + hiding (rawMagma; magma; semigroup; band) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new definitions re-exported from +-- `Algebra.Construct.Terminal` as continuing support for the below is +-- not guaranteed. + +-- Version 2.0 ------------------------------------------------------------------------ -- Raw bundles rawMagma : RawMagma c ℓ -rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -rawMonoid : RawMonoid c ℓ -rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } +rawMagma = Algebra.Construct.Terminal.rawMagma -rawGroup : RawGroup c ℓ -rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } +{-# WARNING_ON_USAGE rawMagma +"Warning: rawMagma was deprecated in v2.0. +Please use Algebra.Construct.Terminal.rawMagma instead." +#-} ------------------------------------------------------------------------ -- Bundles magma : Magma c ℓ -magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } +magma = Algebra.Construct.Terminal.magma +{-# WARNING_ON_USAGE magma +"Warning: magma was deprecated in v2.0. +Please use Algebra.Construct.Terminal.magma instead." +#-} semigroup : Semigroup c ℓ -semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } +semigroup = Algebra.Construct.Terminal.semigroup +{-# WARNING_ON_USAGE semigroup +"Warning: semigroup was deprecated in v2.0. +Please use Algebra.Construct.Terminal.semigroup instead." +#-} band : Band c ℓ -band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -commutativeSemigroup : CommutativeSemigroup c ℓ -commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -monoid : Monoid c ℓ -monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -commutativeMonoid : CommutativeMonoid c ℓ -commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ -idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -group : Group c ℓ -group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } - -abelianGroup : AbelianGroup c ℓ -abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } +band = Algebra.Construct.Terminal.band +{-# WARNING_ON_USAGE semigroup +"Warning: semigroup was deprecated in v2.0. +Please use Algebra.Construct.Terminal.semigroup instead." +#-} From 92305c2f3cfaeeba0688cbf544b8d1d0c5b88da6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 7 Jan 2023 18:34:08 +0000 Subject: [PATCH 05/20] added `Algebra.Construct.Initial` and `Terminal` --- src/Algebra/Construct/Initial.agda | 92 +++++++++++++++++++++++++++++ src/Algebra/Construct/Terminal.agda | 85 ++++++++++++++++++++++++++ 2 files changed, 177 insertions(+) create mode 100644 src/Algebra/Construct/Initial.agda create mode 100644 src/Algebra/Construct/Terminal.agda diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda new file mode 100644 index 0000000000..538fc34d83 --- /dev/null +++ b/src/Algebra/Construct/Initial.agda @@ -0,0 +1,92 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Instances of algebraic structures where the carrier is ⊥. +-- In mathematics, this is usually called 0. +-- +-- From monoids up, these are zero-objects – i.e, the initial +-- object is the terminal object in the relevant category. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Algebra.Construct.Initial {c ℓ : Level} where + +open import Algebra.Bundles + using (Magma; Semigroup; Band) +open import Algebra.Bundles.Raw + using (RawMagma) +open import Algebra.Core using (Op₂) +open import Algebra.Definitions using (Congruent₂) +open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand) +open import Data.Empty.Polymorphic +open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence) + + +------------------------------------------------------------------------ +-- re-export those algebras which are also terminal + +open import Algebra.Construct.Terminal {c} {ℓ} public + hiding (rawMagma; magma; semigroup; band) + +------------------------------------------------------------------------ +-- gather all the functionality in one place + +private module ℤero where + + infixl 7 _∙_ + infix 4 _≈_ + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + + Carrier = ⊥ + _≈_ () + _∙_ () + + refl : Reflexive _≈_ + refl {x = ()} + + sym : Symmetric _≈_ + sym {x = ()} + + trans : Transitive _≈_ + trans {i = ()} + + isEquivalence : IsEquivalence _≈_ + isEquivalence = record { refl = refl ; sym = sym ; trans = trans } + + ∙-cong : Congruent₂ _≈_ _∙_ + ∙-cong {x = ()} + + isMagma : IsMagma _≈_ _∙_ + isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong } + + isSemigroup : IsSemigroup _≈_ _∙_ + isSemigroup = record { isMagma = isMagma ; assoc = λ () } + + isBand : IsBand _≈_ _∙_ + isBand = record { isSemigroup = isSemigroup ; idem = λ () } + +open ℤero + +------------------------------------------------------------------------ +-- Raw bundles + +rawMagma : RawMagma c ℓ +rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ } + +------------------------------------------------------------------------ +-- Bundles + +magma : Magma c ℓ +magma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; isMagma = isMagma } + +semigroup : Semigroup c ℓ +semigroup = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; isSemigroup = isSemigroup } + +band : Band c ℓ +band = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; isBand = isBand } + diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda new file mode 100644 index 0000000000..c964f4570f --- /dev/null +++ b/src/Algebra/Construct/Terminal.agda @@ -0,0 +1,85 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Instances of algebraic structures where the carrier is ⊤. +-- In mathematics, this is usually called 0 (1 in the case of Group). +-- +-- From monoids up, these are zero-objects – i.e, both the initial +-- and the terminal object in the relevant category. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Algebra.Construct.Terminal {c ℓ : Level} where + +open import Algebra.Bundles +open import Data.Unit.Polymorphic +open import Relation.Binary.Core using (Rel) + +private module 𝕆ne where + + infix 4 _≈_ + Carrier : Set c + _≈_ : Rel Carrier ℓ + + Carrier = ⊤ + _ ≈ _ = ⊤ + +open 𝕆ne + +------------------------------------------------------------------------ +-- Raw bundles + +rawMagma : RawMagma c ℓ +rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ } + +rawMonoid : RawMonoid c ℓ +rawMonoid = record { Carrier = Carrier ; _≈_ = _≈_ } + +rawGroup : RawGroup c ℓ +rawGroup = record { Carrier = Carrier ; _≈_ = _≈_ } + +rawSemiring : RawSemiring c ℓ +rawSemiring = record { Carrier = Carrier ; _≈_ = _≈_ } + +rawRing : RawRing c ℓ +rawRing = record { Carrier = Carrier ; _≈_ = _≈_ } + +------------------------------------------------------------------------ +-- Bundles + +magma : Magma c ℓ +magma = record { Carrier = Carrier ; _≈_ = _≈_ } + +semigroup : Semigroup c ℓ +semigroup = record { Carrier = Carrier ; _≈_ = _≈_ } + +band : Band c ℓ +band = record { Carrier = Carrier ; _≈_ = _≈_ } + +commutativeSemigroup : CommutativeSemigroup c ℓ +commutativeSemigroup = record { Carrier = Carrier ; _≈_ = _≈_ } + +monoid : Monoid c ℓ +monoid = record { Carrier = Carrier ; _≈_ = _≈_ } + +commutativeMonoid : CommutativeMonoid c ℓ +commutativeMonoid = record { Carrier = Carrier ; _≈_ = _≈_ } + +idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ +idempotentCommutativeMonoid = record { Carrier = Carrier ; _≈_ = _≈_ } + +group : Group c ℓ +group = record { Carrier = Carrier ; _≈_ = _≈_ } + +abelianGroup : AbelianGroup c ℓ +abelianGroup = record { Carrier = Carrier ; _≈_ = _≈_ } + +semiring : Semiring c ℓ +semiring = record { Carrier = Carrier ; _≈_ = _≈_ } + +ring : Ring c ℓ +ring = record { Carrier = Carrier ; _≈_ = _≈_ } + From 0d2a36dd43e52082ca87148cfa8839ed85d697e6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 7 Jan 2023 19:02:56 +0000 Subject: [PATCH 06/20] refactored `Zero` for modules --- src/Algebra/Construct/Zero.agda | 6 --- src/Algebra/Module/Construct/Zero.agda | 52 ++++++++++---------------- 2 files changed, 20 insertions(+), 38 deletions(-) diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index 76eb4e08c6..512bb2e751 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -35,9 +35,6 @@ open import Algebra.Construct.Terminal public -- Version 2.0 ------------------------------------------------------------------------- --- Raw bundles - rawMagma : RawMagma c ℓ rawMagma = Algebra.Construct.Terminal.rawMagma @@ -46,9 +43,6 @@ rawMagma = Algebra.Construct.Terminal.rawMagma Please use Algebra.Construct.Terminal.rawMagma instead." #-} ------------------------------------------------------------------------- --- Bundles - magma : Magma c ℓ magma = Algebra.Construct.Terminal.magma {-# WARNING_ON_USAGE magma diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index ada60892c5..2247d6696f 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -17,56 +17,44 @@ module Algebra.Module.Construct.Zero {c ℓ : Level} where open import Algebra.Bundles open import Algebra.Module.Bundles open import Data.Unit.Polymorphic +open import Relation.Binary.Core using (Rel) private variable r s ℓr ℓs : Level +private module ℤero where + + infix 4 _≈_ + Carrier : Set c + _≈_ : Rel Carrier ℓ + + Carrier = ⊤ + _ ≈ _ = ⊤ + +open ℤero + leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ -leftSemimodule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +leftSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S c ℓ -rightSemimodule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +rightSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } bisemimodule : {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S c ℓ -bisemimodule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +bisemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R c ℓ -semimodule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +semimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } leftModule : {R : Ring r ℓr} → LeftModule R c ℓ -leftModule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +leftModule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } rightModule : {S : Ring s ℓs} → RightModule S c ℓ -rightModule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +rightModule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S c ℓ -bimodule = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +bimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } ⟨module⟩ : {R : CommutativeRing r ℓr} → Module R c ℓ -⟨module⟩ = record - { Carrierᴹ = ⊤ - ; _≈ᴹ_ = λ _ _ → ⊤ - } +⟨module⟩ = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } From 22b5b22873ce90277669d91cb3775fff49b81802 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 7 Jan 2023 19:17:26 +0000 Subject: [PATCH 07/20] consistency between sources --- src/Algebra/Construct/Terminal.agda | 3 +++ src/Algebra/Construct/Zero.agda | 4 ++++ src/Algebra/Module/Construct/Zero.agda | 12 ++++++++++++ 3 files changed, 19 insertions(+) diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda index c964f4570f..62b143ffa5 100644 --- a/src/Algebra/Construct/Terminal.agda +++ b/src/Algebra/Construct/Terminal.agda @@ -18,6 +18,9 @@ open import Algebra.Bundles open import Data.Unit.Polymorphic open import Relation.Binary.Core using (Rel) +------------------------------------------------------------------------ +-- gather all the functionality in one place + private module 𝕆ne where infix 4 _≈_ diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index 512bb2e751..39e097d182 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -23,6 +23,10 @@ open import Algebra.Bundles.Raw using (RawMagma) open import Algebra.Bundles using (Magma; Semigroup; Band) + +------------------------------------------------------------------------ +-- re-export those algebras which are both initial and terminal + open import Algebra.Construct.Terminal public hiding (rawMagma; magma; semigroup; band) diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index 2247d6696f..b6a1b2d637 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -23,6 +23,9 @@ private variable r s ℓr ℓs : Level +------------------------------------------------------------------------ +-- gather all the functionality in one place + private module ℤero where infix 4 _≈_ @@ -34,6 +37,15 @@ private module ℤero where open ℤero +------------------------------------------------------------------------ +-- Raw bundles NOT YET IMPLEMENTED issue #1828 +{- +rawModule : RawModule c ℓ +rawModule = record { Carrier = Carrier ; _≈_ = _≈_ } +-} +------------------------------------------------------------------------ +-- Bundles + leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ leftSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } From e54f2a70d475ada3a946b439c1ddc92af3da2a72 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 7 Jan 2023 19:54:21 +0000 Subject: [PATCH 08/20] `CHANGELOG` --- CHANGELOG.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0cdb36f8c6..486778805c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -605,6 +605,8 @@ Non-backwards compatible changes * New modules: ``` + Algebra.Construct.Initial + Algebra.Construct.Terminal Data.List.Effectful.Transformer Data.List.NonEmpty.Effectful.Transformer Data.Maybe.Effectful.Transformer @@ -870,6 +872,14 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Construct.Zero`: + ```agda + rawMagma ↦ Algebra.Construct.Terminal.rawMagma + magma ↦ Algebra.Construct.Terminal.magma + semigroup ↦ Algebra.Construct.Terminal.semigroup + band ↦ Algebra.Construct.Terminal.band + ``` + * In `Codata.Guarded.Stream.Properties`: ```agda map-identity ↦ map-id From 3891c168d1a4d2c2b3a3a6b279f35135cef000fc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 8 Jan 2023 10:49:13 +0000 Subject: [PATCH 09/20] removed unnecessary imports from `Data.Unit` --- src/Data/Unit.agda | 2 -- src/Data/Unit/Base.agda | 2 -- 2 files changed, 4 deletions(-) diff --git a/src/Data/Unit.agda b/src/Data/Unit.agda index fd03e9bcad..22a97b4af9 100644 --- a/src/Data/Unit.agda +++ b/src/Data/Unit.agda @@ -8,8 +8,6 @@ module Data.Unit where -import Relation.Binary.PropositionalEquality as PropEq - ------------------------------------------------------------------------ -- Re-export contents of base module diff --git a/src/Data/Unit/Base.agda b/src/Data/Unit/Base.agda index b30cd40d40..49ae91be88 100644 --- a/src/Data/Unit/Base.agda +++ b/src/Data/Unit/Base.agda @@ -6,8 +6,6 @@ {-# OPTIONS --without-K --safe #-} -open import Agda.Builtin.Equality using (_≡_) - module Data.Unit.Base where ------------------------------------------------------------------------ From 7c592c104e782547c40d8259062408a14341248c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 14:30:48 +0000 Subject: [PATCH 10/20] Matthew's feedback --- src/Algebra/Construct/Initial.agda | 41 +++++++++++++++++------------- 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda index 538fc34d83..14b1b32fef 100644 --- a/src/Algebra/Construct/Initial.agda +++ b/src/Algebra/Construct/Initial.agda @@ -38,12 +38,14 @@ private module ℤero where infixl 7 _∙_ infix 4 _≈_ - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∙_ : Op₂ Carrier + Carrier : Set c Carrier = ⊥ + + _≈_ : Rel Carrier ℓ _≈_ () + + _∙_ : Op₂ Carrier _∙_ () refl : Reflexive _≈_ @@ -55,21 +57,9 @@ private module ℤero where trans : Transitive _≈_ trans {i = ()} - isEquivalence : IsEquivalence _≈_ - isEquivalence = record { refl = refl ; sym = sym ; trans = trans } - ∙-cong : Congruent₂ _≈_ _∙_ ∙-cong {x = ()} - isMagma : IsMagma _≈_ _∙_ - isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong } - - isSemigroup : IsSemigroup _≈_ _∙_ - isSemigroup = record { isMagma = isMagma ; assoc = λ () } - - isBand : IsBand _≈_ _∙_ - isBand = record { isSemigroup = isSemigroup ; idem = λ () } - open ℤero ------------------------------------------------------------------------ @@ -78,15 +68,30 @@ open ℤero rawMagma : RawMagma c ℓ rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ } +------------------------------------------------------------------------ +-- Structures + +isEquivalence : IsEquivalence _≈_ +isEquivalence = record { refl = refl ; sym = sym ; trans = trans } + +isMagma : IsMagma _≈_ _∙_ +isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong } + +isSemigroup : IsSemigroup _≈_ _∙_ +isSemigroup = record { isMagma = isMagma ; assoc = λ () } + +isBand : IsBand _≈_ _∙_ +isBand = record { isSemigroup = isSemigroup ; idem = λ () } + ------------------------------------------------------------------------ -- Bundles magma : Magma c ℓ -magma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; isMagma = isMagma } +magma = record { isMagma = isMagma } semigroup : Semigroup c ℓ -semigroup = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; isSemigroup = isSemigroup } +semigroup = record { isSemigroup = isSemigroup } band : Band c ℓ -band = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; isBand = isBand } +band = record { isBand = isBand } From 83cb803942ae45b7bd03379b0201e910cacdb12f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 14:33:20 +0000 Subject: [PATCH 11/20] capitalise comments --- src/Algebra/Construct/Zero.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index 39e097d182..dccfd9d0c6 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -25,7 +25,7 @@ open import Algebra.Bundles using (Magma; Semigroup; Band) ------------------------------------------------------------------------ --- re-export those algebras which are both initial and terminal +-- Re-export those algebras which are both initial and terminal open import Algebra.Construct.Terminal public hiding (rawMagma; magma; semigroup; band) From 46aa741465a3170d87498763b527e0fa4f2d5200 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 14:37:48 +0000 Subject: [PATCH 12/20] =?UTF-8?q?reorder=20declarations=20in=20`?= =?UTF-8?q?=F0=9D=95=86ne`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Construct/Terminal.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda index 62b143ffa5..b932710c57 100644 --- a/src/Algebra/Construct/Terminal.agda +++ b/src/Algebra/Construct/Terminal.agda @@ -19,15 +19,15 @@ open import Data.Unit.Polymorphic open import Relation.Binary.Core using (Rel) ------------------------------------------------------------------------ --- gather all the functionality in one place +-- Gather all the functionality in one place private module 𝕆ne where infix 4 _≈_ Carrier : Set c - _≈_ : Rel Carrier ℓ - Carrier = ⊤ + + _≈_ : Rel Carrier ℓ _ ≈ _ = ⊤ open 𝕆ne From 0575c70abb28270bac2aeee7d5a17094124516f3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 14:59:56 +0000 Subject: [PATCH 13/20] Matthew's simplifications --- src/Algebra/Construct/Flip/Op.agda | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 0bf8192fc6..fa58630c10 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -56,10 +56,10 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) zero zer = Prod.swap zer - module _ (+ : Op₂ A) where +module _ (≈ : Rel A ℓ) (* + : Op₂ A) where - distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + - distributes distrib = Prod.swap distrib + distributes : (≈ DistributesOver *) + → (≈ DistributesOver (flip *)) + + distributes distrib = Prod.swap distrib ------------------------------------------------------------------------ -- Structures @@ -175,17 +175,15 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# isRing r = record - { +-isAbelianGroup = r-isAbelianGroup + { +-isAbelianGroup = r.+-isAbelianGroup ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong - ; *-assoc = associative ≈ * sym r.*-assoc + ; *-assoc = associative ≈ * r.sym r.*-assoc ; *-identity = identity ≈ * r.*-identity ; distrib = distributes ≈ * + r.distrib ; zero = zero ≈ * r.zero } where module r = IsRing r - r-isAbelianGroup = r.+-isAbelianGroup - open IsAbelianGroup r-isAbelianGroup using (sym) ------------------------------------------------------------------------ From a0f96d8ceb5414d5baa3e08b9f24313e91f4f2af Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 15:26:48 +0000 Subject: [PATCH 14/20] making things 'a little nicer' --- src/Algebra/Construct/Flip/Op.agda | 110 +++++++++++++++++------------ 1 file changed, 63 insertions(+), 47 deletions(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index fa58630c10..f8293df928 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -9,7 +9,10 @@ module Algebra.Construct.Flip.Op where -open import Algebra +open import Algebra.Core +open import Algebra.Bundles +import Algebra.Definitions as Def +import Algebra.Structures as Str import Data.Product as Prod import Data.Sum as Sum open import Function.Base using (flip) @@ -33,32 +36,36 @@ preserves₂ : (∼ ≈ ≋ : Rel A ℓ) → ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋ preserves₂ _ _ _ pres = flip pres -module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where +module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where - associative : Symmetric ≈ → Associative ≈ ∙ → Associative ≈ (flip ∙) + open Def ≈ + + associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙) associative sym assoc x y z = sym (assoc z y x) - identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙) + identity : Identity ε ∙ → Identity ε (flip ∙) identity id = Prod.swap id - commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙) + commutative : Commutative ∙ → Commutative (flip ∙) commutative comm = flip comm - selective : Selective ≈ ∙ → Selective ≈ (flip ∙) + selective : Selective ∙ → Selective (flip ∙) selective sel x y = Sum.swap (sel y x) - idempotent : Idempotent ≈ ∙ → Idempotent ≈ (flip ∙) + idempotent : Idempotent ∙ → Idempotent (flip ∙) idempotent idem = idem - inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙) + inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙) inverse inv = Prod.swap inv - zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + zero : Zero ε ∙ → Zero ε (flip ∙) zero zer = Prod.swap zer -module _ (≈ : Rel A ℓ) (* + : Op₂ A) where +module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where + + open Def ≈ - distributes : (≈ DistributesOver *) + → (≈ DistributesOver (flip *)) + + distributes : * DistributesOver + → (flip *) DistributesOver + distributes distrib = Prod.swap distrib ------------------------------------------------------------------------ @@ -66,121 +73,129 @@ module _ (≈ : Rel A ℓ) (* + : Op₂ A) where module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where - isMagma : IsMagma ≈ ∙ → IsMagma ≈ (flip ∙) + open Def ≈ + open Str ≈ + open ∙-Properties ≈ ∙ + + isMagma : IsMagma ∙ → IsMagma (flip ∙) isMagma m = record { isEquivalence = isEquivalence ; ∙-cong = preserves₂ ≈ ≈ ≈ ∙-cong } where open IsMagma m - isSelectiveMagma : IsSelectiveMagma ≈ ∙ → IsSelectiveMagma ≈ (flip ∙) + isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙) isSelectiveMagma m = record { isMagma = isMagma m.isMagma - ; sel = selective ≈ ∙ m.sel + ; sel = selective m.sel } where module m = IsSelectiveMagma m - isCommutativeMagma : IsCommutativeMagma ≈ ∙ → IsCommutativeMagma ≈ (flip ∙) + isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙) isCommutativeMagma m = record { isMagma = isMagma m.isMagma - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMagma m - isSemigroup : IsSemigroup ≈ ∙ → IsSemigroup ≈ (flip ∙) + isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙) isSemigroup s = record { isMagma = isMagma s.isMagma - ; assoc = associative ≈ ∙ s.sym s.assoc + ; assoc = associative s.sym s.assoc } where module s = IsSemigroup s - isBand : IsBand ≈ ∙ → IsBand ≈ (flip ∙) + isBand : IsBand ∙ → IsBand (flip ∙) isBand b = record { isSemigroup = isSemigroup b.isSemigroup ; idem = b.idem } where module b = IsBand b - isCommutativeSemigroup : IsCommutativeSemigroup ≈ ∙ → - IsCommutativeSemigroup ≈ (flip ∙) + isCommutativeSemigroup : IsCommutativeSemigroup ∙ → + IsCommutativeSemigroup (flip ∙) isCommutativeSemigroup s = record { isSemigroup = isSemigroup s.isSemigroup - ; comm = commutative ≈ ∙ s.comm + ; comm = commutative s.comm } where module s = IsCommutativeSemigroup s - isUnitalMagma : IsUnitalMagma ≈ ∙ ε → IsUnitalMagma ≈ (flip ∙) ε + isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε isUnitalMagma m = record { isMagma = isMagma m.isMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsUnitalMagma m - isMonoid : IsMonoid ≈ ∙ ε → IsMonoid ≈ (flip ∙) ε + isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε isMonoid m = record { isSemigroup = isSemigroup m.isSemigroup - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsMonoid m - isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε → - IsCommutativeMonoid ≈ (flip ∙) ε + isCommutativeMonoid : IsCommutativeMonoid ∙ ε → + IsCommutativeMonoid (flip ∙) ε isCommutativeMonoid m = record { isMonoid = isMonoid m.isMonoid - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMonoid m - isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ≈ ∙ ε → - IsIdempotentCommutativeMonoid ≈ (flip ∙) ε + isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε → + IsIdempotentCommutativeMonoid (flip ∙) ε isIdempotentCommutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid - ; idem = idempotent ≈ ∙ m.idem + ; idem = idempotent m.idem } where module m = IsIdempotentCommutativeMonoid m - isInvertibleMagma : IsInvertibleMagma ≈ ∙ ε ⁻¹ → - IsInvertibleMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ → + IsInvertibleMagma (flip ∙) ε ⁻¹ isInvertibleMagma m = record { isMagma = isMagma m.isMagma - ; inverse = inverse ≈ ∙ m.inverse + ; inverse = inverse m.inverse ; ⁻¹-cong = m.⁻¹-cong } where module m = IsInvertibleMagma m - isInvertibleUnitalMagma : IsInvertibleUnitalMagma ≈ ∙ ε ⁻¹ → - IsInvertibleUnitalMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ → + IsInvertibleUnitalMagma (flip ∙) ε ⁻¹ isInvertibleUnitalMagma m = record { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsInvertibleUnitalMagma m - isGroup : IsGroup ≈ ∙ ε ⁻¹ → IsGroup ≈ (flip ∙) ε ⁻¹ + isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹ isGroup g = record { isMonoid = isMonoid g.isMonoid - ; inverse = inverse ≈ ∙ g.inverse + ; inverse = inverse g.inverse ; ⁻¹-cong = g.⁻¹-cong } where module g = IsGroup g - isAbelianGroup : IsAbelianGroup ≈ ∙ ε ⁻¹ → IsAbelianGroup ≈ (flip ∙) ε ⁻¹ + isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹ isAbelianGroup g = record { isGroup = isGroup g.isGroup - ; comm = commutative ≈ ∙ g.comm + ; comm = commutative g.comm } where module g = IsAbelianGroup g module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where - isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1# isRing r = record { +-isAbelianGroup = r.+-isAbelianGroup ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong - ; *-assoc = associative ≈ * r.sym r.*-assoc - ; *-identity = identity ≈ * r.*-identity - ; distrib = distributes ≈ * + r.distrib - ; zero = zero ≈ * r.zero + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero } where module r = IsRing r @@ -266,3 +281,4 @@ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } ring : Ring a ℓ → Ring a ℓ ring r = record { isRing = isRing r.isRing } where module r = Ring r + From 3b0923c7a5c40e4b459f9db932d5cda453fc9a28 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 15:30:54 +0000 Subject: [PATCH 15/20] fix-whitespace --- src/Algebra/Construct/Flip/Op.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index f8293df928..1075a1e942 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -187,7 +187,7 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where open Str ≈ open ∙-Properties ≈ * open *-Properties ≈ * + - + isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1# isRing r = record { +-isAbelianGroup = r.+-isAbelianGroup From 5baffdee43bb86c2b38e29789e0487df334fce97 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 10 Jan 2023 21:07:19 +0000 Subject: [PATCH 16/20] added `CommutativeRing` to the tally --- CHANGELOG.md | 2 ++ src/Algebra/Construct/Flip/Op.agda | 12 ++++++++++++ 2 files changed, 14 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 50b786364b..ab73889cf9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1602,7 +1602,9 @@ Other minor changes zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + isCommutativeRing : IsCommutativeRing ≈ + * - 0# 1# → IsCommutativeRing ≈ + (flip *) - 0# 1# ring : Ring a ℓ → Ring a ℓ + commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ ``` * Added new definition to `Algebra.Definitions`: diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 1075a1e942..88c660bd52 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -200,6 +200,14 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where where module r = IsRing r + isCommutativeRing : IsCommutativeRing + * - 0# 1# → IsCommutativeRing + (flip *) - 0# 1# + isCommutativeRing r = record + { isRing = isRing r.isRing + ; *-comm = commutative r.*-comm + } + where + module r = IsCommutativeRing r + ------------------------------------------------------------------------ -- Bundles @@ -282,3 +290,7 @@ ring : Ring a ℓ → Ring a ℓ ring r = record { isRing = isRing r.isRing } where module r = Ring r +commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ +commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing } + where module r = CommutativeRing r + From 1fbffaba8136f0c5e42b66aacba163241b43b80d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 10 Jan 2023 21:09:48 +0000 Subject: [PATCH 17/20] Bogus commits have entered the picture. Revert "added `CommutativeRing` to the tally" This reverts commit 5baffdee43bb86c2b38e29789e0487df334fce97. --- CHANGELOG.md | 2 -- src/Algebra/Construct/Flip/Op.agda | 12 ------------ 2 files changed, 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ab73889cf9..50b786364b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1602,9 +1602,7 @@ Other minor changes zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# - isCommutativeRing : IsCommutativeRing ≈ + * - 0# 1# → IsCommutativeRing ≈ + (flip *) - 0# 1# ring : Ring a ℓ → Ring a ℓ - commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ ``` * Added new definition to `Algebra.Definitions`: diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 88c660bd52..1075a1e942 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -200,14 +200,6 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where where module r = IsRing r - isCommutativeRing : IsCommutativeRing + * - 0# 1# → IsCommutativeRing + (flip *) - 0# 1# - isCommutativeRing r = record - { isRing = isRing r.isRing - ; *-comm = commutative r.*-comm - } - where - module r = IsCommutativeRing r - ------------------------------------------------------------------------ -- Bundles @@ -290,7 +282,3 @@ ring : Ring a ℓ → Ring a ℓ ring r = record { isRing = isRing r.isRing } where module r = Ring r -commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ -commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing } - where module r = CommutativeRing r - From a0d11072cdf818fa650a53f51132c4829b2dff77 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 10 Jan 2023 21:15:38 +0000 Subject: [PATCH 18/20] Going back to before the spurious commits form #1902 entered this branch/PR Revert "`CHANGELOG`" This reverts commit e54f2a70d475ada3a946b439c1ddc92af3da2a72. --- CHANGELOG.md | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 50b786364b..53a1acc6f8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -605,8 +605,6 @@ Non-backwards compatible changes * New modules: ``` - Algebra.Construct.Initial - Algebra.Construct.Terminal Data.List.Effectful.Transformer Data.List.NonEmpty.Effectful.Transformer Data.Maybe.Effectful.Transformer @@ -872,14 +870,6 @@ Deprecated modules Deprecated names ---------------- -* In `Algebra.Construct.Zero`: - ```agda - rawMagma ↦ Algebra.Construct.Terminal.rawMagma - magma ↦ Algebra.Construct.Terminal.magma - semigroup ↦ Algebra.Construct.Terminal.semigroup - band ↦ Algebra.Construct.Terminal.band - ``` - * In `Codata.Guarded.Stream.Properties`: ```agda map-identity ↦ map-id From 08cdea683ebbca4e9f4f1119f405fbd038be659a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 10 Jan 2023 21:22:01 +0000 Subject: [PATCH 19/20] restored `Algebra.Construct.Zero` --- src/Algebra/Construct/Zero.agda | 75 ++++++++++++++------------------- 1 file changed, 31 insertions(+), 44 deletions(-) diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda index dccfd9d0c6..a608d2d686 100644 --- a/src/Algebra/Construct/Zero.agda +++ b/src/Algebra/Construct/Zero.agda @@ -2,15 +2,13 @@ -- The Agda standard library -- -- Instances of algebraic structures where the carrier is ⊤. --- In mathematics, this is usually called 0 (1 in the case of Group). +-- In mathematics, this is usually called 0. -- -- From monoids up, these are are zero-objects – i.e, both the initial -- and the terminal object in the relevant category. --- --- For structures without an identity element, the terminal algebra is --- *not* initial, because there is an instance of such a structure --- with an empty Carrier. Accordingly, such definitions are now deprecated --- in favour of those defined in `Algebra.Construct.Terminal`. +-- For structures without an identity element, we can't necessarily +-- produce a homomorphism out of 0, because there is an instance of such +-- a structure with an empty Carrier. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -19,51 +17,40 @@ open import Level using (Level) module Algebra.Construct.Zero {c ℓ : Level} where -open import Algebra.Bundles.Raw - using (RawMagma) open import Algebra.Bundles - using (Magma; Semigroup; Band) - ------------------------------------------------------------------------- --- Re-export those algebras which are both initial and terminal - -open import Algebra.Construct.Terminal public - hiding (rawMagma; magma; semigroup; band) - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new definitions re-exported from --- `Algebra.Construct.Terminal` as continuing support for the below is --- not guaranteed. - --- Version 2.0 rawMagma : RawMagma c ℓ -rawMagma = Algebra.Construct.Terminal.rawMagma +rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } -{-# WARNING_ON_USAGE rawMagma -"Warning: rawMagma was deprecated in v2.0. -Please use Algebra.Construct.Terminal.rawMagma instead." -#-} +rawMonoid : RawMonoid c ℓ +rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +rawGroup : RawGroup c ℓ +rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } magma : Magma c ℓ -magma = Algebra.Construct.Terminal.magma -{-# WARNING_ON_USAGE magma -"Warning: magma was deprecated in v2.0. -Please use Algebra.Construct.Terminal.magma instead." -#-} +magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } semigroup : Semigroup c ℓ -semigroup = Algebra.Construct.Terminal.semigroup -{-# WARNING_ON_USAGE semigroup -"Warning: semigroup was deprecated in v2.0. -Please use Algebra.Construct.Terminal.semigroup instead." -#-} +semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } band : Band c ℓ -band = Algebra.Construct.Terminal.band -{-# WARNING_ON_USAGE semigroup -"Warning: semigroup was deprecated in v2.0. -Please use Algebra.Construct.Terminal.semigroup instead." -#-} +band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +commutativeSemigroup : CommutativeSemigroup c ℓ +commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +monoid : Monoid c ℓ +monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +commutativeMonoid : CommutativeMonoid c ℓ +commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ +idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +group : Group c ℓ +group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +abelianGroup : AbelianGroup c ℓ +abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } From 64fb4037cd9a6c902abf4f7825be1efc1e22235c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 10 Jan 2023 21:23:36 +0000 Subject: [PATCH 20/20] re-added `Ring` bundle... now begin again with the review changes --- CHANGELOG.md | 3 +-- src/Algebra/Construct/Flip/Op.agda | 1 - 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 53a1acc6f8..5dee17fe99 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1587,12 +1587,11 @@ Other minor changes moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` -* Added new functions and proofs to `Algebra.Construct.Flip.Op`: +* Added new proofs to `Algebra.Construct.Flip.Op`: ```agda zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# - ring : Ring a ℓ → Ring a ℓ ``` * Added new definition to `Algebra.Definitions`: diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index 1075a1e942..87c03301ab 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -281,4 +281,3 @@ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } ring : Ring a ℓ → Ring a ℓ ring r = record { isRing = isRing r.isRing } where module r = Ring r -