From 0adbbe8acd1438b0f3b5f9fde77ee6bbd2e704a2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 11:22:29 +0100 Subject: [PATCH 01/37] introduced alternative definitions; revised one usage of previous one --- src/Data/Nat/Base.agda | 115 +++++++++++++++++++---------------- src/Data/Nat/Properties.agda | 4 +- 2 files changed, 66 insertions(+), 53 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 1e2db666b8..340eb544e0 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -12,8 +12,10 @@ module Data.Nat.Base where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring) +open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) +open import Data.Product.Base using (_,_; proj₁) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core @@ -120,11 +122,59 @@ instance >-nonZero⁻¹ (suc n) = z′ n = n <′ m ------------------------------------------------------------------------ -- Another alternative definition of _≤_ +infix 4 _≤″_ _<″_ _≥″_ _>″_ record _≤″_ (m n : ℕ) : Set where constructor less-than-or-equal @@ -265,7 +316,14 @@ record _≤″_ (m n : ℕ) : Set where {k} : ℕ proof : m + k ≡ n -infix 4 _≤″_ _<″_ _≥″_ _>″_ +{- + +_≤″_ : (m n : ℕ) → Set +_≤″_ = _∣ˡ_ +-rawMagma + +pattern less-than-or-equal {k} proof = k , proof + +-} _<″_ : Rel ℕ 0ℓ m <″ n = suc m ≤″ n @@ -275,7 +333,6 @@ m ≥″ n = n ≤″ m _>″_ : Rel ℕ 0ℓ m >″ n = n <″ m - ------------------------------------------------------------------------ -- Another alternative definition of _≤_ @@ -314,51 +371,7 @@ compare (suc m) (suc n) with compare m n ... | equal m = equal (suc m) ... | greater n k = greater (suc n) k ------------------------------------------------------------------------- --- Raw bundles - -+-rawMagma : RawMagma 0ℓ 0ℓ -+-rawMagma = record - { _≈_ = _≡_ - ; _∙_ = _+_ - } - -+-0-rawMonoid : RawMonoid 0ℓ 0ℓ -+-0-rawMonoid = record - { _≈_ = _≡_ - ; _∙_ = _+_ - ; ε = 0 - } - -*-rawMagma : RawMagma 0ℓ 0ℓ -*-rawMagma = record - { _≈_ = _≡_ - ; _∙_ = _*_ - } - -*-1-rawMonoid : RawMonoid 0ℓ 0ℓ -*-1-rawMonoid = record - { _≈_ = _≡_ - ; _∙_ = _*_ - ; ε = 1 - } - -+-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ -+-*-rawNearSemiring = record - { Carrier = _ - ; _≈_ = _≡_ - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0 - } - -+-*-rawSemiring : RawSemiring 0ℓ 0ℓ -+-*-rawSemiring = record - { Carrier = _ - ; _≈_ = _≡_ - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0 - ; 1# = 1 - } - +{- +proof : ∀ {m n} (le : m ≤″ n) → m + (_≤″_.k le) ≡ n +proof le = _≤″_.proof le +-} diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 3d38c77d07..37c3824e99 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -2098,8 +2098,8 @@ _>″?_ = flip _<″?_ ≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n ≤‴⇒≤″ {m = m} ≤‴-refl = less-than-or-equal {k = 0} (+-identityʳ m) -≤‴⇒≤″ {m = m} (≤‴-step x) = less-than-or-equal (trans (+-suc m _) (_≤″_.proof ind)) where - ind = ≤‴⇒≤″ x +≤‴⇒≤″ {m = m} (≤‴-step x) with less-than-or-equal proof ← ≤‴⇒≤″ x + = less-than-or-equal (trans (+-suc m _) proof) m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m}) From b62ef817c3bd41fcbcf018d4036244ee8dd15a74 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 11:56:49 +0100 Subject: [PATCH 02/37] deprecated field name (NB tricky) --- README/Design/Decidability.agda | 2 +- src/Data/Nat/Base.agda | 14 +++++++++++--- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index e615af282e..3f267bed4a 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -11,7 +11,7 @@ module README.Design.Decidability where open import Data.Bool open import Data.List open import Data.List.Properties using (∷-injective) -open import Data.Nat +open import Data.Nat hiding (proof) open import Data.Nat.Properties using (suc-injective) open import Data.Product open import Data.Unit diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 340eb544e0..64854b5c99 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -15,7 +15,6 @@ open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; Raw open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) -open import Data.Product.Base using (_,_; proj₁) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core @@ -371,7 +370,16 @@ compare (suc m) (suc n) with compare m n ... | equal m = equal (suc m) ... | greater n k = greater (suc n) k -{- +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + proof : ∀ {m n} (le : m ≤″ n) → m + (_≤″_.k le) ≡ n proof le = _≤″_.proof le --} +{-# WARNING_ON_USAGE proof +"Warning: _≤″_.proof was deprecated in v2.0. Please use pattern-matching instead. Note that the definition of _≤″_ has changed" +#-} From 8993f590b27abf63736db38a5519074aa7761420 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 12:00:28 +0100 Subject: [PATCH 03/37] installed new definition --- src/Data/Nat/Base.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 64854b5c99..15c585ed70 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -15,6 +15,7 @@ open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; Raw open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) +open import Data.Product.Base using (_,_; proj₁) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core @@ -309,21 +310,21 @@ m >′ n = n <′ m -- Another alternative definition of _≤_ infix 4 _≤″_ _<″_ _≥″_ _>″_ +{- + record _≤″_ (m n : ℕ) : Set where constructor less-than-or-equal field {k} : ℕ proof : m + k ≡ n -{- +-} _≤″_ : (m n : ℕ) → Set _≤″_ = _∣ˡ_ +-rawMagma pattern less-than-or-equal {k} proof = k , proof --} - _<″_ : Rel ℕ 0ℓ m <″ n = suc m ≤″ n @@ -378,8 +379,8 @@ compare (suc m) (suc n) with compare m n -- Version 2.0 -proof : ∀ {m n} (le : m ≤″ n) → m + (_≤″_.k le) ≡ n -proof le = _≤″_.proof le +proof : ∀ {m n} (le : m ≤″ n) → m + (proj₁ le) ≡ n +proof (less-than-or-equal {k} prf) = prf {-# WARNING_ON_USAGE proof "Warning: _≤″_.proof was deprecated in v2.0. Please use pattern-matching instead. Note that the definition of _≤″_ has changed" #-} From 7f098087eb95158b6a55d3eac2fc46d8068cd9e9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 12:12:04 +0100 Subject: [PATCH 04/37] removed old definition; tidied up --- src/Data/Nat/Base.agda | 12 ++---------- src/Data/Nat/Combinatorics.agda | 4 ++-- 2 files changed, 4 insertions(+), 12 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 15c585ed70..e4945c470f 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -310,16 +310,6 @@ m >′ n = n <′ m -- Another alternative definition of _≤_ infix 4 _≤″_ _<″_ _≥″_ _>″_ -{- - -record _≤″_ (m n : ℕ) : Set where - constructor less-than-or-equal - field - {k} : ℕ - proof : m + k ≡ n - --} - _≤″_ : (m n : ℕ) → Set _≤″_ = _∣ˡ_ +-rawMagma @@ -333,6 +323,7 @@ m ≥″ n = n ≤″ m _>″_ : Rel ℕ 0ℓ m >″ n = n <″ m + ------------------------------------------------------------------------ -- Another alternative definition of _≤_ @@ -371,6 +362,7 @@ compare (suc m) (suc n) with compare m n ... | equal m = equal (suc m) ... | greater n k = greater (suc n) k + ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda index 6db600699c..850cd01857 100644 --- a/src/Data/Nat/Combinatorics.agda +++ b/src/Data/Nat/Combinatorics.agda @@ -12,7 +12,7 @@ open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Divisibility open import Data.Nat.Properties -open import Relation.Binary.Definitions +open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; subst) @@ -118,7 +118,7 @@ module _ {n k} (k Date: Sat, 22 Apr 2023 12:38:44 +0100 Subject: [PATCH 05/37] `CHANGELOG` plus portable definition of the `proof` projection --- CHANGELOG.md | 27 +++++++++++++++++++++++++++ src/Data/Nat/Base.agda | 2 +- 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ca38cd42..de0d9fff33 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -427,6 +427,28 @@ Non-backwards compatible changes Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n ``` +### Change in the definition of `_≤″_` + +* The definition of `_≤″_` in `Data.Nat.Base` was previously: + ```agda + ``` + which introduced a spurious additional definition, when this is in fact, modulo + field names and implicit/explicit qualifiers, equivalent to the definition of left- + divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. Since the addition of + raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on + consequences include the need to retain the old constructor name, now introduced + as a pattern synonym, and deprecation of (a function equiavlent to) the former + field name/projection function `proof`. + +* Accordingly, the definition has been + changed to: + ```agda + _≤″_ : (m n : ℕ) → Set + _≤″_ = _∣ˡ_ +-rawMagma + + pattern less-than-or-equal {k} proof = k , proof + ``` + ### Renaming of `Reflection` modules * Under the `Reflection` module, there were various impending name clashes @@ -1109,6 +1131,11 @@ Deprecated names map-with-∈↔ ↦ mapWith∈↔ ``` +* In `Data.Nat.Base`: + ``` + _≤″_.proof ↦ proj₂ + ``` + * In `Data.Nat.Properties`: ``` suc[pred[n]]≡n ↦ suc-pred diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index e4945c470f..1d6cca47ca 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -371,7 +371,7 @@ compare (suc m) (suc n) with compare m n -- Version 2.0 -proof : ∀ {m n} (le : m ≤″ n) → m + (proj₁ le) ≡ n +proof : ∀ {m n} (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n proof (less-than-or-equal {k} prf) = prf {-# WARNING_ON_USAGE proof "Warning: _≤″_.proof was deprecated in v2.0. Please use pattern-matching instead. Note that the definition of _≤″_ has changed" From 5935db49992de04d76714668b012a0222277af56 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 12:42:02 +0100 Subject: [PATCH 06/37] `CHANGELOG` --- CHANGELOG.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index de0d9fff33..2545988cd6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -427,10 +427,15 @@ Non-backwards compatible changes Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n ``` -### Change in the definition of `_≤″_` +### Change in the definition of `_≤″_` (issue #1919) * The definition of `_≤″_` in `Data.Nat.Base` was previously: ```agda + record _≤″_ (m n : ℕ) : Set where + constructor less-than-or-equal + field + {k} : ℕ + proof : m + k ≡ n ``` which introduced a spurious additional definition, when this is in fact, modulo field names and implicit/explicit qualifiers, equivalent to the definition of left- @@ -440,8 +445,7 @@ Non-backwards compatible changes as a pattern synonym, and deprecation of (a function equiavlent to) the former field name/projection function `proof`. -* Accordingly, the definition has been - changed to: +* Accordingly, the definition has been changed to: ```agda _≤″_ : (m n : ℕ) → Set _≤″_ = _∣ˡ_ +-rawMagma From 829ddd5fdb5644752b8f4034ab732aa16011cea3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 12:58:39 +0100 Subject: [PATCH 07/37] more explicit deprecation warning --- src/Data/Nat/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 1d6cca47ca..a9c21d9359 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -374,5 +374,5 @@ compare (suc m) (suc n) with compare m n proof : ∀ {m n} (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n proof (less-than-or-equal {k} prf) = prf {-# WARNING_ON_USAGE proof -"Warning: _≤″_.proof was deprecated in v2.0. Please use pattern-matching instead. Note that the definition of _≤″_ has changed" +"Warning: _≤″_.proof was deprecated in v2.0. Please use pattern-matching on less-than-or-equal instead. Note that the definition of _≤″_ has changed" #-} From e9c7170eca2c551f7d2a939dec8b89b3b3151df6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 23 Apr 2023 15:38:44 +0100 Subject: [PATCH 08/37] typo in `CHANGELOG` --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2545988cd6..ea4338176e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -442,7 +442,7 @@ Non-backwards compatible changes divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. Since the addition of raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on consequences include the need to retain the old constructor name, now introduced - as a pattern synonym, and deprecation of (a function equiavlent to) the former + as a pattern synonym, and deprecation of (a function equivalent to) the former field name/projection function `proof`. * Accordingly, the definition has been changed to: From 824dce6b1219a6c3909863ba9e4ebe1504a98454 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 17:48:05 +0100 Subject: [PATCH 09/37] exchnaged repeated recursive for a nested irrefutbale `with` pattern --- src/Data/List/Properties.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index e9ddbe6387..98a7ef92ad 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -905,16 +905,16 @@ module _ {P : Pred A p} (P? : Decidable P) where partition-defn : partition P? ≗ < filter P? , filter (∁? P?) > partition-defn [] = refl - partition-defn (x ∷ xs) with does (P? x) - ... | true = cong (Prod.map (x ∷_) id) (partition-defn xs) - ... | false = cong (Prod.map id (x ∷_)) (partition-defn xs) + partition-defn (x ∷ xs) with rec ← partition-defn xs with does (P? x) + ... | true = cong (Prod.map (x ∷_) id) rec + ... | false = cong (Prod.map id (x ∷_)) rec length-partition : ∀ xs → (let (ys , zs) = partition P? xs) → length ys ≤ length xs × length zs ≤ length xs length-partition [] = z≤n , z≤n - length-partition (x ∷ xs) with does (P? x) | length-partition xs - ... | true | rec = Prod.map s≤s m≤n⇒m≤1+n rec - ... | false | rec = Prod.map m≤n⇒m≤1+n s≤s rec + length-partition (x ∷ xs) with rec ← length-partition xs with does (P? x) + ... | true = Prod.map s≤s m≤n⇒m≤1+n rec + ... | false = Prod.map m≤n⇒m≤1+n s≤s rec ------------------------------------------------------------------------ -- _ʳ++_ From 61ef3f0723aa0f66f8e434233858b7d59a3b0565 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 18:51:19 +0100 Subject: [PATCH 10/37] Revert "Merge branch 'issue1919' of https://github.com/jamesmckinna/agda-stdlib into issue1919" This reverts commit dbfb5a7747b8ee8c1d8c83bb63b1285735ba4b14, reversing changes made to 824dce6b1219a6c3909863ba9e4ebe1504a98454. --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ea4338176e..2545988cd6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -442,7 +442,7 @@ Non-backwards compatible changes divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. Since the addition of raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on consequences include the need to retain the old constructor name, now introduced - as a pattern synonym, and deprecation of (a function equivalent to) the former + as a pattern synonym, and deprecation of (a function equiavlent to) the former field name/projection function `proof`. * Accordingly, the definition has been changed to: From 693270e8d930c9e04ef8cb2afb6526198981979b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 18:52:51 +0100 Subject: [PATCH 11/37] Revert "exchnaged repeated recursive for a nested irrefutbale `with` pattern" This reverts commit 824dce6b1219a6c3909863ba9e4ebe1504a98454. --- src/Data/List/Properties.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 98a7ef92ad..e9ddbe6387 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -905,16 +905,16 @@ module _ {P : Pred A p} (P? : Decidable P) where partition-defn : partition P? ≗ < filter P? , filter (∁? P?) > partition-defn [] = refl - partition-defn (x ∷ xs) with rec ← partition-defn xs with does (P? x) - ... | true = cong (Prod.map (x ∷_) id) rec - ... | false = cong (Prod.map id (x ∷_)) rec + partition-defn (x ∷ xs) with does (P? x) + ... | true = cong (Prod.map (x ∷_) id) (partition-defn xs) + ... | false = cong (Prod.map id (x ∷_)) (partition-defn xs) length-partition : ∀ xs → (let (ys , zs) = partition P? xs) → length ys ≤ length xs × length zs ≤ length xs length-partition [] = z≤n , z≤n - length-partition (x ∷ xs) with rec ← length-partition xs with does (P? x) - ... | true = Prod.map s≤s m≤n⇒m≤1+n rec - ... | false = Prod.map m≤n⇒m≤1+n s≤s rec + length-partition (x ∷ xs) with does (P? x) | length-partition xs + ... | true | rec = Prod.map s≤s m≤n⇒m≤1+n rec + ... | false | rec = Prod.map m≤n⇒m≤1+n s≤s rec ------------------------------------------------------------------------ -- _ʳ++_ From f120c1ee4ba08fc8ad279bdd40d350c5b87bad0b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 25 Apr 2023 14:50:55 +0100 Subject: [PATCH 12/37] tweaks --- CHANGELOG.md | 2 +- src/Data/Nat/Base.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2545988cd6..9154cfc17b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1137,7 +1137,7 @@ Deprecated names * In `Data.Nat.Base`: ``` - _≤″_.proof ↦ proj₂ + _≤″_.proof ↦ Data.Product.Base.proj₂ ``` * In `Data.Nat.Properties`: diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index a9c21d9359..5dc16c0183 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -15,7 +15,7 @@ open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; Raw open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) -open import Data.Product.Base using (_,_; proj₁) +open import Data.Product.Base using (_,_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core From 887e6522c247fa267e8d279ae954666c58bfcee5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 27 Apr 2023 13:22:47 +0100 Subject: [PATCH 13/37] The free `Magma` on a `Set`, resp. `Setoid` --- CHANGELOG.md | 6 ++ src/Algebra/Bundles/Free.agda | 11 +++ src/Algebra/Bundles/Free/Magma.agda | 129 ++++++++++++++++++++++++++++ 3 files changed, 146 insertions(+) create mode 100644 src/Algebra/Bundles/Free.agda create mode 100644 src/Algebra/Bundles/Free/Magma.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ca38cd42..e2453f320d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1325,6 +1325,12 @@ New modules Algebra.Construct.Flip.Op ``` +* Algebraic structures obtained as the free thing (for their signature): + ``` + Algebra.Bundles.Free + Algebra.Bundles.Free.Magma + ``` + * Morphisms between module-like algebraic structures: ``` Algebra.Module.Morphism.Construct.Composition diff --git a/src/Algebra/Bundles/Free.agda b/src/Algebra/Bundles/Free.agda new file mode 100644 index 0000000000..2a6771c5e5 --- /dev/null +++ b/src/Algebra/Bundles/Free.agda @@ -0,0 +1,11 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions of 'pre-free' and 'free' bundles +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Bundles.Free where + +open import Algebra.Bundles.Free.Magma public diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda new file mode 100644 index 0000000000..727503a38f --- /dev/null +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -0,0 +1,129 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions of 'pre-free' and 'free' magma +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Bundles.Free.Magma where + +open import Algebra.Core +import Algebra.Definitions as Defs using (Congruent₂) +import Algebra.Structures as Strs using (IsMagma) +open import Algebra.Bundles using (Magma) +open import Algebra.Bundles.Raw using (RawMagma) +open import Relation.Binary.Core using (Rel) +open import Level using (Level; _⊔_) +open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Binary using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) +open import Relation.Binary.PropositionalEquality + using (_≡_; cong₂) renaming (refl to ≡refl; isEquivalence to ≡isEquivalence) + +------------------------------------------------------------------------ +-- 'pre'-free algebra + +infixl 7 _∙_ + +data PreFreeMagma {c} (A : Set c) : Set c where + + var : A → PreFreeMagma A + _∙_ : Op₂ (PreFreeMagma A) + +------------------------------------------------------------------------ +-- parametrised 'equational' theory over the 'pre'-free algebra + +module PreFreeTheory {c ℓ} {A : Set c} (R : Rel A ℓ) where + + data PreFreeMagmaTheory : Rel (PreFreeMagma A) (c ⊔ ℓ) + + open Defs PreFreeMagmaTheory + + data PreFreeMagmaTheory where + + var : ∀ {a b} → (R a b) → PreFreeMagmaTheory (var a) (var b) + _∙_ : Congruent₂ _∙_ + +PreFreeTheorySyntax : ∀ {c ℓ} {A : Set c} (R : Rel A ℓ) → Rel (PreFreeMagma A) (c ⊔ ℓ) +PreFreeTheorySyntax R = PreFreeMagmaTheory where open PreFreeTheory R + +syntax PreFreeTheorySyntax R m n = m ≈[ R ] n + +module PreservesEquivalence {c ℓ} {A : Set c} (R : Rel A ℓ) where + + open PreFreeTheory R + + _≈R_ = λ m n → m ≈[ R ] n + + refl : (Reflexive R) → Reflexive _≈R_ + refl r {var _} = var r + refl r {_ ∙ _} = (refl r) ∙ (refl r) + + sym : (Symmetric R) → Symmetric _≈R_ + sym s (var r) = var (s r) + sym s (r₁ ∙ r₂) = sym s r₁ ∙ sym s r₂ + + trans : (Transitive R) → Transitive _≈R_ + trans t (var r) (var s) = var (t r s) + trans t (r₁ ∙ r₂) (s₁ ∙ s₂) = trans t r₁ s₁ ∙ trans t r₂ s₂ + + preservesEquivalence : IsEquivalence R → IsEquivalence _≈R_ + preservesEquivalence eq = record { refl = refl r ; sym = sym s ; trans = trans t } + where open IsEquivalence eq renaming (refl to r; sym to s; trans to t) + +------------------------------------------------------------------------ +-- Free algebra on a Setoid + +module FreeMagmaOn {c ℓ} (S : Setoid c ℓ) where + + open Setoid S renaming (Carrier to A; isEquivalence to isEq) + + open PreFreeTheory _≈_ + + open PreservesEquivalence _≈_ + + open Strs _≈R_ + + isMagma : IsMagma _∙_ + isMagma = record { isEquivalence = preservesEquivalence isEq ; ∙-cong = _∙_ } + + freeMagma : Magma c (c ⊔ ℓ) + freeMagma = record { Carrier = PreFreeMagma A; _≈_ = _≈R_ ; _∙_ = _∙_ ; isMagma = isMagma } + +{- in the propositional case, we can immediately define the following + but how best to organise this under the Algebra.Bundles.Free hierarchy? -} + +------------------------------------------------------------------------ +-- Free algebra on a Set + +module FreeMagma {c} (A : Set c) where + + private Carrier = PreFreeMagma A + + _≈_ : Rel Carrier c + m ≈ n = m ≈[ _≡_ ] n + + open PreFreeTheory {A = A} _≡_ + + ≈⇒≡ : ∀ {m n} → m ≈ n → m ≡ n + ≈⇒≡ (var ≡refl) = ≡refl + ≈⇒≡ (eq₁ ∙ eq₂) = cong₂ _∙_ (≈⇒≡ eq₁) (≈⇒≡ eq₂) + + refl : Reflexive _≈_ + refl {var _} = var ≡refl + refl {_ ∙ _} = refl ∙ refl + + ≡⇒≈ : ∀ {m n} → m ≡ n → m ≈ n + ≡⇒≈ ≡refl = refl + + rawFreeMagma : RawMagma c c + rawFreeMagma = record { Carrier = Carrier ; _≈_ = _≡_ ; _∙_ = _∙_ } + + open Strs {A = Carrier} _≡_ + + isMagma : IsMagma _∙_ + isMagma = record { isEquivalence = ≡isEquivalence ; ∙-cong = cong₂ _∙_ } + + freeMagma : Magma c c + freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } + From 60d912bd088315b49edc5dae672ff0cf367af2ca Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 27 Apr 2023 18:49:24 +0100 Subject: [PATCH 14/37] proof of uniquness of the `eval` homomorphism --- src/Algebra/Bundles/Free/Magma.agda | 93 +++++++++++++++++++++++++++-- 1 file changed, 87 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 727503a38f..150aeaf7b3 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -11,14 +11,19 @@ module Algebra.Bundles.Free.Magma where open import Algebra.Core import Algebra.Definitions as Defs using (Congruent₂) import Algebra.Structures as Strs using (IsMagma) +open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) open import Algebra.Bundles using (Magma) open import Algebra.Bundles.Raw using (RawMagma) +open import Function.Base using (id; _∘_) open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Morphism using (Homomorphic₂; IsRelHomomorphism) open import Level using (Level; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) -open import Relation.Binary using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) +open import Relation.Binary + using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) open import Relation.Binary.PropositionalEquality using (_≡_; cong₂) renaming (refl to ≡refl; isEquivalence to ≡isEquivalence) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- 'pre'-free algebra @@ -30,6 +35,10 @@ data PreFreeMagma {c} (A : Set c) : Set c where var : A → PreFreeMagma A _∙_ : Op₂ (PreFreeMagma A) +map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → PreFreeMagma A → PreFreeMagma B +map f (var a) = var (f a) +map f (s ∙ t) = (map f s) ∙ (map f t) + ------------------------------------------------------------------------ -- parametrised 'equational' theory over the 'pre'-free algebra @@ -68,8 +77,8 @@ module PreservesEquivalence {c ℓ} {A : Set c} (R : Rel A ℓ) where trans t (r₁ ∙ r₂) (s₁ ∙ s₂) = trans t r₁ s₁ ∙ trans t r₂ s₂ preservesEquivalence : IsEquivalence R → IsEquivalence _≈R_ - preservesEquivalence eq = record { refl = refl r ; sym = sym s ; trans = trans t } - where open IsEquivalence eq renaming (refl to r; sym to s; trans to t) + preservesEquivalence isEq = record { refl = refl r ; sym = sym s ; trans = trans t } + where open IsEquivalence isEq renaming (refl to r; sym to s; trans to t) ------------------------------------------------------------------------ -- Free algebra on a Setoid @@ -78,7 +87,7 @@ module FreeMagmaOn {c ℓ} (S : Setoid c ℓ) where open Setoid S renaming (Carrier to A; isEquivalence to isEq) - open PreFreeTheory _≈_ + open PreFreeTheory _≈_ public open PreservesEquivalence _≈_ @@ -88,7 +97,7 @@ module FreeMagmaOn {c ℓ} (S : Setoid c ℓ) where isMagma = record { isEquivalence = preservesEquivalence isEq ; ∙-cong = _∙_ } freeMagma : Magma c (c ⊔ ℓ) - freeMagma = record { Carrier = PreFreeMagma A; _≈_ = _≈R_ ; _∙_ = _∙_ ; isMagma = isMagma } + freeMagma = record { Carrier = PreFreeMagma A; _≈_ = _≈R_ ; _∙_ = _∙_ ; isMagma = isMagma } {- in the propositional case, we can immediately define the following but how best to organise this under the Algebra.Bundles.Free hierarchy? -} @@ -123,7 +132,79 @@ module FreeMagma {c} (A : Set c) where isMagma : IsMagma _∙_ isMagma = record { isEquivalence = ≡isEquivalence ; ∙-cong = cong₂ _∙_ } - + freeMagma : Magma c c freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } +------------------------------------------------------------------------ +-- Eval, as the unique fold ⟦_⟧ over PreFreeMagma A + +module Eval {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where + + open Setoid 𝓐 renaming (Carrier to A) + + open Magma 𝓜 renaming (Carrier to M; _∙_ to _∙ᴹ_) + + ⟦_⟧_ : PreFreeMagma A → (A → M) → M + ⟦ var a ⟧ η = η a + ⟦ s ∙ t ⟧ η = ⟦ s ⟧ η ∙ᴹ ⟦ t ⟧ η + +module Alg {m ℓm} (𝓜 : Magma m ℓm) where + + open Magma 𝓜 renaming (setoid to setoidᴹ; Carrier to M) + + open Eval setoidᴹ 𝓜 + + algᴹ : PreFreeMagma M → M + algᴹ t = ⟦ t ⟧ id + +module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where + + open Setoid 𝓐 renaming (Carrier to A) + + open Magma 𝓜 + renaming (Carrier to M; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ + ; setoid to setoidᴹ; rawMagma to rawMagmaᴹ; refl to reflᴹ + ; isMagma to isMagmaᴹ) + + open Eval 𝓐 𝓜 + + open Alg 𝓜 + + open FreeMagmaOn 𝓐 + open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA; _≈_ to _≈ᴬ_) + + module _ {η : A → M} (var-η : Homomorphic₂ A M _≈_ _≈ᴹ_ η) where + + open Strs _≈ᴹ_ + open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) + + cong : ∀ {s t} → s ≈ᴬ t → ⟦ s ⟧ η ≈ᴹ ⟦ t ⟧ η + cong (var r) = var-η r + cong (s ∙ t) = congᴹ (cong s) (cong t) + + isRelHomomorphism : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ (⟦_⟧ η) + isRelHomomorphism = record { cong = cong } + + isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ (⟦_⟧ η) + isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism + ; homo = λ _ _ → reflᴹ + } + + unfold-⟦_⟧ : ∀ t → ⟦ t ⟧ η ≈ᴹ algᴹ (map η t) + unfold-⟦ var a ⟧ = reflᴹ + unfold-⟦ s ∙ t ⟧ = congᴹ unfold-⟦ s ⟧ unfold-⟦ t ⟧ + + module _ {h : FA → M} (isHom : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ h) + (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) where + + open IsMagmaHomomorphism isHom + + open ≈-Reasoning setoidᴹ + + isUnique⟦_⟧ : ∀ t → h t ≈ᴹ ⟦ t ⟧ η + isUnique⟦ var a ⟧ = h∘var≈ᴹη a + isUnique⟦ s ∙ t ⟧ = begin + h (s PreFreeMagma.∙ t) ≈⟨ homo s t ⟩ + (h s) ∙ᴹ (h t) ≈⟨ congᴹ isUnique⟦ s ⟧ isUnique⟦ t ⟧ ⟩ + ⟦ s ⟧ η ∙ᴹ (⟦ t ⟧ η) ∎ From c994ceba43500e436d17bdb2c56ae9b71b5444ad Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 07:44:04 +0100 Subject: [PATCH 15/37] functoriality of `map` --- src/Algebra/Bundles/Free/Magma.agda | 33 ++++++++++++++++++++++------- 1 file changed, 25 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 150aeaf7b3..2f32cd1b46 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -22,22 +22,38 @@ open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) open import Relation.Binary.PropositionalEquality - using (_≡_; cong₂) renaming (refl to ≡refl; isEquivalence to ≡isEquivalence) + using (_≡_; cong₂) renaming (refl to ≡-refl; isEquivalence to ≡isEquivalence) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + ------------------------------------------------------------------------ -- 'pre'-free algebra infixl 7 _∙_ -data PreFreeMagma {c} (A : Set c) : Set c where +data PreFreeMagma {a} (A : Set a) : Set a where var : A → PreFreeMagma A _∙_ : Op₂ (PreFreeMagma A) -map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → PreFreeMagma A → PreFreeMagma B -map f (var a) = var (f a) -map f (s ∙ t) = (map f s) ∙ (map f t) +module _ {a b} {A : Set a} {B : Set b} where + + map : (A → B) → PreFreeMagma A → PreFreeMagma B + map f (var a) = var (f a) + map f (s ∙ t) = (map f s) ∙ (map f t) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + map-id : ∀ (t : PreFreeMagma A) → map id t ≡ t + map-id (var a) = ≡-refl + map-id (s ∙ t) = cong₂ _∙_ (map-id s) (map-id t) + + map-∘ : (g : A → B) → (f : B → C) → ∀ t → map (f ∘ g) t ≡ (map f ∘ map g) t + map-∘ g f (var a) = ≡-refl + map-∘ g f (s ∙ t) = cong₂ _∙_ (map-∘ g f s) (map-∘ g f t) + +------------------------------------------------------------------------ +-- RawMonad, Monad instances TODO ------------------------------------------------------------------------ -- parametrised 'equational' theory over the 'pre'-free algebra @@ -115,15 +131,15 @@ module FreeMagma {c} (A : Set c) where open PreFreeTheory {A = A} _≡_ ≈⇒≡ : ∀ {m n} → m ≈ n → m ≡ n - ≈⇒≡ (var ≡refl) = ≡refl + ≈⇒≡ (var ≡-refl) = ≡-refl ≈⇒≡ (eq₁ ∙ eq₂) = cong₂ _∙_ (≈⇒≡ eq₁) (≈⇒≡ eq₂) refl : Reflexive _≈_ - refl {var _} = var ≡refl + refl {var _} = var ≡-refl refl {_ ∙ _} = refl ∙ refl ≡⇒≈ : ∀ {m n} → m ≡ n → m ≈ n - ≡⇒≈ ≡refl = refl + ≡⇒≈ ≡-refl = refl rawFreeMagma : RawMagma c c rawFreeMagma = record { Carrier = Carrier ; _≈_ = _≡_ ; _∙_ = _∙_ } @@ -172,6 +188,7 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w open Alg 𝓜 open FreeMagmaOn 𝓐 + open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA; _≈_ to _≈ᴬ_) module _ {η : A → M} (var-η : Homomorphic₂ A M _≈_ _≈ᴹ_ η) where From 8da3c1c378ad95fe7af6ac28a0fc202e00a99651 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 09:57:45 +0100 Subject: [PATCH 16/37] tidying up --- src/Algebra/Bundles/Free/Magma.agda | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 2f32cd1b46..af443c98cb 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -16,13 +16,13 @@ open import Algebra.Bundles using (Magma) open import Algebra.Bundles.Raw using (RawMagma) open import Function.Base using (id; _∘_) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Morphism using (Homomorphic₂; IsRelHomomorphism) +open import Relation.Binary.Morphism using (IsRelHomomorphism) open import Level using (Level; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) open import Relation.Binary.PropositionalEquality - using (_≡_; cong₂) renaming (refl to ≡-refl; isEquivalence to ≡isEquivalence) + using (_≡_; cong₂) renaming (refl to ≡-refl; isEquivalence to ≡-isEquivalence) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -53,7 +53,7 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where map-∘ g f (s ∙ t) = cong₂ _∙_ (map-∘ g f s) (map-∘ g f t) ------------------------------------------------------------------------ --- RawMonad, Monad instances TODO +-- Functor, RawMonad instance: TODO ------------------------------------------------------------------------ -- parametrised 'equational' theory over the 'pre'-free algebra @@ -80,15 +80,15 @@ module PreservesEquivalence {c ℓ} {A : Set c} (R : Rel A ℓ) where _≈R_ = λ m n → m ≈[ R ] n - refl : (Reflexive R) → Reflexive _≈R_ + refl : Reflexive R → Reflexive _≈R_ refl r {var _} = var r refl r {_ ∙ _} = (refl r) ∙ (refl r) - sym : (Symmetric R) → Symmetric _≈R_ + sym : Symmetric R → Symmetric _≈R_ sym s (var r) = var (s r) sym s (r₁ ∙ r₂) = sym s r₁ ∙ sym s r₂ - trans : (Transitive R) → Transitive _≈R_ + trans : Transitive R → Transitive _≈R_ trans t (var r) (var s) = var (t r s) trans t (r₁ ∙ r₂) (s₁ ∙ s₂) = trans t r₁ s₁ ∙ trans t r₂ s₂ @@ -147,7 +147,7 @@ module FreeMagma {c} (A : Set c) where open Strs {A = Carrier} _≡_ isMagma : IsMagma _∙_ - isMagma = record { isEquivalence = ≡isEquivalence ; ∙-cong = cong₂ _∙_ } + isMagma = record { isEquivalence = ≡-isEquivalence ; ∙-cong = cong₂ _∙_ } freeMagma : Magma c c freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } @@ -191,13 +191,14 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA; _≈_ to _≈ᴬ_) - module _ {η : A → M} (var-η : Homomorphic₂ A M _≈_ _≈ᴹ_ η) where + module _ {η : A → M} (hom-η : IsRelHomomorphism _≈_ _≈ᴹ_ η) where open Strs _≈ᴹ_ open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) + open IsRelHomomorphism hom-η renaming (cong to cong-η) cong : ∀ {s t} → s ≈ᴬ t → ⟦ s ⟧ η ≈ᴹ ⟦ t ⟧ η - cong (var r) = var-η r + cong (var r) = cong-η r cong (s ∙ t) = congᴹ (cong s) (cong t) isRelHomomorphism : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ (⟦_⟧ η) @@ -224,4 +225,8 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w isUnique⟦ s ∙ t ⟧ = begin h (s PreFreeMagma.∙ t) ≈⟨ homo s t ⟩ (h s) ∙ᴹ (h t) ≈⟨ congᴹ isUnique⟦ s ⟧ isUnique⟦ t ⟧ ⟩ - ⟦ s ⟧ η ∙ᴹ (⟦ t ⟧ η) ∎ + ⟦ s ⟧ η ∙ᴹ (⟦ t ⟧ η) ∎ + +------------------------------------------------------------------------ +-- Monad instance: TODO + From 9458ae246ccc340340ffefae6318ba5982db82f4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 10:10:42 +0100 Subject: [PATCH 17/37] notational tidying up --- src/Algebra/Bundles/Free/Magma.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index af443c98cb..277bef0865 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -176,7 +176,7 @@ module Alg {m ℓm} (𝓜 : Magma m ℓm) where module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where - open Setoid 𝓐 renaming (Carrier to A) + open Setoid 𝓐 renaming (Carrier to A; _≈_ to _≈ᴬ_) open Magma 𝓜 renaming (Carrier to M; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ @@ -189,19 +189,19 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w open FreeMagmaOn 𝓐 - open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA; _≈_ to _≈ᴬ_) + open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA) - module _ {η : A → M} (hom-η : IsRelHomomorphism _≈_ _≈ᴹ_ η) where + module _ {η : A → M} (hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ η) where open Strs _≈ᴹ_ open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) open IsRelHomomorphism hom-η renaming (cong to cong-η) - cong : ∀ {s t} → s ≈ᴬ t → ⟦ s ⟧ η ≈ᴹ ⟦ t ⟧ η + cong : ∀ {s t} → s ≈ t → ⟦ s ⟧ η ≈ᴹ ⟦ t ⟧ η cong (var r) = cong-η r cong (s ∙ t) = congᴹ (cong s) (cong t) - isRelHomomorphism : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ (⟦_⟧ η) + isRelHomomorphism : IsRelHomomorphism _≈_ _≈ᴹ_ (⟦_⟧ η) isRelHomomorphism = record { cong = cong } isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ (⟦_⟧ η) From 7d63a624a3796fbf2d0194cb34b3c5b7d360a409 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 10:14:40 +0100 Subject: [PATCH 18/37] fix-whitespace --- src/Algebra/Bundles/Free/Magma.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 277bef0865..4cdaf40cf4 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -51,7 +51,7 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where map-∘ : (g : A → B) → (f : B → C) → ∀ t → map (f ∘ g) t ≡ (map f ∘ map g) t map-∘ g f (var a) = ≡-refl map-∘ g f (s ∙ t) = cong₂ _∙_ (map-∘ g f s) (map-∘ g f t) - + ------------------------------------------------------------------------ -- Functor, RawMonad instance: TODO @@ -188,7 +188,7 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w open Alg 𝓜 open FreeMagmaOn 𝓐 - + open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA) module _ {η : A → M} (hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ η) where From 4c4e152258f2e4f28c46d0735ce024b117722d10 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 10:36:54 +0100 Subject: [PATCH 19/37] tweak notation --- src/Algebra/Bundles/Free/Magma.agda | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 4cdaf40cf4..8ebcf4e979 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -193,25 +193,28 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w module _ {η : A → M} (hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ η) where + ⟦_⟧ᴹ : FA → M + ⟦_⟧ᴹ = ⟦_⟧ η + open Strs _≈ᴹ_ open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) open IsRelHomomorphism hom-η renaming (cong to cong-η) - cong : ∀ {s t} → s ≈ t → ⟦ s ⟧ η ≈ᴹ ⟦ t ⟧ η + cong : ∀ {s t} → s ≈ t → ⟦ s ⟧ᴹ ≈ᴹ ⟦ t ⟧ᴹ cong (var r) = cong-η r cong (s ∙ t) = congᴹ (cong s) (cong t) - isRelHomomorphism : IsRelHomomorphism _≈_ _≈ᴹ_ (⟦_⟧ η) + isRelHomomorphism : IsRelHomomorphism _≈_ _≈ᴹ_ ⟦_⟧ᴹ isRelHomomorphism = record { cong = cong } - isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ (⟦_⟧ η) + isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ ⟦_⟧ᴹ isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism ; homo = λ _ _ → reflᴹ } - unfold-⟦_⟧ : ∀ t → ⟦ t ⟧ η ≈ᴹ algᴹ (map η t) - unfold-⟦ var a ⟧ = reflᴹ - unfold-⟦ s ∙ t ⟧ = congᴹ unfold-⟦ s ⟧ unfold-⟦ t ⟧ + unfold-⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ᴹ ≈ᴹ algᴹ (map η t) + unfold-⟦ var a ⟧ᴹ = reflᴹ + unfold-⟦ s ∙ t ⟧ᴹ = congᴹ unfold-⟦ s ⟧ᴹ unfold-⟦ t ⟧ᴹ module _ {h : FA → M} (isHom : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ h) (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) where @@ -220,12 +223,12 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w open ≈-Reasoning setoidᴹ - isUnique⟦_⟧ : ∀ t → h t ≈ᴹ ⟦ t ⟧ η - isUnique⟦ var a ⟧ = h∘var≈ᴹη a - isUnique⟦ s ∙ t ⟧ = begin + isUnique⟦_⟧ᴹ : ∀ t → h t ≈ᴹ ⟦ t ⟧ᴹ + isUnique⟦ var a ⟧ᴹ = h∘var≈ᴹη a + isUnique⟦ s ∙ t ⟧ᴹ = begin h (s PreFreeMagma.∙ t) ≈⟨ homo s t ⟩ - (h s) ∙ᴹ (h t) ≈⟨ congᴹ isUnique⟦ s ⟧ isUnique⟦ t ⟧ ⟩ - ⟦ s ⟧ η ∙ᴹ (⟦ t ⟧ η) ∎ + (h s) ∙ᴹ (h t) ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ + ⟦ s ⟧ᴹ ∙ᴹ (⟦ t ⟧ᴹ) ∎ ------------------------------------------------------------------------ -- Monad instance: TODO From 4492833369309ced657aaa42c61075bb7ffa9d0a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 10:43:19 +0100 Subject: [PATCH 20/37] tweak notation a bit more; add comments --- src/Algebra/Bundles/Free/Magma.agda | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 8ebcf4e979..2e8f4df334 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -153,7 +153,7 @@ module FreeMagma {c} (A : Set c) where freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } ------------------------------------------------------------------------ --- Eval, as the unique fold ⟦_⟧ over PreFreeMagma A +-- Eval, as the unique fold ⟦_⟧_ over PreFreeMagma A module Eval {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where @@ -165,6 +165,9 @@ module Eval {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where ⟦ var a ⟧ η = η a ⟦ s ∙ t ⟧ η = ⟦ s ⟧ η ∙ᴹ ⟦ t ⟧ η +------------------------------------------------------------------------ +-- Any Magma *is* an algebra for the PreFreeMagma Functor + module Alg {m ℓm} (𝓜 : Magma m ℓm) where open Magma 𝓜 renaming (setoid to setoidᴹ; Carrier to M) @@ -174,6 +177,9 @@ module Alg {m ℓm} (𝓜 : Magma m ℓm) where algᴹ : PreFreeMagma M → M algᴹ t = ⟦ t ⟧ id +------------------------------------------------------------------------ +-- Properties of ⟦_⟧_ + module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where open Setoid 𝓐 renaming (Carrier to A; _≈_ to _≈ᴬ_) From 86ba4715763230362357c96b70bf9fd2555af5e6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 11:06:19 +0100 Subject: [PATCH 21/37] moved `Set` construction up --- src/Algebra/Bundles/Free/Magma.agda | 80 ++++++++++++++++------------- 1 file changed, 43 insertions(+), 37 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 2e8f4df334..2527d3f14b 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -74,6 +74,49 @@ PreFreeTheorySyntax R = PreFreeMagmaTheory where open PreFreeTheory R syntax PreFreeTheorySyntax R m n = m ≈[ R ] n + +------------------------------------------------------------------------ +-- Free algebra on a Set +{- + in the propositional case, we can immediately define the following + but how best to organise this under the Algebra.Bundles.Free hierarchy? + e.g. should we distinguish Free.Magma.Setoid from Free.Magma.Propositional? +-} + +module FreeMagma {c} (A : Set c) where + + private Carrier = PreFreeMagma A + + _≈_ : Rel Carrier c + m ≈ n = m ≈[ _≡_ ] n + + open PreFreeTheory {A = A} _≡_ + + ≈⇒≡ : ∀ {m n} → m ≈ n → m ≡ n + ≈⇒≡ (var ≡-refl) = ≡-refl + ≈⇒≡ (eq₁ ∙ eq₂) = cong₂ _∙_ (≈⇒≡ eq₁) (≈⇒≡ eq₂) + + refl : Reflexive _≈_ + refl {var _} = var ≡-refl + refl {_ ∙ _} = refl ∙ refl + + ≡⇒≈ : ∀ {m n} → m ≡ n → m ≈ n + ≡⇒≈ ≡-refl = refl + + rawFreeMagma : RawMagma c c + rawFreeMagma = record { Carrier = Carrier ; _≈_ = _≡_ ; _∙_ = _∙_ } + + open Strs {A = Carrier} _≡_ + + isMagma : IsMagma _∙_ + isMagma = record { isEquivalence = ≡-isEquivalence ; ∙-cong = cong₂ _∙_ } + + freeMagma : Magma c c + freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } + +------------------------------------------------------------------------ +-- Extending to a Setoid + module PreservesEquivalence {c ℓ} {A : Set c} (R : Rel A ℓ) where open PreFreeTheory R @@ -115,43 +158,6 @@ module FreeMagmaOn {c ℓ} (S : Setoid c ℓ) where freeMagma : Magma c (c ⊔ ℓ) freeMagma = record { Carrier = PreFreeMagma A; _≈_ = _≈R_ ; _∙_ = _∙_ ; isMagma = isMagma } -{- in the propositional case, we can immediately define the following - but how best to organise this under the Algebra.Bundles.Free hierarchy? -} - ------------------------------------------------------------------------- --- Free algebra on a Set - -module FreeMagma {c} (A : Set c) where - - private Carrier = PreFreeMagma A - - _≈_ : Rel Carrier c - m ≈ n = m ≈[ _≡_ ] n - - open PreFreeTheory {A = A} _≡_ - - ≈⇒≡ : ∀ {m n} → m ≈ n → m ≡ n - ≈⇒≡ (var ≡-refl) = ≡-refl - ≈⇒≡ (eq₁ ∙ eq₂) = cong₂ _∙_ (≈⇒≡ eq₁) (≈⇒≡ eq₂) - - refl : Reflexive _≈_ - refl {var _} = var ≡-refl - refl {_ ∙ _} = refl ∙ refl - - ≡⇒≈ : ∀ {m n} → m ≡ n → m ≈ n - ≡⇒≈ ≡-refl = refl - - rawFreeMagma : RawMagma c c - rawFreeMagma = record { Carrier = Carrier ; _≈_ = _≡_ ; _∙_ = _∙_ } - - open Strs {A = Carrier} _≡_ - - isMagma : IsMagma _∙_ - isMagma = record { isEquivalence = ≡-isEquivalence ; ∙-cong = cong₂ _∙_ } - - freeMagma : Magma c c - freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } - ------------------------------------------------------------------------ -- Eval, as the unique fold ⟦_⟧_ over PreFreeMagma A From 5d9bb28245e14c065d0cac67511be7518920db9a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Apr 2023 11:35:24 +0100 Subject: [PATCH 22/37] =?UTF-8?q?added=20`alg=E1=B4=B9-isMagmaHomomorphism?= =?UTF-8?q?`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Bundles/Free/Magma.agda | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 2527d3f14b..85fb7cbcf0 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -242,6 +242,21 @@ module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) w (h s) ∙ᴹ (h t) ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ ⟦ s ⟧ᴹ ∙ᴹ (⟦ t ⟧ᴹ) ∎ +-- immediate corollary + +module _ {m ℓm} (𝓜 : Magma m ℓm) where + + open Magma 𝓜 renaming (setoid to setoidᴹ; rawMagma to rawMagmaᴹ) + + open Alg 𝓜 + + open Magma (FreeMagmaOn.freeMagma setoidᴹ) + + open Properties setoidᴹ 𝓜 + + algᴹ-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma rawMagmaᴹ algᴹ + algᴹ-isMagmaHomomorphism = isMagmaHomomorphism (record { cong = id }) + ------------------------------------------------------------------------ -- Monad instance: TODO From b91ef55902b9ccf02cd354626734db30ddc4c89a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 29 Apr 2023 13:15:16 +0100 Subject: [PATCH 23/37] radical refactoring; added `map` for lifting `FreeMonad` from `Setoid`s to `SetoidHomomorphism`s --- src/Algebra/Bundles/Free/Magma.agda | 289 +++++++++++++++------------- 1 file changed, 159 insertions(+), 130 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 85fb7cbcf0..75c2de2a73 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -9,11 +9,13 @@ module Algebra.Bundles.Free.Magma where open import Algebra.Core -import Algebra.Definitions as Defs using (Congruent₂) -import Algebra.Structures as Strs using (IsMagma) +import Algebra.Definitions as Definitions using (Congruent₂) +import Algebra.Structures as Structures using (IsMagma) open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) open import Algebra.Bundles using (Magma) open import Algebra.Bundles.Raw using (RawMagma) +open import Effect.Functor +open import Effect.Monad open import Function.Base using (id; _∘_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Morphism using (IsRelHomomorphism) @@ -21,30 +23,39 @@ open import Level using (Level; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) +open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) open import Relation.Binary.PropositionalEquality using (_≡_; cong₂) renaming (refl to ≡-refl; isEquivalence to ≡-isEquivalence) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +private + variable + a ℓa b ℓb c ℓ m ℓm : Level + A : Set a + B : Set b + C : Set c + 𝓐 : Setoid a ℓa + 𝓑 : Setoid b ℓb ------------------------------------------------------------------------ --- 'pre'-free algebra +-- Syntax: 'pre'-free algebra -infixl 7 _∙_ +module Syntax where -data PreFreeMagma {a} (A : Set a) : Set a where + infixl 7 _∙_ - var : A → PreFreeMagma A - _∙_ : Op₂ (PreFreeMagma A) + data Syntax (A : Set a) : Set a where -module _ {a b} {A : Set a} {B : Set b} where + var : A → Syntax A + _∙_ : Op₂ (Syntax A) - map : (A → B) → PreFreeMagma A → PreFreeMagma B +-- Functor instance + + map : (A → B) → Syntax A → Syntax B map f (var a) = var (f a) map f (s ∙ t) = (map f s) ∙ (map f t) -module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where - - map-id : ∀ (t : PreFreeMagma A) → map id t ≡ t + map-id : ∀ (t : Syntax A) → map id t ≡ t map-id (var a) = ≡-refl map-id (s ∙ t) = cong₂ _∙_ (map-id s) (map-id t) @@ -52,28 +63,52 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where map-∘ g f (var a) = ≡-refl map-∘ g f (s ∙ t) = cong₂ _∙_ (map-∘ g f s) (map-∘ g f t) ------------------------------------------------------------------------- --- Functor, RawMonad instance: TODO + syntaxRawFunctor : RawFunctor (Syntax {a}) + syntaxRawFunctor = record { _<$>_ = map } + +-- Monad instance + + bind : Syntax A → (A → Syntax B) → Syntax B + bind (var x) h = h x + bind (s ∙ t) h = bind s h ∙ bind t h + + syntaxRawMonad : RawMonad (Syntax {a}) + syntaxRawMonad = mkRawMonad Syntax var bind ------------------------------------------------------------------------ -- parametrised 'equational' theory over the 'pre'-free algebra -module PreFreeTheory {c ℓ} {A : Set c} (R : Rel A ℓ) where +module EquationalTheory {A : Set a} (R : Rel A ℓ) where - data PreFreeMagmaTheory : Rel (PreFreeMagma A) (c ⊔ ℓ) + open Syntax - open Defs PreFreeMagmaTheory + infix 4 _≈_ - data PreFreeMagmaTheory where + data _≈_ : Rel (Syntax A) (a ⊔ ℓ) - var : ∀ {a b} → (R a b) → PreFreeMagmaTheory (var a) (var b) + open Definitions _≈_ + + data _≈_ where + + var : {a b : A} → (R a b) → _≈_ (var a) (var b) _∙_ : Congruent₂ _∙_ -PreFreeTheorySyntax : ∀ {c ℓ} {A : Set c} (R : Rel A ℓ) → Rel (PreFreeMagma A) (c ⊔ ℓ) -PreFreeTheorySyntax R = PreFreeMagmaTheory where open PreFreeTheory R + refl : Reflexive R → Reflexive _≈_ + refl r {var _} = var r + refl r {_ ∙ _} = (refl r) ∙ (refl r) -syntax PreFreeTheorySyntax R m n = m ≈[ R ] n + sym : Symmetric R → Symmetric _≈_ + sym s (var r) = var (s r) + sym s (r₁ ∙ r₂) = sym s r₁ ∙ sym s r₂ + trans : Transitive R → Transitive _≈_ + trans t (var r) (var s) = var (t r s) + trans t (r₁ ∙ r₂) (s₁ ∙ s₂) = trans t r₁ s₁ ∙ trans t r₂ s₂ + + preservesEquivalence : IsEquivalence R → IsEquivalence _≈_ + preservesEquivalence isEq = record + { refl = refl Eq.refl ; sym = sym Eq.sym ; trans = trans Eq.trans } + where module Eq = IsEquivalence isEq ------------------------------------------------------------------------ -- Free algebra on a Set @@ -83,179 +118,173 @@ syntax PreFreeTheorySyntax R m n = m ≈[ R ] n e.g. should we distinguish Free.Magma.Setoid from Free.Magma.Propositional? -} -module FreeMagma {c} (A : Set c) where +module FreeRawMagma (A : Set a) where - private Carrier = PreFreeMagma A + open Syntax - _≈_ : Rel Carrier c - m ≈ n = m ≈[ _≡_ ] n + open EquationalTheory {A = A} _≡_ - open PreFreeTheory {A = A} _≡_ +-- inductively-defined equational theory conincides with _≡_ ≈⇒≡ : ∀ {m n} → m ≈ n → m ≡ n ≈⇒≡ (var ≡-refl) = ≡-refl ≈⇒≡ (eq₁ ∙ eq₂) = cong₂ _∙_ (≈⇒≡ eq₁) (≈⇒≡ eq₂) - refl : Reflexive _≈_ - refl {var _} = var ≡-refl - refl {_ ∙ _} = refl ∙ refl - ≡⇒≈ : ∀ {m n} → m ≡ n → m ≈ n - ≡⇒≈ ≡-refl = refl + ≡⇒≈ ≡-refl = refl ≡-refl - rawFreeMagma : RawMagma c c - rawFreeMagma = record { Carrier = Carrier ; _≈_ = _≡_ ; _∙_ = _∙_ } + freeRawMagma : RawMagma a a + freeRawMagma = record { Carrier = Syntax A ; _≈_ = _≡_ ; _∙_ = _∙_ } - open Strs {A = Carrier} _≡_ + open Structures {A = Syntax A} _≡_ isMagma : IsMagma _∙_ isMagma = record { isEquivalence = ≡-isEquivalence ; ∙-cong = cong₂ _∙_ } - freeMagma : Magma c c - freeMagma = record { RawMagma rawFreeMagma ; isMagma = isMagma } - ------------------------------------------------------------------------- --- Extending to a Setoid - -module PreservesEquivalence {c ℓ} {A : Set c} (R : Rel A ℓ) where - - open PreFreeTheory R - - _≈R_ = λ m n → m ≈[ R ] n - - refl : Reflexive R → Reflexive _≈R_ - refl r {var _} = var r - refl r {_ ∙ _} = (refl r) ∙ (refl r) - - sym : Symmetric R → Symmetric _≈R_ - sym s (var r) = var (s r) - sym s (r₁ ∙ r₂) = sym s r₁ ∙ sym s r₂ - - trans : Transitive R → Transitive _≈R_ - trans t (var r) (var s) = var (t r s) - trans t (r₁ ∙ r₂) (s₁ ∙ s₂) = trans t r₁ s₁ ∙ trans t r₂ s₂ - - preservesEquivalence : IsEquivalence R → IsEquivalence _≈R_ - preservesEquivalence isEq = record { refl = refl r ; sym = sym s ; trans = trans t } - where open IsEquivalence isEq renaming (refl to r; sym to s; trans to t) + freeMagma : Magma a a + freeMagma = record { RawMagma freeRawMagma ; isMagma = isMagma } ------------------------------------------------------------------------ -- Free algebra on a Setoid -module FreeMagmaOn {c ℓ} (S : Setoid c ℓ) where +module FreeMagma (𝓐 : Setoid a ℓa) where - open Setoid S renaming (Carrier to A; isEquivalence to isEq) + open Setoid 𝓐 renaming (isEquivalence to isEqᴬ; _≈_ to _≈ᴬ_) - open PreFreeTheory _≈_ public + open Syntax - open PreservesEquivalence _≈_ + open EquationalTheory _≈ᴬ_ public + renaming (_≈_ to _≈ᵀ_) hiding (refl; sym; trans) - open Strs _≈R_ + open Structures _≈ᵀ_ isMagma : IsMagma _∙_ - isMagma = record { isEquivalence = preservesEquivalence isEq ; ∙-cong = _∙_ } + isMagma = record { isEquivalence = preservesEquivalence isEqᴬ ; ∙-cong = _∙_ } - freeMagma : Magma c (c ⊔ ℓ) - freeMagma = record { Carrier = PreFreeMagma A; _≈_ = _≈R_ ; _∙_ = _∙_ ; isMagma = isMagma } + freeMagma : Magma a (a ⊔ ℓa) + freeMagma = record { Carrier = Syntax Carrier; _≈_ = _≈ᵀ_ ; _∙_ = _∙_ ; isMagma = isMagma } ------------------------------------------------------------------------- --- Eval, as the unique fold ⟦_⟧_ over PreFreeMagma A +-- reexport some substructure -module Eval {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where + open Magma freeMagma public using (rawMagma; Carrier; _≈_) + +------------------------------------------------------------------------ +-- Semantics: in terms of concrete Magma instances - open Setoid 𝓐 renaming (Carrier to A) +module _ (𝓜 : Magma m ℓm) where - open Magma 𝓜 renaming (Carrier to M; _∙_ to _∙ᴹ_) + open Magma 𝓜 + renaming (Carrier to UM; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ + ; setoid to setoidᴹ; rawMagma to rawMagmaᴹ + ; isMagma to isMagmaᴹ) + open ≈-Reasoning setoidᴹ - ⟦_⟧_ : PreFreeMagma A → (A → M) → M - ⟦ var a ⟧ η = η a - ⟦ s ∙ t ⟧ η = ⟦ s ⟧ η ∙ᴹ ⟦ t ⟧ η + open Syntax ------------------------------------------------------------------------ --- Any Magma *is* an algebra for the PreFreeMagma Functor +-- Eval, as the unique fold ⟦_⟧_ over Syntax -module Alg {m ℓm} (𝓜 : Magma m ℓm) where + module Eval (𝓐 : Setoid a ℓa) where - open Magma 𝓜 renaming (setoid to setoidᴹ; Carrier to M) + open Setoid 𝓐 renaming (Carrier to UA) - open Eval setoidᴹ 𝓜 + ⟦_⟧_ : Syntax UA → (UA → UM) → UM + ⟦ var a ⟧ η = η a + ⟦ s ∙ t ⟧ η = ⟦ s ⟧ η ∙ᴹ ⟦ t ⟧ η - algᴹ : PreFreeMagma M → M - algᴹ t = ⟦ t ⟧ id +------------------------------------------------------------------------ +-- Any Magma *is* an algebra for the Syntax Functor + + alg : Syntax UM → UM + alg t = ⟦ t ⟧ id where open Eval setoidᴹ ------------------------------------------------------------------------ -- Properties of ⟦_⟧_ -module Properties {a ℓa m ℓm} (𝓐 : Setoid a ℓa) (𝓜 : Magma m ℓm) where + module Properties {a ℓa} (𝓐 : Setoid a ℓa) where - open Setoid 𝓐 renaming (Carrier to A; _≈_ to _≈ᴬ_) + open Setoid 𝓐 renaming (Carrier to UA; _≈_ to _≈ᴬ_) - open Magma 𝓜 - renaming (Carrier to M; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ - ; setoid to setoidᴹ; rawMagma to rawMagmaᴹ; refl to reflᴹ - ; isMagma to isMagmaᴹ) + open Eval 𝓐 public - open Eval 𝓐 𝓜 + open FreeMagma 𝓐 renaming (Carrier to UFA) - open Alg 𝓜 + module Existence {η : UA → UM} (hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ η) where - open FreeMagmaOn 𝓐 + ⟦_⟧ᴹ : UFA → UM + ⟦_⟧ᴹ = ⟦_⟧ η - open Magma freeMagma renaming (rawMagma to rawMagmaᴬ; Carrier to FA) + open Structures _≈ᴹ_ + open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) + open IsRelHomomorphism hom-η renaming (cong to cong-η) - module _ {η : A → M} (hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ η) where + cong-⟦_⟧ : ∀ {s t} → s ≈ t → ⟦ s ⟧ᴹ ≈ᴹ ⟦ t ⟧ᴹ + cong-⟦ var r ⟧ = cong-η r + cong-⟦ s ∙ t ⟧ = congᴹ cong-⟦ s ⟧ cong-⟦ t ⟧ - ⟦_⟧ᴹ : FA → M - ⟦_⟧ᴹ = ⟦_⟧ η + isRelHomomorphism : IsRelHomomorphism _≈_ _≈ᴹ_ ⟦_⟧ᴹ + isRelHomomorphism = record { cong = cong-⟦_⟧ } - open Strs _≈ᴹ_ - open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) - open IsRelHomomorphism hom-η renaming (cong to cong-η) + isMagmaHomomorphism : IsMagmaHomomorphism rawMagma rawMagmaᴹ ⟦_⟧ᴹ + isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism + ; homo = λ s t → begin ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ } - cong : ∀ {s t} → s ≈ t → ⟦ s ⟧ᴹ ≈ᴹ ⟦ t ⟧ᴹ - cong (var r) = cong-η r - cong (s ∙ t) = congᴹ (cong s) (cong t) + unfold-⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ᴹ ≈ᴹ alg (map η t) + unfold-⟦ var a ⟧ᴹ = begin η a ∎ + unfold-⟦ s ∙ t ⟧ᴹ = congᴹ unfold-⟦ s ⟧ᴹ unfold-⟦ t ⟧ᴹ - isRelHomomorphism : IsRelHomomorphism _≈_ _≈ᴹ_ ⟦_⟧ᴹ - isRelHomomorphism = record { cong = cong } + module Uniqueness {h : UFA → UM} + (isHom : IsMagmaHomomorphism rawMagma rawMagmaᴹ h) + (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) where - isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ ⟦_⟧ᴹ - isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism - ; homo = λ _ _ → reflᴹ - } + isUnique⟦_⟧ᴹ : ∀ t → h t ≈ᴹ ⟦ t ⟧ᴹ + isUnique⟦ var a ⟧ᴹ = h∘var≈ᴹη a + isUnique⟦ s ∙ t ⟧ᴹ = begin + h (s Syntax.∙ t) ≈⟨ homo s t ⟩ + h s ∙ᴹ h t ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ + ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ where open IsMagmaHomomorphism isHom - unfold-⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ᴹ ≈ᴹ algᴹ (map η t) - unfold-⟦ var a ⟧ᴹ = reflᴹ - unfold-⟦ s ∙ t ⟧ᴹ = congᴹ unfold-⟦ s ⟧ᴹ unfold-⟦ t ⟧ᴹ +-- immediate corollary - module _ {h : FA → M} (isHom : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴹ h) - (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) where + open FreeMagma setoidᴹ + open Properties setoidᴹ - open IsMagmaHomomorphism isHom + alg-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma rawMagmaᴹ alg + alg-isMagmaHomomorphism = Existence.isMagmaHomomorphism (record { cong = id }) - open ≈-Reasoning setoidᴹ +------------------------------------------------------------------------ +-- Functoriality of FreeMonad wrt Setoid homomorphisms - isUnique⟦_⟧ᴹ : ∀ t → h t ≈ᴹ ⟦ t ⟧ᴹ - isUnique⟦ var a ⟧ᴹ = h∘var≈ᴹη a - isUnique⟦ s ∙ t ⟧ᴹ = begin - h (s PreFreeMagma.∙ t) ≈⟨ homo s t ⟩ - (h s) ∙ᴹ (h t) ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ - ⟦ s ⟧ᴹ ∙ᴹ (⟦ t ⟧ᴹ) ∎ +module FreeMonadFunctor (𝓗 : SetoidHomomorphism 𝓐 𝓑) where --- immediate corollary + open Setoid 𝓐 renaming (Carrier to UA; _≈_ to _≈ᴬ_) + open Setoid 𝓑 renaming (Carrier to UB; _≈_ to _≈ᴮ_) + + open FreeMagma 𝓐 + renaming (freeMagma to freeMagmaᴬ; rawMagma to rawMagmaᴬ + ; Carrier to UFA; _≈_ to _≈ᵀᴬ_; isMagma to isMagmaᴬ) -module _ {m ℓm} (𝓜 : Magma m ℓm) where + open FreeMagma 𝓑 + renaming (freeMagma to freeMagmaᴮ; rawMagma to rawMagmaᴮ + ; Carrier to UFB; _≈_ to _≈ᵀᴮ_; isMagma to isMagmaᴮ) - open Magma 𝓜 renaming (setoid to setoidᴹ; rawMagma to rawMagmaᴹ) + open Properties freeMagmaᴮ 𝓐 - open Alg 𝓜 + open SetoidHomomorphism 𝓗 - open Magma (FreeMagmaOn.freeMagma setoidᴹ) + private + η : UA → UFB + η = Syntax.var ∘ ⟦_⟧ - open Properties setoidᴹ 𝓜 + hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᵀᴮ_ η + hom-η = record { cong = EquationalTheory.var ∘ congᴬᴮ } + where open IsRelHomomorphism isRelHomomorphism renaming (cong to congᴬᴮ) - algᴹ-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma rawMagmaᴹ algᴹ - algᴹ-isMagmaHomomorphism = isMagmaHomomorphism (record { cong = id }) + map : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴮ _ + map = Existence.isMagmaHomomorphism hom-η + +------------------------------------------------------------------------ +-- Functoriality of FreeMonadFunctor.map : TODO ------------------------------------------------------------------------ -- Monad instance: TODO From 0e045133a4e063fce273304567275f893c0b491d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 29 Apr 2023 13:55:03 +0100 Subject: [PATCH 24/37] cosmetic --- src/Algebra/Bundles/Free/Magma.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 75c2de2a73..729c0189c0 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -90,7 +90,7 @@ module EquationalTheory {A : Set a} (R : Rel A ℓ) where data _≈_ where - var : {a b : A} → (R a b) → _≈_ (var a) (var b) + var : {a b : A} → (R a b) → var a ≈ var b _∙_ : Congruent₂ _∙_ refl : Reflexive R → Reflexive _≈_ From 3de4bd8ac2bf5d614c0b1bd6eec4dbdfdb9ee0d6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 29 Apr 2023 14:04:08 +0100 Subject: [PATCH 25/37] typo --- src/Algebra/Bundles/Free/Magma.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 729c0189c0..78cd3a7aca 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -284,7 +284,7 @@ module FreeMonadFunctor (𝓗 : SetoidHomomorphism 𝓐 𝓑) where map = Existence.isMagmaHomomorphism hom-η ------------------------------------------------------------------------ --- Functoriality of FreeMonadFunctor.map : TODO +-- Functoriality of FreeMagmaFunctor.map : TODO ------------------------------------------------------------------------ -- Monad instance: TODO From bfc920b311816a43815464c9e03df85acdfa116c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 29 Apr 2023 14:07:41 +0100 Subject: [PATCH 26/37] more typos --- src/Algebra/Bundles/Free/Magma.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 78cd3a7aca..3f0ce02df4 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -194,7 +194,7 @@ module _ (𝓜 : Magma m ℓm) where ------------------------------------------------------------------------ -- Any Magma *is* an algebra for the Syntax Functor - + alg : Syntax UM → UM alg t = ⟦ t ⟧ id where open Eval setoidᴹ @@ -253,9 +253,9 @@ module _ (𝓜 : Magma m ℓm) where alg-isMagmaHomomorphism = Existence.isMagmaHomomorphism (record { cong = id }) ------------------------------------------------------------------------ --- Functoriality of FreeMonad wrt Setoid homomorphisms +-- Functoriality of FreeMagma wrt Setoid homomorphisms -module FreeMonadFunctor (𝓗 : SetoidHomomorphism 𝓐 𝓑) where +module FreeMagmaFunctor (𝓗 : SetoidHomomorphism 𝓐 𝓑) where open Setoid 𝓐 renaming (Carrier to UA; _≈_ to _≈ᴬ_) open Setoid 𝓑 renaming (Carrier to UB; _≈_ to _≈ᴮ_) From 1a8074d24343f6ab7929a1b35d4dfc1ad793f826 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 30 Apr 2023 13:26:22 +0100 Subject: [PATCH 27/37] corollary to uniqueness: naturality of `alg` --- src/Algebra/Bundles/Free/Magma.agda | 73 ++++++++++++++++++++++++----- 1 file changed, 61 insertions(+), 12 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 3f0ce02df4..ad177d1d29 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -9,11 +9,12 @@ module Algebra.Bundles.Free.Magma where open import Algebra.Core +open import Algebra.Bundles using (Magma) +open import Algebra.Bundles.Raw using (RawMagma) import Algebra.Definitions as Definitions using (Congruent₂) import Algebra.Structures as Structures using (IsMagma) open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) -open import Algebra.Bundles using (Magma) -open import Algebra.Bundles.Raw using (RawMagma) +import Algebra.Morphism.Construct.Composition as Compose open import Effect.Functor open import Effect.Monad open import Function.Base using (id; _∘_) @@ -30,13 +31,14 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable - a ℓa b ℓb c ℓ m ℓm : Level + ℓ a ℓa b ℓb c ℓc m ℓm n ℓn : Level A : Set a B : Set b C : Set c 𝓐 : Setoid a ℓa 𝓑 : Setoid b ℓb - + 𝓒 : Setoid c ℓc + ------------------------------------------------------------------------ -- Syntax: 'pre'-free algebra @@ -244,6 +246,18 @@ module _ (𝓜 : Magma m ℓm) where h s ∙ᴹ h t ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ where open IsMagmaHomomorphism isHom + module Corollary {h k : UFA → UM} + (h-isHom : IsMagmaHomomorphism rawMagma rawMagmaᴹ h) + (k-isHom : IsMagmaHomomorphism rawMagma rawMagmaᴹ k) + (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) + (k∘var≈ᴹη : ∀ a → k (var a) ≈ᴹ η a) where + + isUnique : ∀ t → h t ≈ᴹ k t + isUnique t = begin h t ≈⟨ hU⟦ t ⟧ᴹ ⟩ ⟦ t ⟧ᴹ ≈˘⟨ kU⟦ t ⟧ᴹ ⟩ k t ∎ + where + open Uniqueness h-isHom h∘var≈ᴹη renaming (isUnique⟦_⟧ᴹ to hU⟦_⟧ᴹ) + open Uniqueness k-isHom k∘var≈ᴹη renaming (isUnique⟦_⟧ᴹ to kU⟦_⟧ᴹ) + -- immediate corollary open FreeMagma setoidᴹ @@ -272,16 +286,51 @@ module FreeMagmaFunctor (𝓗 : SetoidHomomorphism 𝓐 𝓑) where open SetoidHomomorphism 𝓗 - private - η : UA → UFB - η = Syntax.var ∘ ⟦_⟧ + η : UA → UFB + η = Syntax.var ∘ ⟦_⟧ + + hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᵀᴮ_ η + hom-η = record { cong = EquationalTheory.var ∘ congᴬᴮ } + where open IsRelHomomorphism isRelHomomorphism renaming (cong to congᴬᴮ) + + open Existence - hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᵀᴮ_ η - hom-η = record { cong = EquationalTheory.var ∘ congᴬᴮ } - where open IsRelHomomorphism isRelHomomorphism renaming (cong to congᴬᴮ) + map : UFA → UFB + map = ⟦_⟧ᴹ hom-η - map : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴮ _ - map = Existence.isMagmaHomomorphism hom-η + map-isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴮ map + map-isMagmaHomomorphism = isMagmaHomomorphism hom-η + +------------------------------------------------------------------------ +-- Naturality of alg + +module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where + open Magma 𝓜 renaming (rawMagma to M; setoid to setoidᴹ; Carrier to UM; _≈_ to _≈ᴹ_) + open Magma 𝓝 renaming (rawMagma to N; setoid to setoidᴺ; Carrier to UN; _≈_ to _≈ᴺ_; refl to reflᴺ; trans to transᴺ) + module _ (𝓗 : SetoidHomomorphism setoidᴹ setoidᴺ) where + open SetoidHomomorphism 𝓗 + open FreeMagmaFunctor 𝓗 + open FreeMagma setoidᴹ renaming (freeMagma to freeMagmaᴹ; rawMagma to FM; Carrier to UFM) + algᴹ = alg 𝓜 + algᴹ-isMagmaHomomorphism = alg-isMagmaHomomorphism 𝓜 + algᴺ = alg 𝓝 + algᴺ-isMagmaHomomorphism = alg-isMagmaHomomorphism 𝓝 + module _ (hom : IsMagmaHomomorphism M N ⟦_⟧) where + + h k : UFM → UN + h = ⟦_⟧ ∘ algᴹ + k = algᴺ ∘ map + + h-hom : IsMagmaHomomorphism FM N h + h-hom = Compose.isMagmaHomomorphism transᴺ algᴹ-isMagmaHomomorphism hom + + k-hom : IsMagmaHomomorphism FM N k + k-hom = Compose.isMagmaHomomorphism transᴺ map-isMagmaHomomorphism algᴺ-isMagmaHomomorphism + + naturality : ∀ t → h t ≈ᴺ k t + naturality = isUnique isRelHomomorphism h-hom k-hom (λ _ → reflᴺ) (λ _ → reflᴺ) + where open Properties.Existence.Corollary 𝓝 setoidᴹ + ------------------------------------------------------------------------ -- Functoriality of FreeMagmaFunctor.map : TODO From eef3d3fa0f99720e1fbcad86be3615f90ffedd38 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 30 Apr 2023 15:12:56 +0100 Subject: [PATCH 28/37] cosmetic renamings; more serious refactoring required --- src/Algebra/Bundles/Free/Magma.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index ad177d1d29..65bcdea72e 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -308,7 +308,7 @@ module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where open Magma 𝓜 renaming (rawMagma to M; setoid to setoidᴹ; Carrier to UM; _≈_ to _≈ᴹ_) open Magma 𝓝 renaming (rawMagma to N; setoid to setoidᴺ; Carrier to UN; _≈_ to _≈ᴺ_; refl to reflᴺ; trans to transᴺ) module _ (𝓗 : SetoidHomomorphism setoidᴹ setoidᴺ) where - open SetoidHomomorphism 𝓗 + open SetoidHomomorphism 𝓗 renaming (isRelHomomorphism to hom-⟦⟧) open FreeMagmaFunctor 𝓗 open FreeMagma setoidᴹ renaming (freeMagma to freeMagmaᴹ; rawMagma to FM; Carrier to UFM) algᴹ = alg 𝓜 @@ -328,7 +328,7 @@ module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where k-hom = Compose.isMagmaHomomorphism transᴺ map-isMagmaHomomorphism algᴺ-isMagmaHomomorphism naturality : ∀ t → h t ≈ᴺ k t - naturality = isUnique isRelHomomorphism h-hom k-hom (λ _ → reflᴺ) (λ _ → reflᴺ) + naturality = isUnique hom-⟦⟧ h-hom k-hom (λ _ → reflᴺ) (λ _ → reflᴺ) where open Properties.Existence.Corollary 𝓝 setoidᴹ From d5f2a809e36d2c047f0b4101077b4b6ffb26bc9b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 May 2023 10:09:34 +0100 Subject: [PATCH 29/37] added `MagmaHomomorphism` bundle; another major refactoring --- src/Algebra/Bundles/Free/Magma.agda | 299 +++++++++++++++------------- 1 file changed, 166 insertions(+), 133 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 65bcdea72e..cfc9886107 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -20,24 +20,44 @@ open import Effect.Monad open import Function.Base using (id; _∘_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Morphism using (IsRelHomomorphism) -open import Level using (Level; _⊔_) +open import Level using (Level; suc; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary using (Setoid; IsEquivalence; Reflexive; Symmetric; Transitive) open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) +import Relation.Binary.Morphism.Construct.Identity as Identity +import Relation.Binary.Morphism.Construct.Composition as Compose open import Relation.Binary.PropositionalEquality using (_≡_; cong₂) renaming (refl to ≡-refl; isEquivalence to ≡-isEquivalence) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable - ℓ a ℓa b ℓb c ℓc m ℓm n ℓn : Level + a ℓa b ℓb c ℓ m ℓm n ℓn : Level A : Set a B : Set b C : Set c - 𝓐 : Setoid a ℓa - 𝓑 : Setoid b ℓb - 𝓒 : Setoid c ℓc + +------------------------------------------------------------------------ +-- Morphisms between Magmas: belongs in its own place +-- Algebra.Morphism.Bundles +-- open import Algebra.Morphism.Bundles using (MagmaHomomorphism) +------------------------------------------------------------------------ + +record MagmaHomomorphism (𝓐 : Magma a ℓa) (𝓑 : Magma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where + + open Magma 𝓐 renaming (rawMagma to rawMagmaᴬ; setoid to setoidᴬ; Carrier to UA) + open Magma 𝓑 renaming (rawMagma to rawMagmaᴮ; setoid to setoidᴮ; Carrier to UB) + + field + ⟦_⟧ : UA → UB + + isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴮ ⟦_⟧ + + open IsMagmaHomomorphism isMagmaHomomorphism public + + setoidHomomorphism : SetoidHomomorphism setoidᴬ setoidᴮ + setoidHomomorphism = record { ⟦_⟧ = ⟦_⟧ ; isRelHomomorphism = isRelHomomorphism } ------------------------------------------------------------------------ -- Syntax: 'pre'-free algebra @@ -80,7 +100,7 @@ module Syntax where ------------------------------------------------------------------------ -- parametrised 'equational' theory over the 'pre'-free algebra -module EquationalTheory {A : Set a} (R : Rel A ℓ) where +module EquationalTheory {A : Set a} (_≈ᴬ_ : Rel A ℓ) where open Syntax @@ -92,26 +112,29 @@ module EquationalTheory {A : Set a} (R : Rel A ℓ) where data _≈_ where - var : {a b : A} → (R a b) → var a ≈ var b + var : {a b : A} → a ≈ᴬ b → var a ≈ var b _∙_ : Congruent₂ _∙_ - refl : Reflexive R → Reflexive _≈_ + refl : Reflexive _≈ᴬ_ → Reflexive _≈_ refl r {var _} = var r refl r {_ ∙ _} = (refl r) ∙ (refl r) - sym : Symmetric R → Symmetric _≈_ - sym s (var r) = var (s r) - sym s (r₁ ∙ r₂) = sym s r₁ ∙ sym s r₂ + sym : Symmetric _≈ᴬ_ → Symmetric _≈_ + sym s (var s₀) = var (s s₀) + sym s (s₁ ∙ s₂) = sym s s₁ ∙ sym s s₂ - trans : Transitive R → Transitive _≈_ - trans t (var r) (var s) = var (t r s) + trans : Transitive _≈ᴬ_ → Transitive _≈_ + trans t (var r₀) (var s₀) = var (t r₀ s₀) trans t (r₁ ∙ r₂) (s₁ ∙ s₂) = trans t r₁ s₁ ∙ trans t r₂ s₂ - preservesEquivalence : IsEquivalence R → IsEquivalence _≈_ + preservesEquivalence : IsEquivalence _≈ᴬ_ → IsEquivalence _≈_ preservesEquivalence isEq = record { refl = refl Eq.refl ; sym = sym Eq.sym ; trans = trans Eq.trans } where module Eq = IsEquivalence isEq + varIsRelHomomorphism : IsRelHomomorphism _≈ᴬ_ _≈_ var + varIsRelHomomorphism = record { cong = var } + ------------------------------------------------------------------------ -- Free algebra on a Set {- @@ -166,21 +189,19 @@ module FreeMagma (𝓐 : Setoid a ℓa) where freeMagma : Magma a (a ⊔ ℓa) freeMagma = record { Carrier = Syntax Carrier; _≈_ = _≈ᵀ_ ; _∙_ = _∙_ ; isMagma = isMagma } --- reexport some substructure +-- re-export some substructure + + open Magma freeMagma public using (rawMagma; setoid; Carrier; _≈_) - open Magma freeMagma public using (rawMagma; Carrier; _≈_) + varSetoidHomomorphism : SetoidHomomorphism 𝓐 setoid + varSetoidHomomorphism = record { ⟦_⟧ = var; isRelHomomorphism = varIsRelHomomorphism } ------------------------------------------------------------------------ -- Semantics: in terms of concrete Magma instances module _ (𝓜 : Magma m ℓm) where - open Magma 𝓜 - renaming (Carrier to UM; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ - ; setoid to setoidᴹ; rawMagma to rawMagmaᴹ - ; isMagma to isMagmaᴹ) - open ≈-Reasoning setoidᴹ - + open Magma 𝓜 renaming (setoid to setoidᴹ; Carrier to UM; _∙_ to _∙ᴹ_) open Syntax ------------------------------------------------------------------------ @@ -196,144 +217,156 @@ module _ (𝓜 : Magma m ℓm) where ------------------------------------------------------------------------ -- Any Magma *is* an algebra for the Syntax Functor - + alg : Syntax UM → UM alg t = ⟦ t ⟧ id where open Eval setoidᴹ ------------------------------------------------------------------------ --- Properties of ⟦_⟧_ - - module Properties {a ℓa} (𝓐 : Setoid a ℓa) where - - open Setoid 𝓐 renaming (Carrier to UA; _≈_ to _≈ᴬ_) - - open Eval 𝓐 public - - open FreeMagma 𝓐 renaming (Carrier to UFA) +-- ⟦_⟧_ defines the (unique) lifting of Setoid homomorphisms to Magma homomorphisms - module Existence {η : UA → UM} (hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᴹ_ η) where +module LeftAdjoint {𝓐 : Setoid a ℓa} (𝓜 : Magma m ℓm) + (𝓗 : SetoidHomomorphism 𝓐 (Magma.setoid 𝓜)) where - ⟦_⟧ᴹ : UFA → UM - ⟦_⟧ᴹ = ⟦_⟧ η - - open Structures _≈ᴹ_ - open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) - open IsRelHomomorphism hom-η renaming (cong to cong-η) - - cong-⟦_⟧ : ∀ {s t} → s ≈ t → ⟦ s ⟧ᴹ ≈ᴹ ⟦ t ⟧ᴹ - cong-⟦ var r ⟧ = cong-η r - cong-⟦ s ∙ t ⟧ = congᴹ cong-⟦ s ⟧ cong-⟦ t ⟧ - - isRelHomomorphism : IsRelHomomorphism _≈_ _≈ᴹ_ ⟦_⟧ᴹ - isRelHomomorphism = record { cong = cong-⟦_⟧ } + open Magma 𝓜 + renaming (Carrier to UM; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ + ; setoid to setoidᴹ; rawMagma to rawMagmaᴹ + ; isMagma to isMagmaᴹ) + open ≈-Reasoning setoidᴹ - isMagmaHomomorphism : IsMagmaHomomorphism rawMagma rawMagmaᴹ ⟦_⟧ᴹ - isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism - ; homo = λ s t → begin ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ } + open Syntax - unfold-⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ᴹ ≈ᴹ alg (map η t) - unfold-⟦ var a ⟧ᴹ = begin η a ∎ - unfold-⟦ s ∙ t ⟧ᴹ = congᴹ unfold-⟦ s ⟧ᴹ unfold-⟦ t ⟧ᴹ + open Setoid 𝓐 renaming (Carrier to UA; _≈_ to _≈ᴬ_) - module Uniqueness {h : UFA → UM} - (isHom : IsMagmaHomomorphism rawMagma rawMagmaᴹ h) - (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) where + open Eval 𝓜 𝓐 public - isUnique⟦_⟧ᴹ : ∀ t → h t ≈ᴹ ⟦ t ⟧ᴹ - isUnique⟦ var a ⟧ᴹ = h∘var≈ᴹη a - isUnique⟦ s ∙ t ⟧ᴹ = begin - h (s Syntax.∙ t) ≈⟨ homo s t ⟩ - h s ∙ᴹ h t ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ - ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ where open IsMagmaHomomorphism isHom + open FreeMagma 𝓐 renaming (setoid to FA; Carrier to UFA) - module Corollary {h k : UFA → UM} - (h-isHom : IsMagmaHomomorphism rawMagma rawMagmaᴹ h) - (k-isHom : IsMagmaHomomorphism rawMagma rawMagmaᴹ k) - (h∘var≈ᴹη : ∀ a → h (var a) ≈ᴹ η a) - (k∘var≈ᴹη : ∀ a → k (var a) ≈ᴹ η a) where + open SetoidHomomorphism 𝓗 renaming (⟦_⟧ to η; isRelHomomorphism to hom-η) - isUnique : ∀ t → h t ≈ᴹ k t - isUnique t = begin h t ≈⟨ hU⟦ t ⟧ᴹ ⟩ ⟦ t ⟧ᴹ ≈˘⟨ kU⟦ t ⟧ᴹ ⟩ k t ∎ - where - open Uniqueness h-isHom h∘var≈ᴹη renaming (isUnique⟦_⟧ᴹ to hU⟦_⟧ᴹ) - open Uniqueness k-isHom k∘var≈ᴹη renaming (isUnique⟦_⟧ᴹ to kU⟦_⟧ᴹ) + module Existence where + + ⟦_⟧ᴹ : UFA → UM + ⟦_⟧ᴹ = ⟦_⟧ η + + open Structures _≈ᴹ_ + open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) + open IsRelHomomorphism hom-η renaming (cong to cong-η) + + private + algᴹ = alg 𝓜 + + unfold-⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ᴹ ≈ᴹ algᴹ (map η t) + unfold-⟦ var a ⟧ᴹ = begin η a ∎ + unfold-⟦ s ∙ t ⟧ᴹ = congᴹ unfold-⟦ s ⟧ᴹ unfold-⟦ t ⟧ᴹ + + cong-⟦_⟧ : ∀ {s t} → s ≈ t → ⟦ s ⟧ᴹ ≈ᴹ ⟦ t ⟧ᴹ + cong-⟦ var r ⟧ = cong-η r + cong-⟦ s ∙ t ⟧ = congᴹ cong-⟦ s ⟧ cong-⟦ t ⟧ + + isRelHomomorphismᴹ : IsRelHomomorphism _≈_ _≈ᴹ_ ⟦_⟧ᴹ + isRelHomomorphismᴹ = record { cong = cong-⟦_⟧ } + + setoidHomomorphismᴹ : SetoidHomomorphism FA setoidᴹ + setoidHomomorphismᴹ = record { ⟦_⟧ = ⟦_⟧ᴹ ; isRelHomomorphism = isRelHomomorphismᴹ } + + isMagmaHomomorphismᴹ : IsMagmaHomomorphism rawMagma rawMagmaᴹ ⟦_⟧ᴹ + isMagmaHomomorphismᴹ = record { isRelHomomorphism = isRelHomomorphismᴹ + ; homo = λ s t → begin ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ } + + magmaHomomorphismᴹ : MagmaHomomorphism freeMagma 𝓜 + magmaHomomorphismᴹ = record { ⟦_⟧ = ⟦_⟧ᴹ + ; isMagmaHomomorphism = isMagmaHomomorphismᴹ } + + record η-MagmaHomomorphism : Set (suc (a ⊔ m ⊔ ℓa ⊔ ℓm)) where + + field + magmaHomomorphism : MagmaHomomorphism freeMagma 𝓜 + open MagmaHomomorphism magmaHomomorphism public renaming (homo to ⟦⟧-homo) + field + ⟦_⟧∘var≈ᴹη : ∀ a → ⟦ var a ⟧ ≈ᴹ η a + + module Uniqueness (η-magmaHomomorphism : η-MagmaHomomorphism) where + + open η-MagmaHomomorphism η-magmaHomomorphism + + isUnique⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ ≈ᴹ ⟦ t ⟧ᴹ + isUnique⟦ var a ⟧ᴹ = ⟦ a ⟧∘var≈ᴹη + isUnique⟦ s ∙ t ⟧ᴹ = begin + ⟦ s Syntax.∙ t ⟧ ≈⟨ ⟦⟧-homo s t ⟩ + ⟦ s ⟧ ∙ᴹ ⟦ t ⟧ ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ + ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ + + module Corollary (𝓗 𝓚 : η-MagmaHomomorphism) + where + open η-MagmaHomomorphism 𝓗 renaming (⟦_⟧ to ⟦_⟧ᴴ) + open η-MagmaHomomorphism 𝓚 renaming (⟦_⟧ to ⟦_⟧ᴷ) + open Uniqueness 𝓗 renaming (isUnique⟦_⟧ᴹ to isUnique⟦_⟧ᴴ) + open Uniqueness 𝓚 renaming (isUnique⟦_⟧ᴹ to isUnique⟦_⟧ᴷ) + + isUnique⟦_⟧ : ∀ t → ⟦ t ⟧ᴴ ≈ᴹ ⟦ t ⟧ᴷ + isUnique⟦ t ⟧ = begin ⟦ t ⟧ᴴ ≈⟨ isUnique⟦ t ⟧ᴴ ⟩ ⟦ t ⟧ᴹ ≈˘⟨ isUnique⟦ t ⟧ᴷ ⟩ ⟦ t ⟧ᴷ ∎ -- immediate corollary - open FreeMagma setoidᴹ - open Properties setoidᴹ - - alg-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma rawMagmaᴹ alg - alg-isMagmaHomomorphism = Existence.isMagmaHomomorphism (record { cong = id }) +module _ (𝓜 : Magma m ℓm) where + open Magma 𝓜 renaming (setoid to setoidᴹ) + algMagmaHomomorphism : MagmaHomomorphism (FreeMagma.freeMagma setoidᴹ) 𝓜 + algMagmaHomomorphism = Existence.magmaHomomorphismᴹ + where open LeftAdjoint 𝓜 (Identity.setoidHomomorphism setoidᴹ) + ------------------------------------------------------------------------ --- Functoriality of FreeMagma wrt Setoid homomorphisms - -module FreeMagmaFunctor (𝓗 : SetoidHomomorphism 𝓐 𝓑) where - - open Setoid 𝓐 renaming (Carrier to UA; _≈_ to _≈ᴬ_) - open Setoid 𝓑 renaming (Carrier to UB; _≈_ to _≈ᴮ_) - - open FreeMagma 𝓐 - renaming (freeMagma to freeMagmaᴬ; rawMagma to rawMagmaᴬ - ; Carrier to UFA; _≈_ to _≈ᵀᴬ_; isMagma to isMagmaᴬ) - - open FreeMagma 𝓑 - renaming (freeMagma to freeMagmaᴮ; rawMagma to rawMagmaᴮ - ; Carrier to UFB; _≈_ to _≈ᵀᴮ_; isMagma to isMagmaᴮ) - - open Properties freeMagmaᴮ 𝓐 +-- Action of FreeMagma on Setoid homomorphisms - open SetoidHomomorphism 𝓗 +module FreeMagmaFunctor {𝓐 : Setoid a ℓa} {𝓑 : Setoid b ℓb} + (𝓗 : SetoidHomomorphism 𝓐 𝓑) where - η : UA → UFB - η = Syntax.var ∘ ⟦_⟧ + open FreeMagma 𝓐 renaming (freeMagma to freeMagmaᴬ) + open FreeMagma 𝓑 renaming (freeMagma to freeMagmaᴮ + ; varSetoidHomomorphism to 𝓥ᴮ) - hom-η : IsRelHomomorphism _≈ᴬ_ _≈ᵀᴮ_ η - hom-η = record { cong = EquationalTheory.var ∘ congᴬᴮ } - where open IsRelHomomorphism isRelHomomorphism renaming (cong to congᴬᴮ) - - open Existence - - map : UFA → UFB - map = ⟦_⟧ᴹ hom-η - - map-isMagmaHomomorphism : IsMagmaHomomorphism rawMagmaᴬ rawMagmaᴮ map - map-isMagmaHomomorphism = isMagmaHomomorphism hom-η + mapMagmaHomomorphism : MagmaHomomorphism freeMagmaᴬ freeMagmaᴮ + mapMagmaHomomorphism = Existence.magmaHomomorphismᴹ + where open LeftAdjoint freeMagmaᴮ (Compose.setoidHomomorphism 𝓗 𝓥ᴮ) ------------------------------------------------------------------------ -- Naturality of alg module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where - open Magma 𝓜 renaming (rawMagma to M; setoid to setoidᴹ; Carrier to UM; _≈_ to _≈ᴹ_) - open Magma 𝓝 renaming (rawMagma to N; setoid to setoidᴺ; Carrier to UN; _≈_ to _≈ᴺ_; refl to reflᴺ; trans to transᴺ) - module _ (𝓗 : SetoidHomomorphism setoidᴹ setoidᴺ) where - open SetoidHomomorphism 𝓗 renaming (isRelHomomorphism to hom-⟦⟧) - open FreeMagmaFunctor 𝓗 - open FreeMagma setoidᴹ renaming (freeMagma to freeMagmaᴹ; rawMagma to FM; Carrier to UFM) - algᴹ = alg 𝓜 - algᴹ-isMagmaHomomorphism = alg-isMagmaHomomorphism 𝓜 - algᴺ = alg 𝓝 - algᴺ-isMagmaHomomorphism = alg-isMagmaHomomorphism 𝓝 - module _ (hom : IsMagmaHomomorphism M N ⟦_⟧) where - - h k : UFM → UN - h = ⟦_⟧ ∘ algᴹ - k = algᴺ ∘ map - - h-hom : IsMagmaHomomorphism FM N h - h-hom = Compose.isMagmaHomomorphism transᴺ algᴹ-isMagmaHomomorphism hom - - k-hom : IsMagmaHomomorphism FM N k - k-hom = Compose.isMagmaHomomorphism transᴺ map-isMagmaHomomorphism algᴺ-isMagmaHomomorphism - - naturality : ∀ t → h t ≈ᴺ k t - naturality = isUnique hom-⟦⟧ h-hom k-hom (λ _ → reflᴺ) (λ _ → reflᴺ) - where open Properties.Existence.Corollary 𝓝 setoidᴹ - + open Magma 𝓜 using () renaming (setoid to setoidᴹ) + open Magma 𝓝 using () renaming (_≈_ to _≈ᴺ_; refl to reflᴺ; trans to transᴺ) + + module _ (𝓕 : MagmaHomomorphism 𝓜 𝓝) where + open MagmaHomomorphism 𝓕 using (⟦_⟧; isMagmaHomomorphism; setoidHomomorphism) + open FreeMagmaFunctor setoidHomomorphism using (mapMagmaHomomorphism) + open MagmaHomomorphism mapMagmaHomomorphism + renaming (⟦_⟧ to map; isMagmaHomomorphism to map-isMagmaHomomorphism; setoidHomomorphism to mapSetoidHomomorphism) + open FreeMagma setoidᴹ renaming (freeMagma to freeMagmaᴹ) + open LeftAdjoint 𝓝 setoidHomomorphism + open MagmaHomomorphism (algMagmaHomomorphism 𝓜) + renaming (⟦_⟧ to algᴹ; isMagmaHomomorphism to algᴹ-isMagmaHomomorphism) + open MagmaHomomorphism (algMagmaHomomorphism 𝓝) + renaming (⟦_⟧ to algᴺ; isMagmaHomomorphism to algᴺ-isMagmaHomomorphism) + + H K : MagmaHomomorphism freeMagmaᴹ 𝓝 + H = record { ⟦_⟧ = ⟦_⟧ ∘ algᴹ + ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transᴺ algᴹ-isMagmaHomomorphism isMagmaHomomorphism } + + K = record { ⟦_⟧ = algᴺ ∘ map + ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transᴺ map-isMagmaHomomorphism algᴺ-isMagmaHomomorphism } + + open Existence using (η-MagmaHomomorphism; module Corollary) + + naturality : ∀ t → ⟦ algᴹ t ⟧ ≈ᴺ algᴺ (map t) + naturality = Corollary.isUnique⟦_⟧ 𝓗 𝓚 + where + 𝓗 𝓚 : η-MagmaHomomorphism + 𝓗 = record { magmaHomomorphism = H ; ⟦_⟧∘var≈ᴹη = λ _ → reflᴺ } + 𝓚 = record { magmaHomomorphism = K ; ⟦_⟧∘var≈ᴹη = λ _ → reflᴺ } + ------------------------------------------------------------------------ --- Functoriality of FreeMagmaFunctor.map : TODO +-- Functoriality of FreeMagmaFunctor.map : TODO, by analogy with naturality ------------------------------------------------------------------------ -- Monad instance: TODO From 01862326ea0776ef26b024e3262efa2ec27a340a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 May 2023 14:31:23 +0100 Subject: [PATCH 30/37] added functoriality of `FreeMagmaFunctor` --- src/Algebra/Bundles/Free/Magma.agda | 66 ++++++++++++++++++++++++++--- 1 file changed, 61 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index cfc9886107..dd40aeca2b 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -14,6 +14,7 @@ open import Algebra.Bundles.Raw using (RawMagma) import Algebra.Definitions as Definitions using (Congruent₂) import Algebra.Structures as Structures using (IsMagma) open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) +import Algebra.Morphism.Construct.Identity as Identity import Algebra.Morphism.Construct.Composition as Compose open import Effect.Functor open import Effect.Monad @@ -33,11 +34,12 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable - a ℓa b ℓb c ℓ m ℓm n ℓn : Level + ℓ a ℓa b ℓb c ℓc m ℓm n ℓn : Level A : Set a B : Set b C : Set c + ------------------------------------------------------------------------ -- Morphisms between Magmas: belongs in its own place -- Algebra.Morphism.Bundles @@ -309,11 +311,13 @@ module LeftAdjoint {𝓐 : Setoid a ℓa} (𝓜 : Magma m ℓm) -- immediate corollary module _ (𝓜 : Magma m ℓm) where - open Magma 𝓜 renaming (setoid to setoidᴹ) - algMagmaHomomorphism : MagmaHomomorphism (FreeMagma.freeMagma setoidᴹ) 𝓜 + open Magma 𝓜 renaming (setoid to setoidᴹ; _≈_ to _≈ᴹ_; isMagma to isMagmaᴹ) + open FreeMagma setoidᴹ + + algMagmaHomomorphism : MagmaHomomorphism freeMagma 𝓜 algMagmaHomomorphism = Existence.magmaHomomorphismᴹ where open LeftAdjoint 𝓜 (Identity.setoidHomomorphism setoidᴹ) - + ------------------------------------------------------------------------ -- Action of FreeMagma on Setoid homomorphisms @@ -366,7 +370,59 @@ module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where ------------------------------------------------------------------------ --- Functoriality of FreeMagmaFunctor.map : TODO, by analogy with naturality +-- Functoriality of FreeMagmaFunctor.map : by analogy with naturality + +module Functoriality + {𝓐 : Setoid a ℓa} {𝓑 : Setoid b ℓb} {𝓒 : Setoid c ℓc} + (𝓗 : SetoidHomomorphism 𝓐 𝓑) (𝓚 : SetoidHomomorphism 𝓑 𝓒) where + + 𝓕 : SetoidHomomorphism 𝓐 𝓒 + 𝓕 = Compose.setoidHomomorphism 𝓗 𝓚 + + open FreeMagma 𝓐 renaming (freeMagma to freeMagmaA) + open FreeMagma 𝓑 renaming (freeMagma to freeMagmaB) + open FreeMagma 𝓒 renaming (freeMagma to freeMagmaC + ; rawMagma to rawMagmaC + ; setoid to setoidFC + ; varSetoidHomomorphism to 𝓥) + open Setoid setoidFC renaming (_≈_ to _≈FC_; refl to reflFC; trans to transFC) + 𝓥∘𝓕 = Compose.setoidHomomorphism 𝓕 𝓥 + open FreeMagmaFunctor 𝓕 renaming (mapMagmaHomomorphism to MapAC) + open FreeMagmaFunctor 𝓗 renaming (mapMagmaHomomorphism to MapAB) + open FreeMagmaFunctor 𝓚 renaming (mapMagmaHomomorphism to MapBC) + open MagmaHomomorphism MapAC renaming (⟦_⟧ to mapAC) + open MagmaHomomorphism MapAB renaming (⟦_⟧ to mapAB; isMagmaHomomorphism to isMagmaAB) + open MagmaHomomorphism MapBC renaming (⟦_⟧ to mapBC; isMagmaHomomorphism to isMagmaBC) + + Id : MagmaHomomorphism freeMagmaC freeMagmaC + Id = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = Identity.isMagmaHomomorphism rawMagmaC reflFC} + + open FreeMagmaFunctor (Identity.setoidHomomorphism 𝓒) + renaming (mapMagmaHomomorphism to MapCC) + open MagmaHomomorphism MapCC renaming (⟦_⟧ to map-Id) + + map-id : ∀ t → map-Id t ≈FC t + map-id = Corollary.isUnique⟦_⟧ 𝓘𝓒 𝓘 + where + open LeftAdjoint.Existence freeMagmaC 𝓥 + 𝓘𝓒 𝓘 : η-MagmaHomomorphism + 𝓘𝓒 = record { magmaHomomorphism = MapCC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } + 𝓘 = record { magmaHomomorphism = Id ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } + + MapBC∘MapAB : MagmaHomomorphism freeMagmaA freeMagmaC + MapBC∘MapAB = record + { ⟦_⟧ = mapBC ∘ mapAB + ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transFC isMagmaAB isMagmaBC} + + map-∘ : ∀ t → mapAC t ≈FC mapBC (mapAB t) + map-∘ = Corollary.isUnique⟦_⟧ 𝓐𝓒 𝓑𝓒∘𝓐𝓑 + where + open LeftAdjoint.Existence freeMagmaC 𝓥∘𝓕 + 𝓐𝓒 𝓑𝓒∘𝓐𝓑 : η-MagmaHomomorphism + 𝓐𝓒 = record { magmaHomomorphism = MapAC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } + 𝓑𝓒∘𝓐𝓑 = record { magmaHomomorphism = MapBC∘MapAB ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } ------------------------------------------------------------------------ -- Monad instance: TODO From 7a18f084c2a6b27906ee332839ca0bbf23cb91fd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 May 2023 14:50:56 +0100 Subject: [PATCH 31/37] refactored functoriality of `FreeMagmaFunctor` --- src/Algebra/Bundles/Free/Magma.agda | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index dd40aeca2b..bd527b4151 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -372,7 +372,28 @@ module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where ------------------------------------------------------------------------ -- Functoriality of FreeMagmaFunctor.map : by analogy with naturality -module Functoriality +module IdentityLaw (𝓐 : Setoid a ℓa) where + + open FreeMagma 𝓐 renaming (varSetoidHomomorphism to 𝓥) + open Setoid setoid renaming (_≈_ to _≈FA_; refl to reflFA; trans to transFA) + + Id : MagmaHomomorphism freeMagma freeMagma + Id = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = Identity.isMagmaHomomorphism rawMagma reflFA} + + open FreeMagmaFunctor (Identity.setoidHomomorphism 𝓐) + open MagmaHomomorphism mapMagmaHomomorphism renaming (⟦_⟧ to map-Id) + + map-id : ∀ t → map-Id t ≈FA t + map-id = Corollary.isUnique⟦_⟧ 𝓘ᴬ 𝓘 + where + open LeftAdjoint.Existence freeMagma 𝓥 + 𝓘ᴬ 𝓘 : η-MagmaHomomorphism + 𝓘ᴬ = record { magmaHomomorphism = mapMagmaHomomorphism ; ⟦_⟧∘var≈ᴹη = λ _ → reflFA } + 𝓘 = record { magmaHomomorphism = Id ; ⟦_⟧∘var≈ᴹη = λ _ → reflFA } + +module CompositionLaw {𝓐 : Setoid a ℓa} {𝓑 : Setoid b ℓb} {𝓒 : Setoid c ℓc} (𝓗 : SetoidHomomorphism 𝓐 𝓑) (𝓚 : SetoidHomomorphism 𝓑 𝓒) where From 6bbc2af859ff001ca2482badae1a8620060ff2af Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 May 2023 15:12:54 +0100 Subject: [PATCH 32/37] tidied up leftovers of functoriality of `FreeMagmaFunctor` --- src/Algebra/Bundles/Free/Magma.agda | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index bd527b4151..bc44fe8197 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -415,23 +415,6 @@ module CompositionLaw open MagmaHomomorphism MapAB renaming (⟦_⟧ to mapAB; isMagmaHomomorphism to isMagmaAB) open MagmaHomomorphism MapBC renaming (⟦_⟧ to mapBC; isMagmaHomomorphism to isMagmaBC) - Id : MagmaHomomorphism freeMagmaC freeMagmaC - Id = record - { ⟦_⟧ = id - ; isMagmaHomomorphism = Identity.isMagmaHomomorphism rawMagmaC reflFC} - - open FreeMagmaFunctor (Identity.setoidHomomorphism 𝓒) - renaming (mapMagmaHomomorphism to MapCC) - open MagmaHomomorphism MapCC renaming (⟦_⟧ to map-Id) - - map-id : ∀ t → map-Id t ≈FC t - map-id = Corollary.isUnique⟦_⟧ 𝓘𝓒 𝓘 - where - open LeftAdjoint.Existence freeMagmaC 𝓥 - 𝓘𝓒 𝓘 : η-MagmaHomomorphism - 𝓘𝓒 = record { magmaHomomorphism = MapCC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } - 𝓘 = record { magmaHomomorphism = Id ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } - MapBC∘MapAB : MagmaHomomorphism freeMagmaA freeMagmaC MapBC∘MapAB = record { ⟦_⟧ = mapBC ∘ mapAB From 90434b7b36a1a22d802fd0fd5c24c3844a628b0f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 1 May 2023 16:04:25 +0100 Subject: [PATCH 33/37] refactored dependencies; `Uniqueness` and its `Corollary` no longer depend on `Existence` --- src/Algebra/Bundles/Free/Magma.agda | 86 +++++++++++++++-------------- 1 file changed, 45 insertions(+), 41 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index bc44fe8197..cfc63a6b27 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -245,15 +245,17 @@ module LeftAdjoint {𝓐 : Setoid a ℓa} (𝓜 : Magma m ℓm) open SetoidHomomorphism 𝓗 renaming (⟦_⟧ to η; isRelHomomorphism to hom-η) - module Existence where + private ⟦_⟧ᴹ : UFA → UM ⟦_⟧ᴹ = ⟦_⟧ η - open Structures _≈ᴹ_ - open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) - open IsRelHomomorphism hom-η renaming (cong to cong-η) + open Structures _≈ᴹ_ + open IsMagma isMagmaᴹ renaming (∙-cong to congᴹ) + open IsRelHomomorphism hom-η renaming (cong to cong-η) + module Existence where + private algᴹ = alg 𝓜 @@ -279,36 +281,41 @@ module LeftAdjoint {𝓐 : Setoid a ℓa} (𝓜 : Magma m ℓm) magmaHomomorphismᴹ = record { ⟦_⟧ = ⟦_⟧ᴹ ; isMagmaHomomorphism = isMagmaHomomorphismᴹ } - record η-MagmaHomomorphism : Set (suc (a ⊔ m ⊔ ℓa ⊔ ℓm)) where + record η-MagmaHomomorphism : Set (suc (a ⊔ m ⊔ ℓa ⊔ ℓm)) where - field - magmaHomomorphism : MagmaHomomorphism freeMagma 𝓜 - open MagmaHomomorphism magmaHomomorphism public renaming (homo to ⟦⟧-homo) - field - ⟦_⟧∘var≈ᴹη : ∀ a → ⟦ var a ⟧ ≈ᴹ η a + field + magmaHomomorphism : MagmaHomomorphism freeMagma 𝓜 + open MagmaHomomorphism magmaHomomorphism public renaming (homo to ⟦⟧-homo) + field + ⟦_⟧∘var≈ᴹη : ∀ a → ⟦ var a ⟧ ≈ᴹ η a - module Uniqueness (η-magmaHomomorphism : η-MagmaHomomorphism) where + ⟦⟧ᴹ-η-MagmaHomomorphism : η-MagmaHomomorphism + ⟦⟧ᴹ-η-MagmaHomomorphism = record { magmaHomomorphism = Existence.magmaHomomorphismᴹ + ; ⟦_⟧∘var≈ᴹη = Existence.unfold-⟦_⟧ᴹ ∘ var } + + module Uniqueness (η-magmaHomomorphism : η-MagmaHomomorphism) where - open η-MagmaHomomorphism η-magmaHomomorphism + open η-MagmaHomomorphism η-magmaHomomorphism - isUnique⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ ≈ᴹ ⟦ t ⟧ᴹ - isUnique⟦ var a ⟧ᴹ = ⟦ a ⟧∘var≈ᴹη - isUnique⟦ s ∙ t ⟧ᴹ = begin - ⟦ s Syntax.∙ t ⟧ ≈⟨ ⟦⟧-homo s t ⟩ - ⟦ s ⟧ ∙ᴹ ⟦ t ⟧ ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ - ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ - - module Corollary (𝓗 𝓚 : η-MagmaHomomorphism) - where - open η-MagmaHomomorphism 𝓗 renaming (⟦_⟧ to ⟦_⟧ᴴ) - open η-MagmaHomomorphism 𝓚 renaming (⟦_⟧ to ⟦_⟧ᴷ) - open Uniqueness 𝓗 renaming (isUnique⟦_⟧ᴹ to isUnique⟦_⟧ᴴ) - open Uniqueness 𝓚 renaming (isUnique⟦_⟧ᴹ to isUnique⟦_⟧ᴷ) + isUnique⟦_⟧ᴹ : ∀ t → ⟦ t ⟧ ≈ᴹ ⟦ t ⟧ᴹ + isUnique⟦ var a ⟧ᴹ = ⟦ a ⟧∘var≈ᴹη + isUnique⟦ s ∙ t ⟧ᴹ = begin + ⟦ s Syntax.∙ t ⟧ ≈⟨ ⟦⟧-homo s t ⟩ + ⟦ s ⟧ ∙ᴹ ⟦ t ⟧ ≈⟨ congᴹ isUnique⟦ s ⟧ᴹ isUnique⟦ t ⟧ᴹ ⟩ + ⟦ s ⟧ᴹ ∙ᴹ ⟦ t ⟧ᴹ ∎ + + module Corollary (𝓗 𝓚 : η-MagmaHomomorphism) + where + open η-MagmaHomomorphism 𝓗 renaming (⟦_⟧ to ⟦_⟧ᴴ) + open η-MagmaHomomorphism 𝓚 renaming (⟦_⟧ to ⟦_⟧ᴷ) + open Uniqueness 𝓗 renaming (isUnique⟦_⟧ᴹ to isUnique⟦_⟧ᴴ) + open Uniqueness 𝓚 renaming (isUnique⟦_⟧ᴹ to isUnique⟦_⟧ᴷ) - isUnique⟦_⟧ : ∀ t → ⟦ t ⟧ᴴ ≈ᴹ ⟦ t ⟧ᴷ - isUnique⟦ t ⟧ = begin ⟦ t ⟧ᴴ ≈⟨ isUnique⟦ t ⟧ᴴ ⟩ ⟦ t ⟧ᴹ ≈˘⟨ isUnique⟦ t ⟧ᴷ ⟩ ⟦ t ⟧ᴷ ∎ + isUnique⟦_⟧ : ∀ t → ⟦ t ⟧ᴴ ≈ᴹ ⟦ t ⟧ᴷ + isUnique⟦ t ⟧ = begin ⟦ t ⟧ᴴ ≈⟨ isUnique⟦ t ⟧ᴴ ⟩ ⟦ t ⟧ᴹ ≈˘⟨ isUnique⟦ t ⟧ᴷ ⟩ ⟦ t ⟧ᴷ ∎ --- immediate corollary +------------------------------------------------------------------------ +-- immediate corollary: alg is in fact a MagmaHomomorphism module _ (𝓜 : Magma m ℓm) where open Magma 𝓜 renaming (setoid to setoidᴹ; _≈_ to _≈ᴹ_; isMagma to isMagmaᴹ) @@ -352,18 +359,16 @@ module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where open MagmaHomomorphism (algMagmaHomomorphism 𝓝) renaming (⟦_⟧ to algᴺ; isMagmaHomomorphism to algᴺ-isMagmaHomomorphism) - H K : MagmaHomomorphism freeMagmaᴹ 𝓝 - H = record { ⟦_⟧ = ⟦_⟧ ∘ algᴹ - ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transᴺ algᴹ-isMagmaHomomorphism isMagmaHomomorphism } - - K = record { ⟦_⟧ = algᴺ ∘ map - ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transᴺ map-isMagmaHomomorphism algᴺ-isMagmaHomomorphism } - - open Existence using (η-MagmaHomomorphism; module Corollary) - naturality : ∀ t → ⟦ algᴹ t ⟧ ≈ᴺ algᴺ (map t) naturality = Corollary.isUnique⟦_⟧ 𝓗 𝓚 where + H K : MagmaHomomorphism freeMagmaᴹ 𝓝 + H = record { ⟦_⟧ = ⟦_⟧ ∘ algᴹ + ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transᴺ algᴹ-isMagmaHomomorphism isMagmaHomomorphism } + + K = record { ⟦_⟧ = algᴺ ∘ map + ; isMagmaHomomorphism = Compose.isMagmaHomomorphism transᴺ map-isMagmaHomomorphism algᴺ-isMagmaHomomorphism } + 𝓗 𝓚 : η-MagmaHomomorphism 𝓗 = record { magmaHomomorphism = H ; ⟦_⟧∘var≈ᴹη = λ _ → reflᴺ } 𝓚 = record { magmaHomomorphism = K ; ⟦_⟧∘var≈ᴹη = λ _ → reflᴺ } @@ -388,7 +393,7 @@ module IdentityLaw (𝓐 : Setoid a ℓa) where map-id : ∀ t → map-Id t ≈FA t map-id = Corollary.isUnique⟦_⟧ 𝓘ᴬ 𝓘 where - open LeftAdjoint.Existence freeMagma 𝓥 + open LeftAdjoint freeMagma 𝓥 𝓘ᴬ 𝓘 : η-MagmaHomomorphism 𝓘ᴬ = record { magmaHomomorphism = mapMagmaHomomorphism ; ⟦_⟧∘var≈ᴹη = λ _ → reflFA } 𝓘 = record { magmaHomomorphism = Id ; ⟦_⟧∘var≈ᴹη = λ _ → reflFA } @@ -403,7 +408,6 @@ module CompositionLaw open FreeMagma 𝓐 renaming (freeMagma to freeMagmaA) open FreeMagma 𝓑 renaming (freeMagma to freeMagmaB) open FreeMagma 𝓒 renaming (freeMagma to freeMagmaC - ; rawMagma to rawMagmaC ; setoid to setoidFC ; varSetoidHomomorphism to 𝓥) open Setoid setoidFC renaming (_≈_ to _≈FC_; refl to reflFC; trans to transFC) @@ -423,11 +427,11 @@ module CompositionLaw map-∘ : ∀ t → mapAC t ≈FC mapBC (mapAB t) map-∘ = Corollary.isUnique⟦_⟧ 𝓐𝓒 𝓑𝓒∘𝓐𝓑 where - open LeftAdjoint.Existence freeMagmaC 𝓥∘𝓕 + open LeftAdjoint freeMagmaC 𝓥∘𝓕 𝓐𝓒 𝓑𝓒∘𝓐𝓑 : η-MagmaHomomorphism 𝓐𝓒 = record { magmaHomomorphism = MapAC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } 𝓑𝓒∘𝓐𝓑 = record { magmaHomomorphism = MapBC∘MapAB ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } ------------------------------------------------------------------------ --- Monad instance: TODO +-- Monad instance, etc.: TODO From 038862958a8aafae1b24da185e3e474a71381e41 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 1 May 2023 16:31:58 +0100 Subject: [PATCH 34/37] reverted bogus `merge`; retained refactored dependencies --- src/Algebra/Bundles/Free/Magma.agda | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index cfc63a6b27..45ff0fe06a 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -99,6 +99,7 @@ module Syntax where syntaxRawMonad : RawMonad (Syntax {a}) syntaxRawMonad = mkRawMonad Syntax var bind + ------------------------------------------------------------------------ -- parametrised 'equational' theory over the 'pre'-free algebra @@ -137,6 +138,7 @@ module EquationalTheory {A : Set a} (_≈ᴬ_ : Rel A ℓ) where varIsRelHomomorphism : IsRelHomomorphism _≈ᴬ_ _≈_ var varIsRelHomomorphism = record { cong = var } + ------------------------------------------------------------------------ -- Free algebra on a Set {- @@ -171,6 +173,7 @@ module FreeRawMagma (A : Set a) where freeMagma : Magma a a freeMagma = record { RawMagma freeRawMagma ; isMagma = isMagma } + ------------------------------------------------------------------------ -- Free algebra on a Setoid @@ -198,6 +201,7 @@ module FreeMagma (𝓐 : Setoid a ℓa) where varSetoidHomomorphism : SetoidHomomorphism 𝓐 setoid varSetoidHomomorphism = record { ⟦_⟧ = var; isRelHomomorphism = varIsRelHomomorphism } + ------------------------------------------------------------------------ -- Semantics: in terms of concrete Magma instances @@ -233,6 +237,7 @@ module LeftAdjoint {𝓐 : Setoid a ℓa} (𝓜 : Magma m ℓm) renaming (Carrier to UM; _≈_ to _≈ᴹ_; _∙_ to _∙ᴹ_ ; setoid to setoidᴹ; rawMagma to rawMagmaᴹ ; isMagma to isMagmaᴹ) + open ≈-Reasoning setoidᴹ open Syntax @@ -315,7 +320,7 @@ module LeftAdjoint {𝓐 : Setoid a ℓa} (𝓜 : Magma m ℓm) isUnique⟦ t ⟧ = begin ⟦ t ⟧ᴴ ≈⟨ isUnique⟦ t ⟧ᴴ ⟩ ⟦ t ⟧ᴹ ≈˘⟨ isUnique⟦ t ⟧ᴷ ⟩ ⟦ t ⟧ᴷ ∎ ------------------------------------------------------------------------ --- immediate corollary: alg is in fact a MagmaHomomorphism +-- Immediate corollary: alg is in fact a MagmaHomomorphism module _ (𝓜 : Magma m ℓm) where open Magma 𝓜 renaming (setoid to setoidᴹ; _≈_ to _≈ᴹ_; isMagma to isMagmaᴹ) @@ -380,7 +385,7 @@ module Naturality {𝓜 : Magma m ℓm} {𝓝 : Magma n ℓn} where module IdentityLaw (𝓐 : Setoid a ℓa) where open FreeMagma 𝓐 renaming (varSetoidHomomorphism to 𝓥) - open Setoid setoid renaming (_≈_ to _≈FA_; refl to reflFA; trans to transFA) + open Setoid setoid renaming (_≈_ to _≈FA_; refl to reflFA) Id : MagmaHomomorphism freeMagma freeMagma Id = record @@ -432,6 +437,7 @@ module CompositionLaw 𝓐𝓒 = record { magmaHomomorphism = MapAC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } 𝓑𝓒∘𝓐𝓑 = record { magmaHomomorphism = MapBC∘MapAB ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } + ------------------------------------------------------------------------ -- Monad instance, etc.: TODO From bb3c155ff9b191e2b2668a6d1828b368404ef141 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 1 May 2023 16:33:38 +0100 Subject: [PATCH 35/37] Revert "tidied up leftovers of functoriality of `FreeMagmaFunctor`" This reverts commit 6bbc2af859ff001ca2482badae1a8620060ff2af. --- src/Algebra/Bundles/Free/Magma.agda | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 45ff0fe06a..199af69b4b 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -424,6 +424,23 @@ module CompositionLaw open MagmaHomomorphism MapAB renaming (⟦_⟧ to mapAB; isMagmaHomomorphism to isMagmaAB) open MagmaHomomorphism MapBC renaming (⟦_⟧ to mapBC; isMagmaHomomorphism to isMagmaBC) + Id : MagmaHomomorphism freeMagmaC freeMagmaC + Id = record + { ⟦_⟧ = id + ; isMagmaHomomorphism = Identity.isMagmaHomomorphism rawMagmaC reflFC} + + open FreeMagmaFunctor (Identity.setoidHomomorphism 𝓒) + renaming (mapMagmaHomomorphism to MapCC) + open MagmaHomomorphism MapCC renaming (⟦_⟧ to map-Id) + + map-id : ∀ t → map-Id t ≈FC t + map-id = Corollary.isUnique⟦_⟧ 𝓘𝓒 𝓘 + where + open LeftAdjoint.Existence freeMagmaC 𝓥 + 𝓘𝓒 𝓘 : η-MagmaHomomorphism + 𝓘𝓒 = record { magmaHomomorphism = MapCC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } + 𝓘 = record { magmaHomomorphism = Id ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } + MapBC∘MapAB : MagmaHomomorphism freeMagmaA freeMagmaC MapBC∘MapAB = record { ⟦_⟧ = mapBC ∘ mapAB From 6835c67340aaea2a5b89015ea937e2c219ee08b3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 1 May 2023 16:38:15 +0100 Subject: [PATCH 36/37] final reversion of commits --- src/Algebra/Bundles/Free/Magma.agda | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/Algebra/Bundles/Free/Magma.agda b/src/Algebra/Bundles/Free/Magma.agda index 199af69b4b..45ff0fe06a 100644 --- a/src/Algebra/Bundles/Free/Magma.agda +++ b/src/Algebra/Bundles/Free/Magma.agda @@ -424,23 +424,6 @@ module CompositionLaw open MagmaHomomorphism MapAB renaming (⟦_⟧ to mapAB; isMagmaHomomorphism to isMagmaAB) open MagmaHomomorphism MapBC renaming (⟦_⟧ to mapBC; isMagmaHomomorphism to isMagmaBC) - Id : MagmaHomomorphism freeMagmaC freeMagmaC - Id = record - { ⟦_⟧ = id - ; isMagmaHomomorphism = Identity.isMagmaHomomorphism rawMagmaC reflFC} - - open FreeMagmaFunctor (Identity.setoidHomomorphism 𝓒) - renaming (mapMagmaHomomorphism to MapCC) - open MagmaHomomorphism MapCC renaming (⟦_⟧ to map-Id) - - map-id : ∀ t → map-Id t ≈FC t - map-id = Corollary.isUnique⟦_⟧ 𝓘𝓒 𝓘 - where - open LeftAdjoint.Existence freeMagmaC 𝓥 - 𝓘𝓒 𝓘 : η-MagmaHomomorphism - 𝓘𝓒 = record { magmaHomomorphism = MapCC ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } - 𝓘 = record { magmaHomomorphism = Id ; ⟦_⟧∘var≈ᴹη = λ _ → reflFC } - MapBC∘MapAB : MagmaHomomorphism freeMagmaA freeMagmaC MapBC∘MapAB = record { ⟦_⟧ = mapBC ∘ mapAB From e0a44ddcff897494985909af07bc47877e3dcb91 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 1 May 2023 16:47:22 +0100 Subject: [PATCH 37/37] Revert "tweaks" This reverts commit f120c1ee4ba08fc8ad279bdd40d350c5b87bad0b. --- CHANGELOG.md | 2 +- src/Data/Nat/Base.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 21b1481861..bd6f7350cd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1137,7 +1137,7 @@ Deprecated names * In `Data.Nat.Base`: ``` - _≤″_.proof ↦ Data.Product.Base.proj₂ + _≤″_.proof ↦ proj₂ ``` * In `Data.Nat.Properties`: diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 5dc16c0183..a9c21d9359 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -15,7 +15,7 @@ open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; Raw open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) -open import Data.Product.Base using (_,_) +open import Data.Product.Base using (_,_; proj₁) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core