Category of decorated cospans is symmetric monoidal

4 files changed, 241 insertions, 210 deletions

diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda
index 0847165..2766df2 100644
--- a/Category/Instance/FinitelyCocompletes.agda
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -62,6 +62,7 @@ _×_ 𝒞 𝒟 = record
   where
     module 𝒞 = FinitelyCocompleteCategory 𝒞
     module 𝒟 = FinitelyCocompleteCategory 𝒟
+{-# INJECTIVE_FOR_INFERENCE _×_ #-}
 
 module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
 
diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda
deleted file mode 100644
index dedfa16..0000000
--- a/Category/Instance/Properties/FinitelyCocompletes.agda
+++ /dev/null
@@ -1,210 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level)
-module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where
-
-import Categories.Morphism.Reasoning as ⇒-Reasoning
-
-open import Categories.Category.BinaryProducts using (BinaryProducts)
-open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
-open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_)
-open import Categories.Diagram.Coequalizer using (IsCoequalizer)
-open import Categories.Functor.Core using (Functor)
-open import Categories.Functor using (_∘F_) renaming (id to idF)
-open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct)
-open import Categories.Object.Initial using (IsInitial)
-open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
-open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_)
-open import Data.Product.Base using (_,_) renaming (_×_ to _×′_)
-open import Functor.Exact using (IsRightExact; RightExactFunctor)
-open import Level using (_⊔_; suc)
-
-FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
-FinitelyCocompletes-CC = record
-    { U = FinitelyCocompletes
-    ; cartesian = FinitelyCocompletes-Cartesian
-    }
-
-module FinCoCom = CartesianCategory FinitelyCocompletes-CC
-open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) --  hiding (unique)
-
-module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
-
-  private
-    module 𝒞 = FinitelyCocompleteCategory 𝒞
-    module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞)
-
-  open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-)
-  open Equiv
-
-  private
-    module -+- = Functor -+-
-
-  +-resp-⊥
-      : {(A , B) : 𝒞×𝒞.Obj}
-      → IsInitial 𝒞×𝒞.U (A , B)
-      → IsInitial 𝒞.U (A + B)
-  +-resp-⊥ {A , B} A,B-isInitial = record
-      { ! = [ A-isInitial.! , B-isInitial.! ]
-      ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) }
-      }
-    where
-      open IsRightExact
-      open RightExactFunctor
-      module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial)
-      module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial)
-
-  +-resp-+
-      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
-        {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)}
-        {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
-      → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂)
-      → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂)
-  +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record
-      { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂  , h₂ ∘ i₂ ] ] }
-      ; inject₁ = inject₁
-      ; inject₂ = inject₂
-      ; unique = unique
-      }
-    where
-      open IsRightExact
-      open RightExactFunctor
-      module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct))
-      module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct))
-      open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂)
-      open 𝒞 using (Obj; _≈_; module HomReasoning; assoc)
-      open HomReasoning
-      open ⇒-Reasoning 𝒞.U
-      inject₁
-          : {X : Obj}
-            {h₁ : A₁ + A₂ ⇒ X}
-            {h₂ : B₁ + B₂ ⇒ X}
-          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁
-      inject₁ {_} {h₁} {h₂} = begin
-          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂)  ≈⟨ []∘+₁ ⟩
-          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ]     ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩
-          [ h₁ ∘ i₁ , h₁ ∘ i₂ ]                                                               ≈⟨ +-g-η ⟩
-          h₁                                                                                  ∎
-      inject₂
-          : {X : Obj}
-            {h₁ : A₁ + A₂ ⇒ X}
-            {h₂ : B₁ + B₂ ⇒ X}
-          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂
-      inject₂ {_} {h₁} {h₂} = begin
-          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂)  ≈⟨ []∘+₁ ⟩
-          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ]     ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩
-          [ h₂ ∘ i₁ , h₂ ∘ i₂ ]                                                               ≈⟨ +-g-η ⟩
-          h₂                                                                                  ∎
-      unique
-          : {X : Obj}
-            {i : C₁ + C₂ ⇒ X}
-            {h₁ : A₁ + A₂ ⇒ X}
-            {h₂ : B₁ + B₂ ⇒ X}
-            (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁)
-            (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂)
-          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i
-      unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin
-          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩
-          [ i ∘ i₁ , i ∘ i₂ ]                                               ≈⟨ +-g-η ⟩
-          i                                                                 ∎
-        where
-          eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁
-          eq₁-₁ = begin
-              (i ∘ i₁) ∘ i₁-₁         ≈⟨ pushʳ +₁∘i₁ ⟨
-              i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩
-              h₁ ∘ i₁                 ∎
-          eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁
-          eq₂-₁ = begin
-              (i ∘ i₁) ∘ i₂-₁         ≈⟨ pushʳ +₁∘i₁ ⟨
-              i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩
-              h₂ ∘ i₁                 ∎
-          eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂
-          eq₁-₂ = begin
-              (i ∘ i₂) ∘ i₁-₂         ≈⟨ pushʳ +₁∘i₂ ⟨
-              i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩
-              h₁ ∘ i₂                 ∎
-          eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂
-          eq₂-₂ = begin
-              (i ∘ i₂) ∘ i₂-₂         ≈⟨ pushʳ +₁∘i₂ ⟨
-              i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩
-              h₂ ∘ i₂                 ∎
-
-  +-resp-coeq
-      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
-        {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)}
-        {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
-      → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂)
-      → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂)
-  +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record
-      { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism
-      ; coequalize = coequalize
-      ; universal = universal _
-      ; unique = uniq _
-      }
-    where
-      open IsRightExact
-      open RightExactFunctor
-      module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq)
-      module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq)
-      open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η)
-      open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc)
-      open 𝒞.HomReasoning
-      open ⇒-Reasoning 𝒞.U
-
-      module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where
-
-        eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁
-        eq₁ = begin
-            (k ∘ i₁) ∘ f₁       ≈⟨ pushʳ +₁∘i₁ ⟨
-            k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩
-            k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩
-            (k ∘ i₁) ∘ g₁       ∎
-
-        eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂
-        eq₂ = begin
-            (k ∘ i₂) ∘ f₂       ≈⟨ pushʳ +₁∘i₂ ⟨
-            k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩
-            k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩
-            (k ∘ i₂) ∘ g₂       ∎
-
-        coequalize : C₁ + C₂ ⇒ X
-        coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ]
-
-        universal : k ≈ coequalize ∘ (h₁ +₁ h₂)
-        universal = begin
-            k                                                         ≈⟨ +-g-η ⟨
-            [ k ∘ i₁ , k ∘ i₂ ]                                       ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩
-            [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨
-            coequalize ∘ (h₁ +₁ h₂)                                   ∎
-
-        uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize
-        uniq {i} eq′ = begin
-            i                   ≈⟨ +-g-η ⟨
-            [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩
-            [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎
-          where
-            eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁
-            eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁
-            eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂
-            eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂
-
-module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
-
-  open FinCoCom using (_⇒_; _∘_; id)
-  module 𝒞 = FinitelyCocompleteCategory 𝒞
-
-  -+- : 𝒞 × 𝒞 ⇒ 𝒞
-  -+- = record
-      { F = 𝒞.-+-
-      ; isRightExact = record
-          { F-resp-⊥ = +-resp-⊥ 𝒞
-          ; F-resp-+ = +-resp-+ 𝒞
-          ; F-resp-coeq = +-resp-coeq 𝒞
-          }
-      }
-
-  [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
-  [x+y]+z = -+- ∘ (-+- ×₁ id)
-
-  x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
-  x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ
diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda
new file mode 100644
index 0000000..fa15295
--- /dev/null
+++ b/Category/Instance/Properties/SymMonCat.agda
@@ -0,0 +1,166 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Level using (Level; suc; _⊔_)
+module Category.Instance.Properties.SymMonCat {o ℓ e : Level} where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI
+import Categories.Functor.Monoidal.Symmetric {o} {o} {ℓ} {ℓ} {e} {e} as SMF
+
+open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat)
+
+open import Categories.Category using (Category; _[_≈_]; _[_∘_])
+open import Categories.Object.Product.Core SymMonCat using (Product)
+open import Categories.Object.Terminal SymMonCat using (Terminal)
+open import Categories.Category.Instance.One using (One)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Cartesian SymMonCat using (Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
+open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts)
+open import Categories.Functor.Monoidal.Construction.Product
+  using ()
+  renaming
+    ( πˡ-SymmetricMonoidalFunctor to πˡ-SMF
+    ; πʳ-SymmetricMonoidalFunctor to πʳ-SMF
+    ; ※-SymmetricMonoidalFunctor to ※-SMF
+    )
+open import Categories.Category.Monoidal.Construction.Product using (Product-SymmetricMonoidalCategory)
+open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+
+open SMF.Lax using (SymmetricMonoidalFunctor)
+open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
+
+module Cone
+  {A B X : SymmetricMonoidalCategory o ℓ e}
+  {F : SymmetricMonoidalFunctor X A}
+  {G : SymmetricMonoidalFunctor X B} where
+
+  module A = SymmetricMonoidalCategory A
+  module B = SymmetricMonoidalCategory B
+  module X = SymmetricMonoidalCategory X
+  module F = SymmetricMonoidalFunctor X A F
+  module G = SymmetricMonoidalFunctor X B G
+
+  A×B : SymmetricMonoidalCategory o ℓ e
+  A×B = (Product-SymmetricMonoidalCategory A B)
+
+  πˡ : SymmetricMonoidalFunctor A×B A
+  πˡ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+
+  πʳ : SymmetricMonoidalFunctor A×B B
+  πʳ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+
+  module _ where
+    open Category A.U
+    open Equiv
+    open ⇒-Reasoning A.U
+    open ⊗-Reasoning A.monoidal
+    project₁ : SymMonCat [ SymMonCat [ πˡ ∘ ※-SMF F G ] ≈ F ]
+    project₁ = record
+        { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F}
+        ; F⇒G-isMonoidal = record
+            { ε-compat = identityˡ ○ identityʳ
+            ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym A.⊗.identity }
+            }
+        }
+    module _ (H : SymmetricMonoidalFunctor X A×B) (eq₁ : SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]) where
+      private
+        module H = SymmetricMonoidalFunctor X A×B H
+      open SymmetricMonoidalNaturalIsomorphism eq₁
+      ε-compat₁ : ⇐.η X.unit A.∘ F.ε A.≈ H.ε .proj₁
+      ε-compat₁ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ
+      ⊗-homo-compat₁
+          : ∀ {C D}
+          → ⇐.η (X.⊗.₀ (C , D)) ∘ F.⊗-homo.η (C , D)
+          ≈ H.⊗-homo.η (C , D) .proj₁ ∘ A.⊗.₁ (⇐.η C , ⇐.η D)
+      ⊗-homo-compat₁ {C} {D} =
+          insertʳ
+              (sym ⊗-distrib-over-∘
+              ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D
+              ○ A.⊗.identity)
+          ○ (pullʳ (sym ⊗-homo-compat)
+            ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D)))
+            ○ identityʳ) ⟩∘⟨refl
+
+  module _ where
+    open Category B.U
+    open Equiv
+    open ⇒-Reasoning B.U
+    open ⊗-Reasoning B.monoidal
+    project₂ : SymMonCat [ SymMonCat [ πʳ ∘ ※-SMF F G ] ≈ G ]
+    project₂ = record
+        { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F}
+        ; F⇒G-isMonoidal = record
+            { ε-compat = identityˡ ○ identityʳ
+            ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym B.⊗.identity }
+            }
+        }
+    module _ (H : SymmetricMonoidalFunctor X A×B) (eq₂ : SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]) where
+      private
+        module H = SymmetricMonoidalFunctor X A×B H
+      open SymmetricMonoidalNaturalIsomorphism eq₂
+      ε-compat₂ : ⇐.η X.unit ∘ G.ε ≈ H.ε .proj₂
+      ε-compat₂ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ
+      ⊗-homo-compat₂
+          : ∀ {C D}
+          → ⇐.η (X.⊗.₀ (C , D)) ∘ G.⊗-homo.η (C , D)
+          ≈ H.⊗-homo.η (C , D) .proj₂ ∘ B.⊗.₁ (⇐.η C , ⇐.η D)
+      ⊗-homo-compat₂ {C} {D} =
+          insertʳ
+              (sym ⊗-distrib-over-∘
+              ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D
+              ○ B.⊗.identity)
+          ○ (pullʳ (sym ⊗-homo-compat)
+            ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D)))
+            ○ identityʳ) ⟩∘⟨refl
+
+  unique
+      : (H : SymmetricMonoidalFunctor X A×B)
+      → SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]
+      → SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]
+      → SymMonCat [ ※-SMF F G ≈ H ]
+  unique H eq₁ eq₂ = record
+      { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} {H.F} eq₁.U eq₂.U
+      ; F⇒G-isMonoidal = record
+          { ε-compat = ε-compat₁ H eq₁ , ε-compat₂ H eq₂
+          ; ⊗-homo-compat = ⊗-homo-compat₁ H eq₁ , ⊗-homo-compat₂ H eq₂
+          }
+      }
+    where
+      module H = SymmetricMonoidalFunctor X A×B H
+      module eq₁ = SymmetricMonoidalNaturalIsomorphism eq₁
+      module eq₂ = SymmetricMonoidalNaturalIsomorphism eq₂
+
+prod-SymMonCat : ∀ {A B} → Product A B
+prod-SymMonCat {A} {B} = record
+    { A×B = Product-SymmetricMonoidalCategory A B
+    ; π₁ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+    ; π₂ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+    ; ⟨_,_⟩ = ※-SMF
+    ; project₁ = λ { {X} {f} {g} → Cone.project₁ {A} {B} {X} {f} {g} }
+    ; project₂ = λ { {X} {f} {g} → Cone.project₂ {A} {B} {X} {f} {g} }
+    ; unique = λ { {X} {h} {f} {g} eq₁ eq₂ → Cone.unique {A} {B} {X} {f} {g} h eq₁ eq₂ }
+    }
+
+SymMonCat-BinaryProducts : BinaryProducts
+SymMonCat-BinaryProducts = record { product = prod-SymMonCat }
+
+SymMonCat-Terminal : Terminal
+SymMonCat-Terminal = record
+    { ⊤ = record
+        { U = One
+        ; monoidal = _
+        ; symmetric = _
+        }
+    ; ⊤-is-terminal = _
+    }
+
+SymMonCat-Cartesian : Cartesian
+SymMonCat-Cartesian = record
+    { terminal = SymMonCat-Terminal
+    ; products = SymMonCat-BinaryProducts
+    }
diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda
new file mode 100644
index 0000000..e4b136c
--- /dev/null
+++ b/Category/Instance/SymMonCat.agda
@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Level using (Level; suc; _⊔_)
+module Category.Instance.SymMonCat {o ℓ e : Level} where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Functor.Monoidal.Symmetric as SMF
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Morphism as Morphism
+import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI
+import Categories.Category.Monoidal.Utilities as MonoidalUtil
+import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
+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.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 }
+    }