diff options
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) |