From c9da00d8069d77bc4cd253d1197983e87edd1d6f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 10 Dec 2025 13:38:10 -0600 Subject: Add free/forget multiset adjunction --- Adjoint/Instance/List.agda | 2 +- Adjoint/Instance/Multiset.agda | 112 ++++++++++++++++++++++++++++++++ Data/Opaque/Multiset.agda | 74 +++++++++++++++++++-- Functor/Forgetful/Instance/CMonoid.agda | 36 ++++++++++ 4 files changed, 218 insertions(+), 6 deletions(-) create mode 100644 Adjoint/Instance/Multiset.agda create mode 100644 Functor/Forgetful/Instance/CMonoid.agda diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda index f3bf061..1b65985 100644 --- a/Adjoint/Instance/List.agda +++ b/Adjoint/Instance/List.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; _⊔_; suc; 0ℓ) +open import Level using (Level; _⊔_; suc) module Adjoint.Instance.List {ℓ : Level} where diff --git a/Adjoint/Instance/Multiset.agda b/Adjoint/Instance/Multiset.agda new file mode 100644 index 0000000..c51baa9 --- /dev/null +++ b/Adjoint/Instance/Multiset.agda @@ -0,0 +1,112 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; suc; 0ℓ) + +module Adjoint.Instance.Multiset {ℓ : Level} where + +open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×) + +private + module S = Setoids-× + +import Categories.Object.Monoid S.monoidal as MonoidObject +import Data.List as L +import Data.List.Relation.Binary.Permutation.Setoid as ↭ +import Functor.Forgetful.Instance.CMonoid S.symmetric as CMonoid +import Functor.Forgetful.Instance.Monoid S.monoidal as Monoid +import Object.Monoid.Commutative S.symmetric as CMonoidObject + +open import Categories.Adjoint using (_⊣_) +open import Categories.Category using (Category) +open import Categories.Functor using (Functor; id; _∘F_) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Category.Construction.CMonoids using (CMonoids) +open import Data.CMonoid using (toCMonoid; toCMonoid⇒) +open import Data.Monoid using (toMonoid; toMonoid⇒) +open import Data.Opaque.Multiset using ([-]ₛ; Multisetₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) +open import Data.Product using (_,_; uncurry) +open import Data.Setoid using (∣_∣) +open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Functor.Free.Instance.CMonoid {ℓ} {ℓ} using (Multisetₘ; mapₘ; MultisetCMonoid) renaming (Free to Free′) +open import Relation.Binary using (Setoid) + +open CMonoidObject using (CommutativeMonoid; CommutativeMonoid⇒) +open CommutativeMonoid using (Carrier; monoid; identityʳ) +open CommutativeMonoid⇒ using (arr; monoid⇒) +open MonoidObject using (Monoid; Monoid⇒) +open Monoid⇒ using (preserves-μ; preserves-η) + +CMon[S] : Category (suc ℓ) ℓ ℓ +CMon[S] = CMonoids S.symmetric + +Free : Functor S.U CMon[S] +Free = Free′ + +Forget : Functor CMon[S] S.U +Forget = Monoid.Forget ∘F CMonoid.Forget + +opaque + unfolding [-]ₛ + map-[-]ₛ + : {X Y : Setoid ℓ ℓ} + (f : X ⟶ₛ Y) + {x : ∣ X ∣} + → (open Setoid (Multisetₛ Y)) + → [-]ₛ ⟨$⟩ (f ⟨$⟩ x) + ≈ arr (mapₘ f) ⟨$⟩ ([-]ₛ ⟨$⟩ x) + map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Multisetₛ Y) + +unit : NaturalTransformation id (Forget ∘F Free) +unit = ntHelper record + { η = λ X → [-]ₛ {ℓ} {ℓ} {X} + ; commute = map-[-]ₛ + } + +opaque + unfolding toMonoid MultisetCMonoid + foldₘ : (X : CommutativeMonoid) → CommutativeMonoid⇒ (Multisetₘ (Carrier X)) X + foldₘ X .monoid⇒ .Monoid⇒.arr = foldₛ (toCMonoid X) + foldₘ X .monoid⇒ .preserves-μ {xs , ys} = ++ₛ-homo (toCMonoid X) xs ys + foldₘ X .monoid⇒ .preserves-η {_} = []ₛ-homo (toCMonoid X) + +opaque + unfolding foldₘ toMonoid⇒ + fold-mapₘ + : {X Y : CommutativeMonoid} + (f : CommutativeMonoid⇒ X Y) + {x : ∣ Multisetₛ (Carrier X) ∣} + → (open Setoid (Carrier Y)) + → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x) + ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x) + fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toCMonoid X) (toCMonoid Y)) (toCMonoid⇒ X Y f) + +counit : NaturalTransformation (Free ∘F Forget) id +counit = ntHelper record + { η = foldₘ + ; commute = fold-mapₘ + } + +opaque + unfolding foldₘ fold Multisetₛ + zig : (Aₛ : Setoid ℓ ℓ) + {xs : ∣ Multisetₛ Aₛ ∣} + → (open Setoid (Multisetₛ Aₛ)) + → arr (foldₘ (Multisetₘ Aₛ)) ⟨$⟩ (arr (mapₘ [-]ₛ) ⟨$⟩ xs) ≈ xs + zig Aₛ {L.[]} = ↭.↭-refl Aₛ + zig Aₛ {x L.∷ xs} = ↭.prep (Setoid.refl Aₛ) (zig Aₛ) + +opaque + unfolding foldₘ fold + zag : (M : CommutativeMonoid) + {x : ∣ Carrier M ∣} + → (open Setoid (Carrier M)) + → arr (foldₘ M) ⟨$⟩ ([-]ₛ ⟨$⟩ x) ≈ x + zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _}) + +Multiset⊣ : Free ⊣ Forget +Multiset⊣ = record + { unit = unit + ; counit = counit + ; zig = λ {X} → zig X + ; zag = λ {M} → zag M + } diff --git a/Data/Opaque/Multiset.agda b/Data/Opaque/Multiset.agda index 2ba0a0e..99501d6 100644 --- a/Data/Opaque/Multiset.agda +++ b/Data/Opaque/Multiset.agda @@ -4,14 +4,20 @@ module Data.Opaque.Multiset where import Data.List as L +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Data.Opaque.List as List -open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; prep) +open import Algebra.Bundles using (CommutativeMonoid) +open import Data.List.Effectful.Foldable using (foldable; ++-homo) +open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; ↭-refl) open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺; ++⁺; ++-comm) -open import Data.Product using (_,_) -open import Data.Product using (uncurry′) +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Data.Product using (_,_; uncurry′) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) open import Data.Setoid.Unit using (⊤ₛ) -open import Function using (_⟶ₛ_; Func; _⟨$⟩_) +open import Effect.Foldable using (RawFoldable) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id) open import Function.Construct.Constant using () renaming (function to Const) open import Level using (Level; _⊔_) open import Relation.Binary using (Setoid) @@ -50,7 +56,11 @@ opaque ∷ₛ : Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ ∷ₛ .to = uncurry′ _∷_ - ∷ₛ .cong = uncurry′ prep + ∷ₛ .cong = uncurry′ ↭.prep + + [-]ₛ : Aₛ ⟶ₛ Multisetₛ Aₛ + [-]ₛ .to = L.[_] + [-]ₛ {Aₛ} .cong y = ↭.prep y (↭-refl Aₛ) mapₛ : (Aₛ ⟶ₛ Bₛ) → Multisetₛ Aₛ ⟶ₛ Multisetₛ Bₛ mapₛ f .to = map (to f) @@ -65,3 +75,57 @@ opaque → (xs ys : Carrier) → ++ₛ ⟨$⟩ (xs , ys) ≈ ++ₛ ⟨$⟩ (ys , xs) ++ₛ-comm {Aₛ} xs ys = ++-comm Aₛ xs ys + +module _ (M : CommutativeMonoid c ℓ) where + + open CommutativeMonoid M renaming (setoid to Mₛ) + + opaque + unfolding Multiset List.fold-cong + fold : ∣ Multisetₛ Mₛ ∣ → ∣ Mₛ ∣ + fold = List.fold monoid -- RawFoldable.fold foldable rawMonoid + + fold-cong + : {xs ys : ∣ Multisetₛ Mₛ ∣} + → (let module [M]ₛ = Setoid (Multisetₛ Mₛ)) + → (xs [M]ₛ.≈ ys) + → fold xs ≈ fold ys + fold-cong (↭.refl x) = cong (List.foldₛ monoid) x + fold-cong (↭.prep x≈y xs↭ys) = ∙-cong x≈y (fold-cong xs↭ys) + fold-cong + {x₀ L.∷ x₁ L.∷ xs} + {y₀ L.∷ y₁ L.∷ ys} + (↭.swap x₀≈y₁ x₁≈y₀ xs↭ys) = trans + (sym (assoc x₀ x₁ (fold xs))) (trans  + (∙-cong (trans (∙-cong x₀≈y₁ x₁≈y₀) (comm y₁ y₀)) (fold-cong xs↭ys)) + (assoc y₀ y₁ (fold ys))) + fold-cong {xs} {ys} (↭.trans xs↭zs zs↭ys) = trans (fold-cong xs↭zs) (fold-cong zs↭ys) + + foldₛ : Multisetₛ Mₛ ⟶ₛ Mₛ + foldₛ .to = fold + foldₛ .cong = fold-cong + + opaque + unfolding fold + ++ₛ-homo + : (xs ys : ∣ Multisetₛ Mₛ ∣) + → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys) + ++ₛ-homo xs ys = ++-homo monoid id xs + + []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε + []ₛ-homo = refl + +module _ (M N : CommutativeMonoid c ℓ) where + + module M = CommutativeMonoid M + module N = CommutativeMonoid N + + opaque + unfolding fold + + fold-mapₛ + : (f : M.setoid ⟶ₛ N.setoid) + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f) + → {xs : ∣ Multisetₛ M.setoid ∣} + → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs) + fold-mapₛ = List.fold-mapₛ M.monoid N.monoid diff --git a/Functor/Forgetful/Instance/CMonoid.agda b/Functor/Forgetful/Instance/CMonoid.agda new file mode 100644 index 0000000..fd8ecc1 --- /dev/null +++ b/Functor/Forgetful/Instance/CMonoid.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Level using (Level) + +module Functor.Forgetful.Instance.CMonoid + {o ℓ e : Level} + {S : Category o ℓ e} + {monoidal : Monoidal S} + (symmetric : Symmetric monoidal) + where + +open import Categories.Category.Construction.Monoids monoidal using (Monoids) +open import Categories.Functor using (Functor) +open import Category.Construction.CMonoids symmetric using (CMonoids) +open import Function using (id) +open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒) + +private + module S = Category S + +open CommutativeMonoid +open CommutativeMonoid⇒ +open Functor +open S.Equiv using (refl) + +Forget : Functor CMonoids Monoids +Forget .F₀ = monoid +Forget .F₁ = monoid⇒ +Forget .identity = refl +Forget .homomorphism = refl +Forget .F-resp-≈ = id + +module Forget = Functor Forget -- cgit v1.2.3