diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-04-30 13:56:37 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-04-30 13:56:37 -0500 |
| commit | be685059304423e5a5cbb176b44aef1a4a76325b (patch) | |
| tree | 5fa7f6d64eb428e0edffab0467a14afea0b922d2 /Data/CMonoid.agda | |
| parent | e4ab2f40d7713d871bae5e23f6f81ea5eb9d2de2 (diff) | |
Add monoids / monoid objects in setoids equivalencemain
Diffstat (limited to 'Data/CMonoid.agda')
| -rw-r--r-- | Data/CMonoid.agda | 5 |
1 files changed, 2 insertions, 3 deletions
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) |