Add strong variants of cats to preorders functors

4 files changed, 265 insertions, 58 deletions

diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda
index 814abeb..6693639 100644
--- a/Category/Instance/SymMonCat.agda
+++ b/Category/Instance/SymMonCat.agda
@@ -16,59 +16,121 @@ open import Relation.Binary.Core using (Rel)
 open import Categories.Category using (Category; _[_,_]; _[_∘_])
 open import Categories.Category.Helper using (categoryHelper)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
-
-open SMF.Lax using (SymmetricMonoidalFunctor)
-open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
-
-assoc
-    : {A B C D : SymmetricMonoidalCategory o ℓ e}
-      {F : SymmetricMonoidalFunctor A B}
-      {G : SymmetricMonoidalFunctor B C}
-      {H : SymmetricMonoidalFunctor C D}
-    → SymmetricMonoidalNaturalIsomorphism
-        (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F)
-        (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F))
-assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H}
-
-identityˡ
-    : {A B : SymmetricMonoidalCategory o ℓ e}
-      {F : SymmetricMonoidalFunctor A B}
-    → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F
-identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
-
-identityʳ
-    : {A B : SymmetricMonoidalCategory o ℓ e}
-      {F : SymmetricMonoidalFunctor A B}
-    → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F
-identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
-
-Compose
-    : {A B C : SymmetricMonoidalCategory o ℓ e}
-    → SymmetricMonoidalFunctor B C
-    → SymmetricMonoidalFunctor A B
-    → SymmetricMonoidalFunctor A C
-Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G
-
-∘-resp-≈
-    : {A B C : SymmetricMonoidalCategory o ℓ e}
-      {f h : SymmetricMonoidalFunctor B C}
-      {g i : SymmetricMonoidalFunctor A B}
-    → SymmetricMonoidalNaturalIsomorphism f h
-    → SymmetricMonoidalNaturalIsomorphism g i
-    → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i)
-∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′
-
-SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
-SymMonCat = categoryHelper record
-    { Obj = SymmetricMonoidalCategory o ℓ e
-    ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e}
-    ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} }
-    ; id = λ { {X} → idF-SymmetricMonoidal X }
-    ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G }
-    ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} }
-    ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} }
-    ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} }
-    ; equiv = isEquivalence
-    ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i }
-    }
+open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; idF-StrongSymmetricMonoidal; ∘-SymmetricMonoidal; ∘-StrongSymmetricMonoidal)
+
+
+-- Category of symmetric monoidal categories and lax symmetric monoidal functors
+
+module Lax where
+
+  open SMF.Lax using (SymmetricMonoidalFunctor)
+  open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
+
+  assoc
+      : {A B C D : SymmetricMonoidalCategory o ℓ e}
+        {F : SymmetricMonoidalFunctor A B}
+        {G : SymmetricMonoidalFunctor B C}
+        {H : SymmetricMonoidalFunctor C D}
+      → SymmetricMonoidalNaturalIsomorphism
+          (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F)
+          (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F))
+  assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H}
+
+  identityˡ
+      : {A B : SymmetricMonoidalCategory o ℓ e}
+        {F : SymmetricMonoidalFunctor A B}
+      → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F
+  identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
+
+  identityʳ
+      : {A B : SymmetricMonoidalCategory o ℓ e}
+        {F : SymmetricMonoidalFunctor A B}
+      → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F
+  identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
+
+  Compose
+      : {A B C : SymmetricMonoidalCategory o ℓ e}
+      → SymmetricMonoidalFunctor B C
+      → SymmetricMonoidalFunctor A B
+      → SymmetricMonoidalFunctor A C
+  Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G
+
+  ∘-resp-≈
+      : {A B C : SymmetricMonoidalCategory o ℓ e}
+        {f h : SymmetricMonoidalFunctor B C}
+        {g i : SymmetricMonoidalFunctor A B}
+      → SymmetricMonoidalNaturalIsomorphism f h
+      → SymmetricMonoidalNaturalIsomorphism g i
+      → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i)
+  ∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′
+
+  SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+  SymMonCat = categoryHelper record
+      { Obj = SymmetricMonoidalCategory o ℓ e
+      ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e}
+      ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} }
+      ; id = λ { {X} → idF-SymmetricMonoidal X }
+      ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G }
+      ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} }
+      ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} }
+      ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} }
+      ; equiv = isEquivalence
+      ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i }
+      }
+
+module Strong where
+
+  open SMF.Strong using (SymmetricMonoidalFunctor)
+  open SMNI.Strong using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
+
+  assoc
+      : {A B C D : SymmetricMonoidalCategory o ℓ e}
+        {F : SymmetricMonoidalFunctor A B}
+        {G : SymmetricMonoidalFunctor B C}
+        {H : SymmetricMonoidalFunctor C D}
+      → SymmetricMonoidalNaturalIsomorphism
+          (∘-StrongSymmetricMonoidal (∘-StrongSymmetricMonoidal H G) F)
+          (∘-StrongSymmetricMonoidal H (∘-StrongSymmetricMonoidal G F))
+  assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Strong.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H}
+
+  identityˡ
+      : {A B : SymmetricMonoidalCategory o ℓ e}
+        {F : SymmetricMonoidalFunctor A B}
+      → SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal (idF-StrongSymmetricMonoidal B) F) F
+  identityˡ {A} {B} {F} = SMNI.Strong.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
+
+  identityʳ
+      : {A B : SymmetricMonoidalCategory o ℓ e}
+        {F : SymmetricMonoidalFunctor A B}
+      → SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal F (idF-StrongSymmetricMonoidal A)) F
+  identityʳ {A} {B} {F} = SMNI.Strong.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
+
+  Compose
+      : {A B C : SymmetricMonoidalCategory o ℓ e}
+      → SymmetricMonoidalFunctor B C
+      → SymmetricMonoidalFunctor A B
+      → SymmetricMonoidalFunctor A C
+  Compose {A} {B} {C} F G = ∘-StrongSymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G
+
+  ∘-resp-≈
+      : {A B C : SymmetricMonoidalCategory o ℓ e}
+        {f h : SymmetricMonoidalFunctor B C}
+        {g i : SymmetricMonoidalFunctor A B}
+      → SymmetricMonoidalNaturalIsomorphism f h
+      → SymmetricMonoidalNaturalIsomorphism g i
+      → SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal f g) (∘-StrongSymmetricMonoidal h i)
+  ∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Strong._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′
+
+  SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+  SymMonCat = categoryHelper record
+      { Obj = SymmetricMonoidalCategory o ℓ e
+      ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e}
+      ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} }
+      ; id = λ { {X} → idF-StrongSymmetricMonoidal X }
+      ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G }
+      ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} }
+      ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} }
+      ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} }
+      ; equiv = isEquivalence
+      ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i }
+      }
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})
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})