2 files changed, 70 insertions, 2 deletions
diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda
index 8bf567d..ebb3dc0 100644
--- a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda
+++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda
@@ -5,7 +5,7 @@ module Functor.Free.Instance.SymmetricMonoidalPreorder.Lax where
 import Functor.Free.Instance.MonoidalPreorder.Lax as MP
 
 open import Categories.Category using (Category)
-open import Category.Instance.SymMonCat using (SymMonCat)
+open import Category.Instance.SymMonCat using (module Lax)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁)
@@ -54,7 +54,7 @@ module _ {o ℓ e : Level} where
         → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G
     pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋
 
-Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ)
+Free : {o ℓ e : Level} → Functor (Lax.SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ)
 Free = record
     { F₀ = symmetricMonoidalPreorder
     ; F₁ = symmetricMonoidalMonotone
diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda
new file mode 100644
index 0000000..f759f17
--- /dev/null
+++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Strong.agda
@@ -0,0 +1,68 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Free.Instance.SymmetricMonoidalPreorder.Strong where
+
+import Functor.Free.Instance.MonoidalPreorder.Strong as MP
+
+open import Categories.Category using (Category)
+open import Category.Instance.SymMonCat using (module Strong)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Monoidal.Symmetric using () renaming (module Strong to Strong₁)
+open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-StrongSymmetricMonoidal)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Strong to Strong₂)
+open import Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Strong using (SymMonPre; _≃_; module ≃)
+open import Data.Product using (_,_)
+open import Level using (Level)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (SymmetricMonoidalMonotone)
+
+open Strong₁ using (SymmetricMonoidalFunctor)
+open Strong₂ using (SymmetricMonoidalNaturalIsomorphism)
+ 
+-- The free symmetric monoidal preorder of a symmetric monoidal category
+
+module _ {o ℓ e : Level} where
+
+  symmetricMonoidalPreorder : SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalPreorder o ℓ
+  symmetricMonoidalPreorder C = record
+      { M
+      ; symmetric = record
+          { symmetric = λ x y → braiding.⇒.η (x , y)
+          }
+      }
+    where
+      open SymmetricMonoidalCategory C
+      module M = MonoidalPreorder (MP.Free.₀ monoidalCategory)
+
+  module _ {A B : SymmetricMonoidalCategory o ℓ e} where
+
+    symmetricMonoidalMonotone
+        : SymmetricMonoidalFunctor A B
+        → SymmetricMonoidalMonotone (symmetricMonoidalPreorder A) (symmetricMonoidalPreorder B)
+    symmetricMonoidalMonotone F = record
+        { monoidalMonotone = MP.Free.₁ F.monoidalFunctor
+        }
+      where
+        module F = SymmetricMonoidalFunctor F
+
+    open SymmetricMonoidalNaturalIsomorphism using (⌊_⌋)
+
+    pointwiseIsomorphism
+        : {F G : SymmetricMonoidalFunctor A B}
+        → SymmetricMonoidalNaturalIsomorphism F G
+        → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G
+    pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋
+
+Free : {o ℓ e : Level} → Functor (Strong.SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ)
+Free = record
+    { F₀ = symmetricMonoidalPreorder
+    ; F₁ = symmetricMonoidalMonotone
+    ; identity = λ {A} → ≃.refl {A = symmetricMonoidalPreorder A} {x = id}
+    ; homomorphism = λ {f = f} {h} → ≃.refl {x = symmetricMonoidalMonotone (∘-StrongSymmetricMonoidal h f)}
+    ; F-resp-≈ = pointwiseIsomorphism
+    }
+  where
+    open Category (SymMonPre _ _) using (id)
+
+module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})