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 --- Data/CMonoid.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'Data/CMonoid.agda') diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda index dd0277c..4d84921 100644 --- a/Data/CMonoid.agda +++ b/Data/CMonoid.agda @@ -5,7 +5,7 @@ module Data.CMonoid {c ℓ : Level} where import Algebra.Bundles as Alg -open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Algebra.Morphism.Bundles using (MonoidHomomorphism) open import Categories.Object.Monoid using (Monoid) open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′) open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒; module FromMonoid) @@ -63,6 +63,5 @@ module _ (M N : CommutativeMonoid Setoids-×.symmetric) where toCMonoid⇒ : CommutativeMonoid⇒ Setoids-×.symmetric M N - → Σ (M.setoid ⟶ₛ N.setoid) (λ f - → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)) + → MonoidHomomorphism M.rawMonoid N.rawMonoid toCMonoid⇒ f = toMonoid⇒ (monoid M) (monoid N) (monoid⇒ f) -- cgit v1.2.3