diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 11:41:01 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 11:41:01 -0600 |
| commit | fc941b6d2e2293d9d9e096519eac708ae3b0aa0a (patch) | |
| tree | efa253dd238ba7484c958099078d6f267b059bea /Preorder/Primitive | |
| parent | 4326ca8d5b9386a480303418fb3e57b9054213f0 (diff) | |
Add SMP to commutative monoids functor
Diffstat (limited to 'Preorder/Primitive')
| -rw-r--r-- | Preorder/Primitive/Monoidal.agda | 2 |
1 files changed, 1 insertions, 1 deletions
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 |