[bug] replace wrong argument to projection in Algebra.Morphism.Construct.DirectProduct (#2822)

* [bug] fix "wrong" argument to projection

* add: note on bug fix to `CHANGELOG`

---------

Co-authored-by: jamesmckinna <j.mckinna@hw.ac.uk>

Author: carlostome

CHANGELOG.md

@@ -11,6 +11,8 @@ Bug-fixes
 
 * Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`.
 
+* Fix a typo in `Algebra.Morphism.Construct.DirectProduct`.
+
 Non-backwards compatible changes
 --------------------------------
 

src/Algebra/Morphism/Construct/DirectProduct.agda

@@ -133,7 +133,7 @@ module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where
     module N = RawMonoid N
 
   module _ {refl : Reflexive M._≈_} where
-    proj₁ = Proj₁.isMonoidHomomorphism M M refl
+    proj₁ = Proj₁.isMonoidHomomorphism M N refl
 
   module _ {refl : Reflexive N._≈_} where
     proj₂ = Proj₂.isMonoidHomomorphism M N refl