From be685059304423e5a5cbb176b44aef1a4a76325b Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 30 Apr 2026 13:56:37 -0500 Subject: Add monoids / monoid objects in setoids equivalence --- Adjoint/Instance/Multiset.agda | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'Adjoint/Instance/Multiset.agda') diff --git a/Adjoint/Instance/Multiset.agda b/Adjoint/Instance/Multiset.agda index c51baa9..5bc46ba 100644 --- a/Adjoint/Instance/Multiset.agda +++ b/Adjoint/Instance/Multiset.agda @@ -16,6 +16,7 @@ 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 Algebra.Morphism.Bundles using (MonoidHomomorphism) open import Categories.Adjoint using (_⊣_) open import Categories.Category using (Category) open import Categories.Functor using (Functor; id; _∘F_) @@ -24,7 +25,7 @@ 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.Product using (_,_) open import Data.Setoid using (∣_∣) open import Function using (_⟶ₛ_; _⟨$⟩_) open import Functor.Free.Instance.CMonoid {ℓ} {ℓ} using (Multisetₘ; mapₘ; MultisetCMonoid) renaming (Free to Free′) @@ -78,7 +79,9 @@ opaque → (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) + fold-mapₘ {X} {Y} f = fold-mapₛ (toCMonoid X) (toCMonoid Y) (record { cong = ⟦⟧-cong }) isMonoidHomomorphism + where + open MonoidHomomorphism (toCMonoid⇒ X Y f) counit : NaturalTransformation (Free ∘F Forget) id counit = ntHelper record -- cgit v1.2.3