From b2c2426959715260f57153b91ce11d12c7fdb298 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 7 Jan 2026 10:52:51 -0600
Subject: Add strong variants of cats to preorders functors

---
 Category/Instance/SymMonCat.agda | 174 ++++++++++++++++++++++++++-------------
 1 file changed, 118 insertions(+), 56 deletions(-)

(limited to 'Category/Instance')

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 }
+      }
-- 
cgit v1.2.3