diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..f6526de846 100644 --- a/CHANGELOG.md +++ b/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 -------------------------------- diff --git a/src/Algebra/Morphism/Construct/DirectProduct.agda b/src/Algebra/Morphism/Construct/DirectProduct.agda index 4c69593499..09bf528a16 100644 --- a/src/Algebra/Morphism/Construct/DirectProduct.agda +++ b/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