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/List.agda | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'Adjoint/Instance/List.agda') diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda index 1b65985..6837c8d 100644 --- a/Adjoint/Instance/List.agda +++ b/Adjoint/Instance/List.agda @@ -12,6 +12,7 @@ open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoi module S = SymmetricMonoidalCategory Setoids-× +open import Algebra.Morphism.Bundles using (MonoidHomomorphism) open import Categories.Adjoint using (_⊣_) open import Categories.Category.Construction.Monoids using (Monoids) open import Categories.Functor using (Functor; id; _∘F_) @@ -19,7 +20,7 @@ open import Categories.NaturalTransformation using (NaturalTransformation; ntHel open import Categories.Object.Monoid S.monoidal using (Monoid; IsMonoid; Monoid⇒) open import Data.Monoid using (toMonoid; toMonoid⇒) open import Data.Opaque.List using ([-]ₛ; Listₛ; mapₛ; 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.Forgetful.Instance.Monoid {suc ℓ} {ℓ} {ℓ} using () renaming (Forget to Forget′) @@ -70,10 +71,12 @@ opaque : {X Y : Monoid} (f : Monoid⇒ X Y) {x : ∣ Listₛ (Carrier X) ∣} - → (open Setoid (Carrier Y)) + (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ₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f) + fold-mapₘ {X} {Y} f = fold-mapₛ (toMonoid X) (toMonoid Y) (record { cong = ⟦⟧-cong }) isMonoidHomomorphism + where + open MonoidHomomorphism (toMonoid⇒ X Y f) counit : NaturalTransformation (Free ∘F Forget) id counit = ntHelper record -- cgit v1.2.3