From 05cbf6f56bce1d45876630fe29b694dc57942e9c Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 13 Nov 2025 13:24:21 -0600 Subject: Add adjunction between free monoid and forget --- Data/Monoid.agda | 66 ++++++++++++++++++++++++++++++ Data/Opaque/List.agda | 110 ++++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 173 insertions(+), 3 deletions(-) create mode 100644 Data/Monoid.agda (limited to 'Data') diff --git a/Data/Monoid.agda b/Data/Monoid.agda new file mode 100644 index 0000000..ae2ded9 --- /dev/null +++ b/Data/Monoid.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +module Data.Monoid {c ℓ : Level} where + +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×) +open import Categories.Object.Monoid using (Monoid; Monoid⇒) + +module Setoids-× = SymmetricMonoidalCategory Setoids-× + +import Algebra.Bundles as Alg + +open import Data.Setoid using (∣_∣) +open import Relation.Binary using (Setoid) +open import Function using (Func) +open import Data.Product using (curry′; _,_) +open Func + +-- A monoid object in the (monoidal) category of setoids is just a monoid + +toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ +toMonoid M = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _∙_ = curry′ (to μ) + ; ε = to η _ + ; isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = curry′ (cong μ) + } + ; assoc = λ x y z → assoc {(x , y) , z} + } + ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _}) + } + } + where + open Monoid M renaming (Carrier to A) + open Setoid A + +-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism + +module _ (M N : Monoid Setoids-×.monoidal) where + + module M = Alg.Monoid (toMonoid M) + module N = Alg.Monoid (toMonoid N) + + open import Data.Product using (Σ; _,_) + open import Function using (_⟶ₛ_; _⟨$⟩_) + open import Algebra.Morphism using (IsMonoidHomomorphism) + open Monoid⇒ + toMonoid⇒ + : Monoid⇒ Setoids-×.monoidal M N + → Σ (M.setoid ⟶ₛ N.setoid) (λ f + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)) + toMonoid⇒ f = arr f , record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = cong (arr f) + } + ; homo = λ x y → preserves-μ f {x , y} + } + ; ε-homo = preserves-η f + } diff --git a/Data/Opaque/List.agda b/Data/Opaque/List.agda index a8e536f..83a2fe3 100644 --- a/Data/Opaque/List.agda +++ b/Data/Opaque/List.agda @@ -4,13 +4,19 @@ module Data.Opaque.List where import Data.List as L import Function.Construct.Constant as Const +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Level using (Level; _⊔_) +open import Algebra.Bundles using (Monoid) +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Data.List.Effectful.Foldable using (foldable; ++-homo) open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺) -open import Data.Product using (uncurry′) +open import Data.Product using (_,_; curry′; uncurry′) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) open import Data.Unit.Polymorphic using (⊤) -open import Function using (_⟶ₛ_; Func) +open import Effect.Foldable using (RawFoldable) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id) +open import Level using (Level; _⊔_) open import Relation.Binary using (Setoid) open Func @@ -52,10 +58,108 @@ opaque ∷ₛ .to = uncurry′ _∷_ ∷ₛ .cong = uncurry′ PW._∷_ + [-]ₛ : Aₛ ⟶ₛ Listₛ Aₛ + [-]ₛ .to = L.[_] + [-]ₛ .cong y = y PW.∷ PW.[] + mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ mapₛ f .to = map (to f) mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys) + cartesianProduct : ∣ Listₛ Aₛ ∣ → ∣ Listₛ Bₛ ∣ → ∣ Listₛ (Aₛ ×ₛ Bₛ) ∣ + cartesianProduct = L.cartesianProduct + + cartesian-product-cong + : {xs xs′ : ∣ Listₛ Aₛ ∣} + {ys ys′ : ∣ Listₛ Bₛ ∣} + → (let open Setoid (Listₛ Aₛ) in xs ≈ xs′) + → (let open Setoid (Listₛ Bₛ) in ys ≈ ys′) + → (let open Setoid (Listₛ (Aₛ ×ₛ Bₛ)) in cartesianProduct xs ys ≈ cartesianProduct xs′ ys′) + cartesian-product-cong PW.[] ys≋ys′ = PW.[] + cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} {xs = x₀ L.∷ xs} {xs′ = x₀′ L.∷ xs′} (x₀≈x₀′ PW.∷ xs≋xs′) ys≋ys′ = + ++⁺ + (map⁺ (x₀ ,_) (x₀′ ,_) (PW.map (x₀≈x₀′ ,_) ys≋ys′)) + (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} xs≋xs′ ys≋ys′) + + pairsₛ : Listₛ Aₛ ×ₛ Listₛ Bₛ ⟶ₛ Listₛ (Aₛ ×ₛ Bₛ) + pairsₛ .to = uncurry′ L.cartesianProduct + pairsₛ {Aₛ = Aₛ} {Bₛ = Bₛ} .cong = uncurry′ (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ}) + ++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ ++ₛ .to = uncurry′ _++_ ++ₛ .cong = uncurry′ ++⁺ + + foldr : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → ∣ Listₛ Aₛ ∣ → ∣ Bₛ ∣ + foldr f = L.foldr (curry′ (to f)) + + foldr-cong + : (f : Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) + → (e : ∣ Bₛ ∣) + → (let module [A]ₛ = Setoid (Listₛ Aₛ)) + → {xs ys : ∣ Listₛ Aₛ ∣} + → (xs [A]ₛ.≈ ys) + → (open Setoid Bₛ) + → foldr f e xs ≈ foldr f e ys + foldr-cong {Bₛ = Bₛ} f e PW.[] = Setoid.refl Bₛ + foldr-cong f e (x≈y PW.∷ xs≋ys) = cong f (x≈y , foldr-cong f e xs≋ys) + + foldrₛ : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → Listₛ Aₛ ⟶ₛ Bₛ + foldrₛ f e .to = foldr f e + foldrₛ {Bₛ = Bₛ} f e .cong = foldr-cong f e + +module _ (M : Monoid c ℓ) where + + open Monoid M renaming (setoid to Mₛ) + + opaque + unfolding List + fold : ∣ Listₛ Mₛ ∣ → ∣ Mₛ ∣ + fold = RawFoldable.fold foldable rawMonoid + + fold-cong + : {xs ys : ∣ Listₛ Mₛ ∣} + → (let module [M]ₛ = Setoid (Listₛ Mₛ)) + → (xs [M]ₛ.≈ ys) + → fold xs ≈ fold ys + fold-cong = PW.rec (λ {xs} {ys} _ → fold xs ≈ fold ys) ∙-cong refl + + foldₛ : Listₛ Mₛ ⟶ₛ Mₛ + foldₛ .to = fold + foldₛ .cong = fold-cong + + opaque + unfolding fold + ++ₛ-homo + : (xs ys : ∣ Listₛ Mₛ ∣) + → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys) + ++ₛ-homo xs ys = ++-homo M id xs + + []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε + []ₛ-homo = refl + +module _ (M N : Monoid c ℓ) where + + module M = Monoid M + module N = Monoid N + + open IsMonoidHomomorphism + + opaque + unfolding fold + + fold-mapₛ + : (f : M.setoid ⟶ₛ N.setoid) + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f) + → {xs : ∣ Listₛ M.setoid ∣} + → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs) + fold-mapₛ f isMH {L.[]} = N.sym (ε-homo isMH) + fold-mapₛ f isMH {x L.∷ xs} = begin + f′ x ∙ fold N (map f′ xs) ≈⟨ N.∙-cong N.refl (fold-mapₛ f isMH {xs}) ⟩ + f′ x ∙ f′ (fold M xs) ≈⟨ homo isMH x (fold M xs) ⟨ + f′ (x ∘ fold M xs) ∎ + where + open N using (_∙_) + open M using () renaming (_∙_ to _∘_) + open ≈-Reasoning N.setoid + f′ : M.Carrier → N.Carrier + f′ = to f -- cgit v1.2.3