From fc941b6d2e2293d9d9e096519eac708ae3b0aa0a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 7 Jan 2026 11:41:01 -0600 Subject: Add SMP to commutative monoids functor --- Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda') diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda index f759f17..4eb3ad5 100644 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda @@ -28,7 +28,7 @@ module _ {o ℓ e : Level} where symmetricMonoidalPreorder C = record { M ; symmetric = record - { symmetric = λ x y → braiding.⇒.η (x , y) + { symmetry = λ x y → braiding.⇒.η (x , y) } } where -- cgit v1.2.3