1 files changed, 77 insertions, 0 deletions
diff --git a/Functor/Free/Instance/MonoidalPreorder/Strong.agda b/Functor/Free/Instance/MonoidalPreorder/Strong.agda
new file mode 100644
index 0000000..612e91c
--- /dev/null
+++ b/Functor/Free/Instance/MonoidalPreorder/Strong.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Free.Instance.MonoidalPreorder.Strong where
+
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+import Functor.Free.Instance.Preorder as Preorder
+
+open import Categories.Category using (Category)
+open import Categories.Category.Instance.Monoidals using (StrongMonoidals)
+open import Categories.Category.Monoidal using (MonoidalCategory)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
+open import Categories.Functor.Monoidal.Properties using (∘-StrongMonoidal)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal using (module Strong)
+open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (_≃_; module ≃) renaming (Monoidals to Monoidalsₚ)
+open import Data.Product using (_,_)
+open import Level using (Level)
+open import Preorder.Primitive using (module Isomorphism)
+open import Preorder.Primitive.MonotoneMap using (MonotoneMap)
+open import Preorder.Primitive.Monoidal using (MonoidalPreorder)
+open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone)
+
+open Strong using (MonoidalNaturalIsomorphism)
+ 
+-- The free monoidal preorder of a monoidal category
+
+module _ {o ℓ e : Level} where
+
+  monoidalPreorder : MonoidalCategory o ℓ e → MonoidalPreorder o ℓ
+  monoidalPreorder C = record
+      { U = Preorder.Free.₀ U
+      ; monoidal = record
+          { unit = unit
+          ; tensor = Preorder.Free.₁ ⊗
+          ; unitaryˡ = Preorder.Free.F-resp-≈ unitorˡ-naturalIsomorphism
+          ; unitaryʳ = Preorder.Free.F-resp-≈ unitorʳ-naturalIsomorphism
+          ; associative = λ x y z → record
+              { from = associator.from {x} {y} {z}
+              ; to = associator.to {x} {y} {z}
+              }
+          }
+      }
+    where
+      open MonoidalCategory C
+      open ⊗-Util monoidal
+
+  module _ {A B : MonoidalCategory o ℓ e} where
+
+    monoidalMonotone : StrongMonoidalFunctor A B → MonoidalMonotone (monoidalPreorder A) (monoidalPreorder B)
+    monoidalMonotone F = record
+        { F = Preorder.Free.₁ F.F
+        ; ε = record { F.ε }
+        ; ⊗-homo = λ p₁ p₂ → Preorder.Free.F-resp-≈ F.⊗-homo (p₁ , p₂)
+        }
+      where
+        module F = StrongMonoidalFunctor F
+
+    open MonoidalNaturalIsomorphism using (U)
+
+    pointwiseIsomorphism
+        : {F G : StrongMonoidalFunctor A B}
+        → MonoidalNaturalIsomorphism F G
+        → monoidalMonotone F ≃ monoidalMonotone G
+    pointwiseIsomorphism F≃G = Preorder.Free.F-resp-≈ (U F≃G)
+
+Free : {o ℓ e : Level} → Functor (StrongMonoidals o ℓ e) (Monoidalsₚ o ℓ)
+Free = record
+    { F₀ = monoidalPreorder
+    ; F₁ = monoidalMonotone
+    ; identity = λ {A} → ≃.refl {A = monoidalPreorder A} {x = id}
+    ; homomorphism = λ {f = f} {h} → ≃.refl {x = monoidalMonotone (∘-StrongMonoidal h f)}
+    ; F-resp-≈ = pointwiseIsomorphism
+    }
+  where
+    open Category (Monoidalsₚ _ _) using (id)
+
+module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})