From 876c287ca46a1036b5c7f9483e3023ea8763bf49 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 24 Jun 2024 15:45:01 +0200 Subject: [PATCH 01/10] Add some type relations/isomorphisms --- .../Function/Dependent/Propositional.agda | 7 ++- src/Function/Related/TypeIsomorphisms.agda | 46 +++++++++++++++---- 2 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index cb8a8d99a1..c4eb338087 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -17,7 +17,7 @@ open import Function.Related.Propositional implication; reverseImplication; equivalence; injection; reverseInjection; leftInverse; surjection; bijection) open import Function.Base using (_$_; _∘_; _∘′_) -open import Function.Properties.Inverse using (↔⇒↠; ↔⇒⟶; ↔⇒⟵; ↔-sym; ↔⇒↩) +open import Function.Properties.Inverse using (↔⇒↠; ↔⇒⟶; ↔⇒⟵; ↔-sym; ↔⇒↩; refl) open import Function.Properties.RightInverse using (↩⇒↪; ↪⇒↩) open import Function.Properties.Inverse.HalfAdjointEquivalence using (↔⇒≃; _≃_; ≃⇒↔) @@ -316,3 +316,8 @@ cong {B = B} {k = reverseInjection} I↔J A↢B = Σ-↣ (↔-sym I↔J) (swap cong {B = B} {k = leftInverse} I↔J A↩B = ↩⇒↪ (Σ-↩ (↔⇒↩ (↔-sym I↔J)) (↪⇒↩ (swap-coercions {k = leftInverse} B I↔J A↩B))) cong {k = surjection} I↔J A↠B = Σ-↠ (↔⇒↠ I↔J) A↠B cong {k = bijection} I↔J A↔B = Σ-↔ I↔J A↔B + +cong′ : ∀ {k} → {A : Set a} {B₁ : A → Set b} {B₂ : A → Set c} → + (∀ {x} → B₁ x ∼[ k ] B₂ x) → + Σ A B₁ ∼[ k ] Σ A B₂ +cong′ = cong (refl _) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 3386032654..a1f26b0cca 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -15,7 +15,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Bool.Base using (true; false) open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Product.Base as Product - using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃) + using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃; ∃-syntax) open import Data.Product.Function.NonDependent.Propositional open import Data.Sum.Base as Sum open import Data.Sum.Properties using (swap-involutive) @@ -106,24 +106,44 @@ private ⊎-identity ℓ = ⊎-identityˡ ℓ , ⊎-identityʳ ℓ ------------------------------------------------------------------------ --- Properties of × and ⊎ +-- Properties of ∃ and ⊎ --- × distributes over ⊎ +-- ∃ distributes over ⊎ -×-distribˡ-⊎ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_ -×-distribˡ-⊎ ℓ _ _ _ = mk↔ₛ′ +Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} → + (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) +Σ-distribˡ-⊎ = mk↔ₛ′ (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′) [ Product.map₂ inj₁ , Product.map₂ inj₂ ]′ [ (λ _ → refl) , (λ _ → refl) ] (uncurry λ _ → [ (λ _ → refl) , (λ _ → refl) ]) -×-distribʳ-⊎ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_ -×-distribʳ-⊎ ℓ _ _ _ = mk↔ₛ′ - (uncurry [ curry inj₁ , curry inj₂ ]′) - [ Product.map₁ inj₁ , Product.map₁ inj₂ ]′ +Σ-distribʳ-⊎ : {P : Set a} {Q : Set b} {R : P ⊎ Q → Set c} → + (Σ (P ⊎ Q) R) ↔ (Σ P (R ∘ inj₁) ⊎ Σ Q (R ∘ inj₂)) +Σ-distribʳ-⊎ = mk↔ₛ′ + (uncurry [ curry inj₁ , curry inj₂ ]) + [ Product.dmap inj₁ id , Product.dmap inj₂ id ] [ (λ _ → refl) , (λ _ → refl) ] (uncurry [ (λ _ _ → refl) , (λ _ _ → refl) ]) +------------------------------------------------------------------------ +-- Properties of × and ⊎ + +-- × distributes over ⊎ +-- primed variants are more level polymorphic + +×-distribˡ-⊎′ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) +×-distribˡ-⊎′ = Σ-distribˡ-⊎ + +×-distribˡ-⊎ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_ +×-distribˡ-⊎ ℓ _ _ _ = ×-distribˡ-⊎′ + +×-distribʳ-⊎′ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) +×-distribʳ-⊎′ = Σ-distribʳ-⊎ + +×-distribʳ-⊎ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_ +×-distribʳ-⊎ ℓ _ _ _ = ×-distribʳ-⊎′ + ×-distrib-⊎ : ∀ ℓ → _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_ ×-distrib-⊎ ℓ = ×-distribˡ-⊎ ℓ , ×-distribʳ-⊎ ℓ @@ -332,3 +352,11 @@ True↔ ( true because [p]) irr = mk↔ₛ′ (λ _ → invert [p]) (λ _ → _) (irr _) (λ _ → refl) True↔ (false because ofⁿ ¬p) _ = mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (λ x → flip contradiction ¬p x) (λ ()) + +------------------------------------------------------------------------ +-- Relating a predicate to an existentially quantified one with the +-- restriction that the quantified variable is equal to the given one + +∃-≡ : ∀ {A : Set a} (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) +∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , (refl , Py)) → Py) + (λ where (_ , refl , _) → refl) (λ where _ → refl) From e468b94cc10e77fe2f21cab281ba0ef35d598324 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Tue, 25 Jun 2024 16:57:41 +0200 Subject: [PATCH 02/10] Remove some explicitly bound variables in type signatures --- src/Data/Product/Function/Dependent/Propositional.agda | 4 +--- src/Function/Related/TypeIsomorphisms.agda | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index c4eb338087..4a9359bcd0 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -317,7 +317,5 @@ cong {B = B} {k = leftInverse} I↔J A↩B = ↩⇒↪ (Σ-↩ (↔⇒↩ cong {k = surjection} I↔J A↠B = Σ-↠ (↔⇒↠ I↔J) A↠B cong {k = bijection} I↔J A↔B = Σ-↔ I↔J A↔B -cong′ : ∀ {k} → {A : Set a} {B₁ : A → Set b} {B₂ : A → Set c} → - (∀ {x} → B₁ x ∼[ k ] B₂ x) → - Σ A B₁ ∼[ k ] Σ A B₂ +cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B cong′ = cong (refl _) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index a1f26b0cca..fe1fea3470 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -357,6 +357,6 @@ True↔ (false because ofⁿ ¬p) _ = -- Relating a predicate to an existentially quantified one with the -- restriction that the quantified variable is equal to the given one -∃-≡ : ∀ {A : Set a} (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) +∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) ∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , (refl , Py)) → Py) (λ where (_ , refl , _) → refl) (λ where _ → refl) From e6f51de7f64e114a4b46e361fdba89575b41a8e0 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Fri, 30 Aug 2024 12:50:27 +0200 Subject: [PATCH 03/10] Add new functions to CHANGELOG --- CHANGELOG.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 57222329ef..8852110e2b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,6 +48,11 @@ New modules Additions to existing modules ----------------------------- +* In `Data.Product.Function.Dependent.Propositional`: + ```agda + cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B + ``` + * In `Data.List.Properties`: ```agda product≢0 : All NonZero ns → NonZero (product ns) @@ -93,6 +98,15 @@ Additions to existing modules _≡?_ : DecidableEquality (Vec A n) ``` +* In `Function.Related.TypeIsomorphisms`: + ```agda + Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} → (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) + Σ-distribʳ-⊎ : {P : Set a} {Q : Set b} {R : P ⊎ Q → Set c} → (Σ (P ⊎ Q) R) ↔ (Σ P (R ∘ inj₁) ⊎ Σ Q (R ∘ inj₂)) + ×-distribˡ-⊎′ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) + ×-distribʳ-⊎′ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) + ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) + ``` + * In `Relation.Nullary.Decidable`: ```agda does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b? From 8391682ddeb8e7f104c13ebd5604ce1535057edf Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Mon, 30 Sep 2024 18:23:21 +0100 Subject: [PATCH 04/10] Update src/Data/Product/Function/Dependent/Propositional.agda Name change --- src/Data/Product/Function/Dependent/Propositional.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 4a9359bcd0..4c6f391e2f 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -317,5 +317,5 @@ cong {B = B} {k = leftInverse} I↔J A↩B = ↩⇒↪ (Σ-↩ (↔⇒↩ cong {k = surjection} I↔J A↠B = Σ-↠ (↔⇒↠ I↔J) A↠B cong {k = bijection} I↔J A↔B = Σ-↔ I↔J A↔B -cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B -cong′ = cong (refl _) +congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B +congˡ = cong (refl _) From 22889c75cb74e605e98e98db35e95164ecbd5f66 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Mon, 30 Sep 2024 18:24:03 +0100 Subject: [PATCH 05/10] Update CHANGELOG.md Name change inherited from source update --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 45e612b514..599dc03646 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -314,7 +314,7 @@ Additions to existing modules * In `Data.Product.Function.Dependent.Propositional`: ```agda - cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B + congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B ``` * New lemma in `Data.Vec.Properties`: From dd1b1dc414589c0647ef8ae416afa2f165abbb3f Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Mon, 30 Sep 2024 18:25:49 +0100 Subject: [PATCH 06/10] Update src/Function/Related/TypeIsomorphisms.agda Remove redundant parentheses --- src/Function/Related/TypeIsomorphisms.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index fe1fea3470..40c408e6ff 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -358,5 +358,5 @@ True↔ (false because ofⁿ ¬p) _ = -- restriction that the quantified variable is equal to the given one ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) -∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , (refl , Py)) → Py) +∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py) (λ where (_ , refl , _) → refl) (λ where _ → refl) From 7850ace897bcc77c21db9a81b03efabf11b8dd4f Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Fri, 6 Dec 2024 15:09:38 +0000 Subject: [PATCH 07/10] Update TypeIsomorphisms.agda @JacquesCarette @jamesmckinna @gallais switched the prime discipline on the distributive laws for products and sums --- src/Function/Related/TypeIsomorphisms.agda | 30 +++++++++++----------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 40c408e6ff..fa29312f7a 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -106,9 +106,9 @@ private ⊎-identity ℓ = ⊎-identityˡ ℓ , ⊎-identityʳ ℓ ------------------------------------------------------------------------ --- Properties of ∃ and ⊎ +-- Properties of Σ and ⊎ --- ∃ distributes over ⊎ +-- Σ distributes over ⊎ Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} → (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) @@ -118,8 +118,8 @@ private [ (λ _ → refl) , (λ _ → refl) ] (uncurry λ _ → [ (λ _ → refl) , (λ _ → refl) ]) -Σ-distribʳ-⊎ : {P : Set a} {Q : Set b} {R : P ⊎ Q → Set c} → - (Σ (P ⊎ Q) R) ↔ (Σ P (R ∘ inj₁) ⊎ Σ Q (R ∘ inj₂)) +Σ-distribʳ-⊎ : {P : A ⊎ B → Set c} → + (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂)) Σ-distribʳ-⊎ = mk↔ₛ′ (uncurry [ curry inj₁ , curry inj₂ ]) [ Product.dmap inj₁ id , Product.dmap inj₂ id ] @@ -130,22 +130,22 @@ private -- Properties of × and ⊎ -- × distributes over ⊎ --- primed variants are more level polymorphic +-- primed variants are less level polymorphic -×-distribˡ-⊎′ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) -×-distribˡ-⊎′ = Σ-distribˡ-⊎ +×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) +×-distribˡ-⊎ = Σ-distribˡ-⊎ -×-distribˡ-⊎ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_ -×-distribˡ-⊎ ℓ _ _ _ = ×-distribˡ-⊎′ +×-distribˡ-⊎′ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_ +×-distribˡ-⊎′ ℓ _ _ _ = ×-distribˡ-⊎ -×-distribʳ-⊎′ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) -×-distribʳ-⊎′ = Σ-distribʳ-⊎ +×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) +×-distribʳ-⊎ = Σ-distribʳ-⊎ -×-distribʳ-⊎ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_ -×-distribʳ-⊎ ℓ _ _ _ = ×-distribʳ-⊎′ +×-distribʳ-⊎′ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_ +×-distribʳ-⊎′ ℓ _ _ _ = ×-distribʳ-⊎ -×-distrib-⊎ : ∀ ℓ → _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_ -×-distrib-⊎ ℓ = ×-distribˡ-⊎ ℓ , ×-distribʳ-⊎ ℓ +×-distrib-⊎′ : ∀ ℓ → _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_ +×-distrib-⊎′ ℓ = ×-distribˡ-⊎′ ℓ , ×-distribʳ-⊎′ ℓ ------------------------------------------------------------------------ -- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring From 7a5ddb90b61cec4948121f36a368b61590e96c01 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Fri, 6 Dec 2024 15:14:08 +0000 Subject: [PATCH 08/10] Update CHANGELOG.md --- CHANGELOG.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 599dc03646..2283df1684 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,8 @@ Bug-fixes Non-backwards compatible changes -------------------------------- +In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold. + Minor improvements ------------------ @@ -329,10 +331,10 @@ Additions to existing modules * In `Function.Related.TypeIsomorphisms`: ```agda - Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} → (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) - Σ-distribʳ-⊎ : {P : Set a} {Q : Set b} {R : P ⊎ Q → Set c} → (Σ (P ⊎ Q) R) ↔ (Σ P (R ∘ inj₁) ⊎ Σ Q (R ∘ inj₂)) - ×-distribˡ-⊎′ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) - ×-distribʳ-⊎′ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) + Σ-distribˡ-⊎ : (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) + Σ-distribʳ-⊎ : (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂)) + ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) + ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) ``` From 473195abf418bc930d47e9bafa4f374de38bd834 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 6 Dec 2024 15:20:06 +0000 Subject: [PATCH 09/10] [ fix ] whitespace violation --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a7de6bd5e7..c0dd26217b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -19,7 +19,7 @@ Bug-fixes Non-backwards compatible changes -------------------------------- -In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold. +In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold. Minor improvements ------------------ From 4f9ab4d822fdcac0ce514804ba4872ef1533d746 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Fri, 6 Dec 2024 15:56:31 +0000 Subject: [PATCH 10/10] use the more polymorphic one here --- src/Function/Related/TypeIsomorphisms.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index fa29312f7a..478ef28a2e 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -248,7 +248,7 @@ private ×-⊎-isCommutativeSemiring k ℓ = isCommutativeSemiringˡ record { +-isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ ; *-isCommutativeMonoid = ×-isCommutativeMonoid k ℓ - ; distribʳ = λ A B C → ↔⇒ (×-distribʳ-⊎ ℓ A B C) + ; distribʳ = λ _ _ _ → ↔⇒ ×-distribʳ-⊎ ; zeroˡ = ↔⇒ ∘ ×-zeroˡ ℓ }