Update circuit values

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