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 /Functor/Free/Instance/SymmetricMonoidalPreorder | |
| parent | 4326ca8d5b9386a480303418fb3e57b9054213f0 (diff) | |
Add SMP to commutative monoids functor
Diffstat (limited to 'Functor/Free/Instance/SymmetricMonoidalPreorder')
| -rw-r--r-- | Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda | 2 | ||||
| -rw-r--r-- | Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda index ebb3dc0..59161ae 100644 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.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 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 |