Add SMP to commutative monoids functor

3 files changed, 69 insertions, 2 deletions

diff --git a/Functor/Free/Instance/InducedCMonoid.agda b/Functor/Free/Instance/InducedCMonoid.agda
new file mode 100644
index 0000000..be913d6
--- /dev/null
+++ b/Functor/Free/Instance/InducedCMonoid.agda
@@ -0,0 +1,67 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Functor.Free.Instance.InducedCMonoid {c ℓ : Level} where
+
+-- The induced commutative monoid of a symmetric monoidal preorder
+
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+
+open import Categories.Functor using (Functor)
+open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid)
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Strong using (SymMonPre)
+open import Data.Product using (_,_)
+open import Data.Setoid using (∣_∣)
+open import Function.Construct.Setoid using (_∙_)
+open import Functor.Free.Instance.InducedMonoid using (μ) renaming (module InducedMonoid to IM)
+open import Functor.Free.Instance.InducedSetoid using () renaming (module InducedSetoid to IS)
+open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
+open import Preorder.Primitive using (module Isomorphism)
+open import Preorder.Primitive.Monoidal using (SymmetricMonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (SymmetricMonoidalMonotone)
+
+open Setoids-× using (_⊗₀_; _⊗₁_; _≈_; module braiding)
+
+module _ (P : SymmetricMonoidalPreorder c ℓ) where
+
+  open SymmetricMonoidalPreorder P
+
+  private module M = Monoid (IM.₀ monoidalPreorder)
+
+  opaque
+    unfolding μ
+    commutative : M.μ ≈ M.μ ∙ braiding.⇒.η (IS.₀ U , IS.₀ U)
+    commutative {x , y} = record { from = symmetry x y ; to = symmetry y x }
+
+  ≅-cmonoid : CommutativeMonoid
+  ≅-cmonoid = record
+      { M
+      ; isCommutativeMonoid = record
+          { M
+          ; commutative = commutative
+          }
+      }
+
+cmonoid⇒
+    : {A B : SymmetricMonoidalPreorder c ℓ}
+    → SymmetricMonoidalMonotone A B
+    → CommutativeMonoid⇒ (≅-cmonoid A) (≅-cmonoid B)
+cmonoid⇒ f = let open SymmetricMonoidalMonotone f in record
+    { monoid⇒ = IM.₁ monoidalMonotone
+    }
+
+InducedCMonoid : Functor (SymMonPre c ℓ) CMonoids
+InducedCMonoid = record
+    { F₀ = ≅-cmonoid
+    ; F₁ = cmonoid⇒
+    ; identity = λ {A} {x} → ≅.refl (U A)
+    ; homomorphism = λ {Z = Z} → ≅.refl (U Z)
+    ; F-resp-≈ = λ f≃g {x} → f≃g x
+    }
+  where
+    open SymmetricMonoidalPreorder using (U)
+    open Isomorphism using (module ≅)
+
+module InducedCMonoid = Functor InducedCMonoid
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