From fc941b6d2e2293d9d9e096519eac708ae3b0aa0a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 7 Jan 2026 11:41:01 -0600
Subject: Add SMP to commutative monoids functor

---
 Preorder/Primitive/Monoidal.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Preorder')

diff --git a/Preorder/Primitive/Monoidal.agda b/Preorder/Primitive/Monoidal.agda
index af57b70..86c6b25 100644
--- a/Preorder/Primitive/Monoidal.agda
+++ b/Preorder/Primitive/Monoidal.agda
@@ -52,7 +52,7 @@ record Symmetric {c ℓ : Level} {P : Preorder c ℓ} (M : Monoidal P) : Set (c
   open Preorder P
 
   field
-    symmetric : (x y : Carrier) → x ⊗ y ≲ y ⊗ x
+    symmetry : (x y : Carrier) → x ⊗ y ≲ y ⊗ x
 
 record MonoidalPreorder (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where
 
-- 
cgit v1.2.3