From 69d0dffb1dca9c5c57d49186e786a860647159d2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 7 Jan 2023 18:33:15 +0000 Subject: [PATCH 01/14] 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 02/14] 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 03/14] 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 04/14] 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 05/14] `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 06/14] 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 07/14] 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 08/14] 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 09/14] =?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 5fbceb2151c566f7ad5f52ff7cda43f9c3f22543 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 17:24:07 +0000 Subject: [PATCH 10/14] fixed `Algebra.Module.Construct.Zero` --- src/Algebra/Module/Construct/Zero.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index b6a1b2d637..cd628f046e 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -30,9 +30,9 @@ private module ℤero where infix 4 _≈_ Carrier : Set c - _≈_ : Rel Carrier ℓ - Carrier = ⊤ + + _≈_ : Rel Carrier ℓ _ ≈ _ = ⊤ open ℤero From 579e6df09e1a8576dfb178e870db5cb9087f21c3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 9 Jan 2023 17:26:17 +0000 Subject: [PATCH 11/14] fix whitespace --- src/Algebra/Construct/Terminal.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda index b932710c57..cf5f770812 100644 --- a/src/Algebra/Construct/Terminal.agda +++ b/src/Algebra/Construct/Terminal.agda @@ -26,7 +26,7 @@ private module 𝕆ne where infix 4 _≈_ Carrier : Set c Carrier = ⊤ - + _≈_ : Rel Carrier ℓ _ ≈ _ = ⊤ From 88ca2432a90dbc09b2630a8a240c503e0069c81d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 23 Feb 2023 14:18:38 +0000 Subject: [PATCH 12/14] Capitalise comments --- src/Algebra/Construct/Initial.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda index 14b1b32fef..ff52f0a7a7 100644 --- a/src/Algebra/Construct/Initial.agda +++ b/src/Algebra/Construct/Initial.agda @@ -26,13 +26,13 @@ open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEqui ------------------------------------------------------------------------ --- re-export those algebras which are also terminal +-- 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 +-- Gather all the functionality in one place private module ℤero where From d8117f7569c56e4e88e7b7232252813572a93e1e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 23 Feb 2023 14:52:38 +0000 Subject: [PATCH 13/14] I think I have understood record/module infernce a bit better now --- src/Algebra/Construct/Initial.agda | 6 ++--- src/Algebra/Construct/Terminal.agda | 36 ++++++++++++++--------------- 2 files changed, 20 insertions(+), 22 deletions(-) diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda index ff52f0a7a7..7851eb1b62 100644 --- a/src/Algebra/Construct/Initial.agda +++ b/src/Algebra/Construct/Initial.agda @@ -34,7 +34,7 @@ open import Algebra.Construct.Terminal {c} {ℓ} public ------------------------------------------------------------------------ -- Gather all the functionality in one place -private module ℤero where +module ℤero where infixl 7 _∙_ infix 4 _≈_ @@ -66,13 +66,13 @@ open ℤero -- Raw bundles rawMagma : RawMagma c ℓ -rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ } +rawMagma = record { ℤero } ------------------------------------------------------------------------ -- Structures isEquivalence : IsEquivalence _≈_ -isEquivalence = record { refl = refl ; sym = sym ; trans = trans } +isEquivalence = record { ℤero } isMagma : IsMagma _≈_ _∙_ isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong } diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda index cf5f770812..f914a010b5 100644 --- a/src/Algebra/Construct/Terminal.agda +++ b/src/Algebra/Construct/Terminal.agda @@ -21,7 +21,7 @@ open import Relation.Binary.Core using (Rel) ------------------------------------------------------------------------ -- Gather all the functionality in one place -private module 𝕆ne where +module 𝕆ne where infix 4 _≈_ Carrier : Set c @@ -30,59 +30,57 @@ private module 𝕆ne where _≈_ : Rel Carrier ℓ _ ≈ _ = ⊤ -open 𝕆ne - ------------------------------------------------------------------------ -- Raw bundles rawMagma : RawMagma c ℓ -rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ } +rawMagma = record { 𝕆ne } rawMonoid : RawMonoid c ℓ -rawMonoid = record { Carrier = Carrier ; _≈_ = _≈_ } +rawMonoid = record { 𝕆ne } rawGroup : RawGroup c ℓ -rawGroup = record { Carrier = Carrier ; _≈_ = _≈_ } +rawGroup = record { 𝕆ne } rawSemiring : RawSemiring c ℓ -rawSemiring = record { Carrier = Carrier ; _≈_ = _≈_ } +rawSemiring = record { 𝕆ne } rawRing : RawRing c ℓ -rawRing = record { Carrier = Carrier ; _≈_ = _≈_ } +rawRing = record { 𝕆ne } ------------------------------------------------------------------------ -- Bundles magma : Magma c ℓ -magma = record { Carrier = Carrier ; _≈_ = _≈_ } +magma = record { 𝕆ne } semigroup : Semigroup c ℓ -semigroup = record { Carrier = Carrier ; _≈_ = _≈_ } +semigroup = record { 𝕆ne } band : Band c ℓ -band = record { Carrier = Carrier ; _≈_ = _≈_ } +band = record { 𝕆ne } commutativeSemigroup : CommutativeSemigroup c ℓ -commutativeSemigroup = record { Carrier = Carrier ; _≈_ = _≈_ } +commutativeSemigroup = record { 𝕆ne } monoid : Monoid c ℓ -monoid = record { Carrier = Carrier ; _≈_ = _≈_ } +monoid = record { 𝕆ne } commutativeMonoid : CommutativeMonoid c ℓ -commutativeMonoid = record { Carrier = Carrier ; _≈_ = _≈_ } +commutativeMonoid = record { 𝕆ne } idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ -idempotentCommutativeMonoid = record { Carrier = Carrier ; _≈_ = _≈_ } +idempotentCommutativeMonoid = record { 𝕆ne } group : Group c ℓ -group = record { Carrier = Carrier ; _≈_ = _≈_ } +group = record { 𝕆ne } abelianGroup : AbelianGroup c ℓ -abelianGroup = record { Carrier = Carrier ; _≈_ = _≈_ } +abelianGroup = record { 𝕆ne } semiring : Semiring c ℓ -semiring = record { Carrier = Carrier ; _≈_ = _≈_ } +semiring = record { 𝕆ne } ring : Ring c ℓ -ring = record { Carrier = Carrier ; _≈_ = _≈_ } +ring = record { 𝕆ne } From 19181c0863cb9bbea223ded1c012e40d673540c0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 23 Feb 2023 15:15:21 +0000 Subject: [PATCH 14/14] forgot `Algebra.Module.Construct.Zero` --- src/Algebra/Module/Construct/Zero.agda | 30 +++++++++++++------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda index cd628f046e..ae5e3e7df3 100644 --- a/src/Algebra/Module/Construct/Zero.agda +++ b/src/Algebra/Module/Construct/Zero.agda @@ -26,14 +26,14 @@ private ------------------------------------------------------------------------ -- gather all the functionality in one place -private module ℤero where +module ℤero where - infix 4 _≈_ - Carrier : Set c - Carrier = ⊤ + infix 4 _≈ᴹ_ + Carrierᴹ : Set c + Carrierᴹ = ⊤ - _≈_ : Rel Carrier ℓ - _ ≈ _ = ⊤ + _≈ᴹ_ : Rel Carrierᴹ ℓ + _ ≈ᴹ _ = ⊤ open ℤero @@ -41,32 +41,32 @@ open ℤero -- Raw bundles NOT YET IMPLEMENTED issue #1828 {- rawModule : RawModule c ℓ -rawModule = record { Carrier = Carrier ; _≈_ = _≈_ } +rawModule = record { ℤero } -} ------------------------------------------------------------------------ -- Bundles leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ -leftSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +leftSemimodule = record { ℤero } rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S c ℓ -rightSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +rightSemimodule = record { ℤero } bisemimodule : {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S c ℓ -bisemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +bisemimodule = record { ℤero } semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R c ℓ -semimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +semimodule = record { ℤero } leftModule : {R : Ring r ℓr} → LeftModule R c ℓ -leftModule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +leftModule = record { ℤero } rightModule : {S : Ring s ℓs} → RightModule S c ℓ -rightModule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +rightModule = record { ℤero } bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S c ℓ -bimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +bimodule = record { ℤero } ⟨module⟩ : {R : CommutativeRing r ℓr} → Module R c ℓ -⟨module⟩ = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ } +⟨module⟩ = record { ℤero }