diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/Instance/Monoids.agda | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Category/Instance/Monoids.agda b/Category/Instance/Monoids.agda index 28f214b..f084b79 100644 --- a/Category/Instance/Monoids.agda +++ b/Category/Instance/Monoids.agda @@ -12,8 +12,10 @@ open import Algebra using (Monoid) open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) open import Relation.Binary using (IsEquivalence) +open import Function using (Func; _⟶ₛ_) open Monoid hiding (_≈_) +open Func record MonoidHomomorphism (M N : Monoid c ℓ) : Set (c ⊔ ℓ) where @@ -24,6 +26,10 @@ record MonoidHomomorphism (M N : Monoid c ℓ) : Set (c ⊔ ℓ) where open Raw.MonoidHomomorphism rawMonoidHomomorphism public + func : setoid M ⟶ₛ setoid N + func .to = ⟦_⟧ + func .cong = ⟦⟧-cong + module _ {M N : Monoid c ℓ} where -- Pointwise equality of monoid homomorphisms |