From 90ac9b57675007dbd7f4e680fb6b7bfb51dd2489 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 29 Aug 2025 14:38:29 +0200 Subject: [PATCH 1/2] [bug] fix "wrong" argument to projection --- src/Algebra/Morphism/Construct/DirectProduct.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 4892036eeb0f6a8c3b6c608ddc50855cff7c4865 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 5 Oct 2025 11:58:14 +0100 Subject: [PATCH 2/2] add: note on bug fix to `CHANGELOG` --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) 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 --------------------------------