From 0148ad8f8a5a1cea964ae916eed34a5253b442e2 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Fri, 14 May 2021 16:25:37 +0530 Subject: [PATCH 01/22] add IsUnitalMagma to Structures.agda --- src/Algebra/Structures.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index e5e2f3313c..d2d6fa005e 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -567,3 +567,8 @@ record IsBooleanAlgebra ¬-cong : Congruent₁ ¬ open IsDistributiveLattice isDistributiveLattice public + +record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where + field + isMagma : IsMagma ∙ + identity : Identity ε ∙ From fbec7f3d5c35ff9a4592e0adff117a112ac1ab15 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Fri, 14 May 2021 21:16:50 +0530 Subject: [PATCH 02/22] fix white spaces --- src/Algebra/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index d2d6fa005e..dabfb9baf0 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -571,4 +571,4 @@ record IsBooleanAlgebra record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isMagma : IsMagma ∙ - identity : Identity ε ∙ + identity : Identity ε ∙ From 10a4cb7fc898d0d776df881ceb6002d7698befd1 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sat, 15 May 2021 12:09:01 +0530 Subject: [PATCH 03/22] update UnitalMagma in Structures.agda --- src/Algebra/Structures.agda | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index dabfb9baf0..522a023316 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -572,3 +572,11 @@ record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isMagma : IsMagma ∙ identity : Identity ε ∙ + + open IsMagma isMagma public + + identityˡ : LeftIdentity ε ∙ + identityˡ = proj₁ identity + + identityʳ : RightIdentity ε ∙ + identityʳ = proj₂ identity From 4fb7332431152f16fa09beb423c7900a7c772ffc Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sat, 15 May 2021 12:27:49 +0530 Subject: [PATCH 04/22] add IsSemiGroupoid and IsSmallCategory --- src/Algebra/Structures.agda | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 522a023316..e75aff2987 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -580,3 +580,18 @@ record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where identityʳ : RightIdentity ε ∙ identityʳ = proj₂ identity + +record IsSemiGroupoid (∙ : Op₂ A) : Set (a ⊔ ℓ) where + field + assoc : Associative ∙ + +record IsSmallCategory (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where + field + isSemiGroupoid : IsSemiGroupoid ∙ + identity : Identity ε ∙ + + identityˡ : LeftIdentity ε ∙ + identityˡ = proj₁ identity + + identityʳ : RightIdentity ε ∙ + identityʳ = proj₂ identity From 0d6d1d5e2dc6fa7bfa1adbd50b0706e04ea9be44 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sat, 15 May 2021 12:42:56 +0530 Subject: [PATCH 05/22] fix whitespace --- src/Algebra/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index e75aff2987..78e4e233f5 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -583,7 +583,7 @@ record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where record IsSemiGroupoid (∙ : Op₂ A) : Set (a ⊔ ℓ) where field - assoc : Associative ∙ + assoc : Associative ∙ record IsSmallCategory (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field From 3f179395875a91759af960c1fdbccb92ebc9b619 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sat, 15 May 2021 21:24:58 +0530 Subject: [PATCH 06/22] remove redundant definitions --- src/Algebra/Structures.agda | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 78e4e233f5..522a023316 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -580,18 +580,3 @@ record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where identityʳ : RightIdentity ε ∙ identityʳ = proj₂ identity - -record IsSemiGroupoid (∙ : Op₂ A) : Set (a ⊔ ℓ) where - field - assoc : Associative ∙ - -record IsSmallCategory (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where - field - isSemiGroupoid : IsSemiGroupoid ∙ - identity : Identity ε ∙ - - identityˡ : LeftIdentity ε ∙ - identityˡ = proj₁ identity - - identityʳ : RightIdentity ε ∙ - identityʳ = proj₂ identity From 43968abbc68455b8633639c434823069c3f130c1 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sun, 16 May 2021 11:54:54 +0530 Subject: [PATCH 07/22] define IsQuasigroup in Structures.agda --- src/Algebra/Structures.agda | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 522a023316..49b86609f8 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -580,3 +580,16 @@ record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where identityʳ : RightIdentity ε ∙ identityʳ = proj₂ identity + +record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where + field + isMagma : IsMagma _∙_ + inverse : Inverse ε _⁻¹ _∙_ + + open IsMagma isMagma public + + inverseˡ : LeftInverse ε _⁻¹ _∙_ + inverseˡ = proj₁ inverse + + inverseʳ : RightInverse ε _⁻¹ _∙_ + inverseʳ = proj₂ inverse \ No newline at end of file From 079532dea491a6670fbef971b8a6963752852d67 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sun, 16 May 2021 19:40:08 +0530 Subject: [PATCH 08/22] fix whitespace --- src/Algebra/Morphism/UnitalMagmaMonomorphism.agda | 0 src/Algebra/Structures.agda | 5 +++-- 2 files changed, 3 insertions(+), 2 deletions(-) create mode 100644 src/Algebra/Morphism/UnitalMagmaMonomorphism.agda diff --git a/src/Algebra/Morphism/UnitalMagmaMonomorphism.agda b/src/Algebra/Morphism/UnitalMagmaMonomorphism.agda new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 49b86609f8..d8692ab62a 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -567,7 +567,7 @@ record IsBooleanAlgebra ¬-cong : Congruent₁ ¬ open IsDistributiveLattice isDistributiveLattice public - + record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isMagma : IsMagma ∙ @@ -592,4 +592,5 @@ record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ inverseˡ = proj₁ inverse inverseʳ : RightInverse ε _⁻¹ _∙_ - inverseʳ = proj₂ inverse \ No newline at end of file + inverseʳ = proj₂ inverse + From 86d062fb07d4ee75719e7aab8c8a25131a5b2759 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Sun, 16 May 2021 19:41:38 +0530 Subject: [PATCH 09/22] Delete UnitalMagmaMonomorphism.agda --- src/Algebra/Morphism/UnitalMagmaMonomorphism.agda | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 src/Algebra/Morphism/UnitalMagmaMonomorphism.agda diff --git a/src/Algebra/Morphism/UnitalMagmaMonomorphism.agda b/src/Algebra/Morphism/UnitalMagmaMonomorphism.agda deleted file mode 100644 index e69de29bb2..0000000000 From 67a8ec4b40b7591344a91e566689b846bec70878 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 17 May 2021 11:33:58 +0530 Subject: [PATCH 10/22] Bundeled version of UnitalMagma --- src/Algebra/Bundles.agda | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 627a939019..9a8eb915d1 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -86,7 +86,6 @@ record CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where open Magma magma public using (rawMagma) - record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ @@ -168,6 +167,25 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where -- A raw monoid is a monoid without any laws. +record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε + + open IsUnitalMagma isUnitalMagma public + + magma : Magma c ℓ + magma = record { isMagma = isMagma } + + open Magma magma public + using (_≉_; rawMagma) + + record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ From ba20230fc4ca5f198a11fa80a3c6759492da3523 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 17 May 2021 11:56:00 +0530 Subject: [PATCH 11/22] add structure in correct place --- src/Algebra/Structures.agda | 51 ++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index d8692ab62a..a361412c5b 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -106,6 +106,18 @@ record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where ------------------------------------------------------------------------ -- Structures with 1 binary operation & 1 element ------------------------------------------------------------------------ +record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where + field + isMagma : IsMagma ∙ + identity : Identity ε ∙ + + open IsMagma isMagma public + + identityˡ : LeftIdentity ε ∙ + identityˡ = proj₁ identity + + identityʳ : RightIdentity ε ∙ + identityʳ = proj₂ identity record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field @@ -162,6 +174,19 @@ module IsBoundedLattice {∙ : Op₂ A} ------------------------------------------------------------------------ -- Structures with 1 binary operation, 1 unary operation & 1 element ------------------------------------------------------------------------ +record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where + field + isMagma : IsMagma _∙_ + inverse : Inverse ε _⁻¹ _∙_ + + open IsMagma isMagma public + + inverseˡ : LeftInverse ε _⁻¹ _∙_ + inverseˡ = proj₁ inverse + + inverseʳ : RightInverse ε _⁻¹ _∙_ + inverseʳ = proj₂ inverse + record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field @@ -568,29 +593,3 @@ record IsBooleanAlgebra open IsDistributiveLattice isDistributiveLattice public -record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where - field - isMagma : IsMagma ∙ - identity : Identity ε ∙ - - open IsMagma isMagma public - - identityˡ : LeftIdentity ε ∙ - identityˡ = proj₁ identity - - identityʳ : RightIdentity ε ∙ - identityʳ = proj₂ identity - -record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where - field - isMagma : IsMagma _∙_ - inverse : Inverse ε _⁻¹ _∙_ - - open IsMagma isMagma public - - inverseˡ : LeftInverse ε _⁻¹ _∙_ - inverseˡ = proj₁ inverse - - inverseʳ : RightInverse ε _⁻¹ _∙_ - inverseʳ = proj₂ inverse - From 2284f8c7bcf0eb4878872d8772bcaf8cba8013b7 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 17 May 2021 16:00:55 +0530 Subject: [PATCH 12/22] Bundled version of Quasigroup --- src/Algebra/Bundles.agda | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 9a8eb915d1..2eed1a5df5 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -309,6 +309,25 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where open RawMonoid rawMonoid public using (_≉_; rawMagma) +record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 _⁻¹ + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + _⁻¹ : Op₁ Carrier + isQuasigroup : IsQuasigroup _≈_ _∙_ ε _⁻¹ + + open IsQuasigroup isQuasigroup public + + magma : Magma _ _ + magma = record { isMagma = isMagma } + + open Magma magma public + using (_≉_; rawMagma) record Group c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ From 26c7847edf3c5832afcab4e29707d6da0609e2da Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 17 May 2021 16:06:10 +0530 Subject: [PATCH 13/22] Define Loop --- src/Algebra/Structures.agda | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index a361412c5b..1f1d83aa42 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -187,6 +187,19 @@ record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ inverseʳ : RightInverse ε _⁻¹ _∙_ inverseʳ = proj₂ inverse +record IsLoop (∙ : Op₂ A) + (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where + field + isQuasigroup : IsQuasigroup ∙ ε ⁻¹ + identity : Identity ε ∙ + + open IsQuasigroup isQuasigroup public + + identityˡ : LeftIdentity ε ∙ + identityˡ = proj₁ identity + + identityʳ : RightIdentity ε ∙ + identityʳ = proj₂ identity record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field From 99aab798acfabcb237c406a617ffc24acdcbeea4 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 17 May 2021 19:34:48 +0530 Subject: [PATCH 14/22] fix comment --- src/Algebra/Bundles.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 2eed1a5df5..25a1f1966b 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -165,8 +165,6 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where -- Bundles with 1 binary operation & 1 element ------------------------------------------------------------------------ --- A raw monoid is a monoid without any laws. - record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ @@ -185,6 +183,7 @@ record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where open Magma magma public using (_≉_; rawMagma) +-- A raw monoid is a monoid without any laws. record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ From ccccf53ac47fa81072cb26ff14427d29832374b2 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Tue, 18 May 2021 13:17:29 +0530 Subject: [PATCH 15/22] remove IsLoop --- src/Algebra/Structures.agda | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1f1d83aa42..edecb1ea17 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -187,20 +187,6 @@ record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ inverseʳ : RightInverse ε _⁻¹ _∙_ inverseʳ = proj₂ inverse -record IsLoop (∙ : Op₂ A) - (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where - field - isQuasigroup : IsQuasigroup ∙ ε ⁻¹ - identity : Identity ε ∙ - - open IsQuasigroup isQuasigroup public - - identityˡ : LeftIdentity ε ∙ - identityˡ = proj₁ identity - - identityʳ : RightIdentity ε ∙ - identityʳ = proj₂ identity - record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field isMonoid : IsMonoid _∙_ ε From e1ab3676b764014a85c4c8d92c4d3ca7387965ab Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Fri, 11 Jun 2021 18:28:23 +0530 Subject: [PATCH 16/22] constructs an instance of IsUnitalMagma in Monoid --- src/Algebra/Bundles.agda | 6 +++++- src/Algebra/Structures.agda | 8 ++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 25a1f1966b..9fbc108e99 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -203,7 +203,6 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where open RawMagma rawMagma public using (_≉_) - record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ @@ -225,6 +224,11 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where rawMonoid : RawMonoid _ _ rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε} + unitalMagma : UnitalMagma _ _ + unitalMagma = record { isUnitalMagma = isUnitalMagma } + + open UnitalMagma unitalMagma public + using (isMagma) record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index edecb1ea17..3a6f3e38ba 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -132,6 +132,14 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where identityʳ : RightIdentity ε ∙ identityʳ = proj₂ identity + isUnitalMagma : IsUnitalMagma ∙ ε + isUnitalMagma = record + { isMagma = isMagma + ; identity = identity + } + + open IsUnitalMagma isUnitalMagma public + using (isMagma) record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field From fb3d757f552945e1dff069cbe2ea3de939c34250 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 14 Jun 2021 12:29:36 +0530 Subject: [PATCH 17/22] renaming in larger structures --- src/Algebra/Structures.agda | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 3a6f3e38ba..c199218403 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -317,6 +317,7 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where ; identityˡ to +-identityˡ ; identityʳ to +-identityʳ ; isMagma to +-isMagma + ; isUnitalMagma to +-isUnitalMagma ; isSemigroup to +-isSemigroup ) @@ -338,14 +339,10 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where distrib : * DistributesOver + zero : Zero 0# * - open IsCommutativeMonoid +-isCommutativeMonoid public - using () - renaming - ( comm to +-comm - ; isMonoid to +-isMonoid - ; isCommutativeMagma to +-isCommutativeMagma - ; isCommutativeSemigroup to +-isCommutativeSemigroup - ) + open IsCommutativeMonoid +-isCommutativeMonoid public using () + renaming ( comm to +-comm ; isMonoid to +-isMonoid ; + isCommutativeMagma to +-isCommutativeMagma ; + isCommutativeSemigroup to +-isCommutativeSemigroup ) zeroˡ : LeftZero 0# * zeroˡ = proj₁ zero @@ -414,6 +411,7 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A) ; isMagma to +-isMagma ; isSemigroup to +-isSemigroup ; isMonoid to +-isMonoid + ; isUnitalMagma to +-isUnitalMagma ; isCommutativeMagma to +-isCommutativeMagma ; isCommutativeSemigroup to +-isCommutativeSemigroup ) @@ -522,6 +520,7 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where ; isMagma to +-isMagma ; isSemigroup to +-isSemigroup ; isMonoid to +-isMonoid + ; isUnitalMagma to +-isUnitalMagma ; isCommutativeMagma to +-isCommutativeMagma ; isCommutativeMonoid to +-isCommutativeMonoid ; isCommutativeSemigroup to +-isCommutativeSemigroup From 379eb71150311720bcad2920d7fae4cf9328eefb Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 14 Jun 2021 12:47:54 +0530 Subject: [PATCH 18/22] fix-whitespace --- src/Algebra/Bundles.agda | 9 +++++---- src/Algebra/Structures.agda | 11 +++++++---- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 9fbc108e99..33e536e9f9 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -515,10 +515,11 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where open Monoid +-monoid public using (_≉_) renaming - ( rawMagma to +-rawMagma - ; magma to +-magma - ; semigroup to +-semigroup - ; rawMonoid to +-rawMonoid + ( rawMagma to +-rawMagma + ; magma to +-magma + ; semigroup to +-semigroup + ; unitalMagma to +-unitalMagma + ; rawMonoid to +-rawMonoid ) *-semigroup : Semigroup _ _ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index c199218403..7651688144 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -317,7 +317,7 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where ; identityˡ to +-identityˡ ; identityʳ to +-identityʳ ; isMagma to +-isMagma - ; isUnitalMagma to +-isUnitalMagma + ; isUnitalMagma to +-isUnitalMagma ; isSemigroup to +-isSemigroup ) @@ -340,9 +340,12 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where zero : Zero 0# * open IsCommutativeMonoid +-isCommutativeMonoid public using () - renaming ( comm to +-comm ; isMonoid to +-isMonoid ; - isCommutativeMagma to +-isCommutativeMagma ; - isCommutativeSemigroup to +-isCommutativeSemigroup ) + renaming + ( comm to +-comm + ; isMonoid to +-isMonoid + ; isCommutativeMagma to +-isCommutativeMagma + ; isCommutativeSemigroup to +-isCommutativeSemigroup + ) zeroˡ : LeftZero 0# * zeroˡ = proj₁ zero From 2323e91fc4f05ca755c175d6db46d70f75ce164b Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Mon, 14 Jun 2021 13:07:32 +0530 Subject: [PATCH 19/22] indentation --- src/Algebra/Structures.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 7651688144..f163e70d9f 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -341,9 +341,9 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where open IsCommutativeMonoid +-isCommutativeMonoid public using () renaming - ( comm to +-comm - ; isMonoid to +-isMonoid - ; isCommutativeMagma to +-isCommutativeMagma + ( comm to +-comm + ; isMonoid to +-isMonoid + ; isCommutativeMagma to +-isCommutativeMagma ; isCommutativeSemigroup to +-isCommutativeSemigroup ) From 82e8ec33477273b941e32c809856ac5914fb0db5 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Wed, 16 Jun 2021 17:28:28 +0530 Subject: [PATCH 20/22] update changes in CHANGELOG.md --- CHANGELOG.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 126a65bd0a..51f6a5224f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -93,3 +93,13 @@ Other minor additions ```agda m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m ``` +* Added `UnitalMagma` and `QuasiGroup` to the Algebra.Bundles: + ```agda + record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) + record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) + ``` +* Added new records to `Algebra.Structures`: + ```agda + record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) + ``` \ No newline at end of file From 6ff1c3669157051806ddf6ed56a7d9302f248de1 Mon Sep 17 00:00:00 2001 From: "akshobhya.k.m@sap.com" Date: Wed, 16 Jun 2021 19:16:00 +0530 Subject: [PATCH 21/22] Update Structures.agda --- src/Algebra/Structures.agda | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index f163e70d9f..3f306e1172 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -138,9 +138,6 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where ; identity = identity } - open IsUnitalMagma isUnitalMagma public - using (isMagma) - record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isMonoid : IsMonoid ∙ ε From 404ae5c5dbd2b49a585f651a36d34cfe9027da32 Mon Sep 17 00:00:00 2001 From: = Date: Sun, 20 Jun 2021 21:24:01 +0800 Subject: [PATCH 22/22] A few minor tweaks --- CHANGELOG.md | 10 +++-- src/Algebra/Bundles.agda | 87 ++++++++++++++++++++++--------------- src/Algebra/Structures.agda | 35 ++++++++++----- 3 files changed, 82 insertions(+), 50 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 51f6a5224f..508eb6ebf5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -93,13 +93,15 @@ Other minor additions ```agda m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m ``` + * Added `UnitalMagma` and `QuasiGroup` to the Algebra.Bundles: ```agda record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) - record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) + record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) ``` + * Added new records to `Algebra.Structures`: ```agda - record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) - record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) - ``` \ No newline at end of file + record IsUnitalMagma (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) + ``` diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 33e536e9f9..329e273fb4 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -86,6 +86,7 @@ record CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where open Magma magma public using (rawMagma) + record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ @@ -165,24 +166,6 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where -- Bundles with 1 binary operation & 1 element ------------------------------------------------------------------------ -record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where - infixl 7 _∙_ - infix 4 _≈_ - field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _∙_ : Op₂ Carrier - ε : Carrier - isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε - - open IsUnitalMagma isUnitalMagma public - - magma : Magma c ℓ - magma = record { isMagma = isMagma } - - open Magma magma public - using (_≉_; rawMagma) - -- A raw monoid is a monoid without any laws. record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where @@ -203,6 +186,26 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where open RawMagma rawMagma public using (_≉_) + +record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where + infixl 7 _∙_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε + + open IsUnitalMagma isUnitalMagma public + + magma : Magma c ℓ + magma = record { isMagma = isMagma } + + open Magma magma public + using (_≉_; rawMagma) + + record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ @@ -227,8 +230,6 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where unitalMagma : UnitalMagma _ _ unitalMagma = record { isUnitalMagma = isUnitalMagma } - open UnitalMagma unitalMagma public - using (isMagma) record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ @@ -246,7 +247,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where monoid = record { isMonoid = isMonoid } open Monoid monoid public - using (_≉_; rawMagma; magma; semigroup; rawMonoid) + using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup } @@ -272,7 +273,8 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeMonoid commutativeMonoid public using - ( _≉_; rawMagma; magma; commutativeMagma; semigroup; commutativeSemigroup + ( _≉_; rawMagma; magma; unitalMagma; commutativeMagma + ; semigroup; commutativeSemigroup ; rawMonoid; monoid ) @@ -312,6 +314,7 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where open RawMonoid rawMonoid public using (_≉_; rawMagma) + record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -332,6 +335,7 @@ record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where open Magma magma public using (_≉_; rawMagma) + record Group c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -353,7 +357,13 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where monoid = record { isMonoid = isMonoid } open Monoid monoid public - using (_≉_; rawMagma; magma; semigroup; rawMonoid) + using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) + + quasigroup : Quasigroup c ℓ + quasigroup = record + { isQuasigroup = isQuasigroup + } + record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ @@ -372,8 +382,10 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where group : Group _ _ group = record { isGroup = isGroup } - open Group group public - using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup) + open Group group public using + (_≉_; rawMagma; magma; semigroup + ; rawMonoid; monoid; rawGroup; quasigroup + ) commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } @@ -551,7 +563,7 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open NearSemiring nearSemiring public using - ( _≉_; +-rawMagma; +-magma; +-semigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup ; +-rawMonoid; +-monoid ; *-rawMagma; *-magma; *-semigroup ; rawNearSemiring @@ -589,7 +601,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where open SemiringWithoutOne semiringWithoutOne public using - ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; nearSemiring; rawNearSemiring @@ -667,6 +679,7 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where using (_≉_) renaming ( rawMagma to +-rawMagma ; magma to +-magma + ; unitalMagma to +-unitalMagma ; commutativeMagma to +-commutativeMagma ; semigroup to +-semigroup ; commutativeSemigroup to +-commutativeSemigroup @@ -710,7 +723,8 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero public using - ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid @@ -745,7 +759,8 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where open Semiring semiring public using - ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid @@ -793,7 +808,8 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeSemiring commutativeSemiring public using - ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid; *-commutativeMonoid @@ -849,6 +865,7 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where ; _⁻¹ = -_ } + record Ring c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ @@ -874,7 +891,8 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where open Semiring semiring public using - ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid ; +-commutativeMonoid ; *-rawMonoid; *-monoid @@ -883,7 +901,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where ) open AbelianGroup +-abelianGroup public - using () renaming (group to +-group) + using () renaming (group to +-group; quasigroup to +-quasigroup) rawRing : RawRing _ _ rawRing = record @@ -916,7 +934,7 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where ring : Ring _ _ ring = record { isRing = isRing } - open Ring ring public using (_≉_; rawRing; +-group; +-abelianGroup) + open Ring ring public using (_≉_; rawRing; +-quasigroup; +-group; +-abelianGroup) commutativeSemiring : CommutativeSemiring _ _ commutativeSemiring = @@ -924,7 +942,8 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where open CommutativeSemiring commutativeSemiring public using - ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup + ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma + ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid; *-commutativeMonoid diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 3f306e1172..62243f9c7d 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -106,9 +106,10 @@ record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where ------------------------------------------------------------------------ -- Structures with 1 binary operation & 1 element ------------------------------------------------------------------------ + record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field - isMagma : IsMagma ∙ + isMagma : IsMagma ∙ identity : Identity ε ∙ open IsMagma isMagma public @@ -119,6 +120,7 @@ record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where identityʳ : RightIdentity ε ∙ identityʳ = proj₂ identity + record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isSemigroup : IsSemigroup ∙ @@ -134,10 +136,11 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where isUnitalMagma : IsUnitalMagma ∙ ε isUnitalMagma = record - { isMagma = isMagma + { isMagma = isMagma ; identity = identity } + record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where field isMonoid : IsMonoid ∙ ε @@ -179,6 +182,7 @@ module IsBoundedLattice {∙ : Op₂ A} ------------------------------------------------------------------------ -- Structures with 1 binary operation, 1 unary operation & 1 element ------------------------------------------------------------------------ + record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field isMagma : IsMagma _∙_ @@ -192,6 +196,7 @@ record IsQuasigroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ inverseʳ : RightInverse ε _⁻¹ _∙_ inverseʳ = proj₂ inverse + record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where field isMonoid : IsMonoid _∙_ ε @@ -218,6 +223,12 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique setoid ∙-cong assoc identity inverseˡ + isQuasigroup : IsQuasigroup _∙_ ε _⁻¹ + isQuasigroup = record + { isMagma = isMagma + ; inverse = inverse + } + record IsAbelianGroup (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where @@ -306,16 +317,16 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where open IsMonoid +-isMonoid public renaming - ( assoc to +-assoc - ; ∙-cong to +-cong - ; ∙-congˡ to +-congˡ - ; ∙-congʳ to +-congʳ - ; identity to +-identity - ; identityˡ to +-identityˡ - ; identityʳ to +-identityʳ - ; isMagma to +-isMagma + ( assoc to +-assoc + ; ∙-cong to +-cong + ; ∙-congˡ to +-congˡ + ; ∙-congʳ to +-congʳ + ; identity to +-identity + ; identityˡ to +-identityˡ + ; identityʳ to +-identityʳ + ; isMagma to +-isMagma ; isUnitalMagma to +-isUnitalMagma - ; isSemigroup to +-isSemigroup + ; isSemigroup to +-isSemigroup ) open IsSemigroup *-isSemigroup public @@ -524,6 +535,7 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where ; isCommutativeMagma to +-isCommutativeMagma ; isCommutativeMonoid to +-isCommutativeMonoid ; isCommutativeSemigroup to +-isCommutativeSemigroup + ; isQuasigroup to +-isQuasigroup ; isGroup to +-isGroup ) @@ -598,4 +610,3 @@ record IsBooleanAlgebra ¬-cong : Congruent₁ ¬ open IsDistributiveLattice isDistributiveLattice public -