1 files changed, 166 insertions, 0 deletions
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
+    }