Category of decorated cospans is symmetric monoidal

1 files changed, 169 insertions, 0 deletions

diff --git a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
new file mode 100644
index 0000000..346999b
--- /dev/null
+++ b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
@@ -0,0 +1,169 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Level using (Level)
+
+module Functor.Cartesian.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o ℓ e : Level} where
+
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Product using (_※_)
+open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor.Cartesian using (CartesianF)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.NaturalTransformation.Core using (ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using (module Lax)
+open import Categories.Object.Product using (IsProduct)
+open import Categories.Object.Terminal using (IsTerminal)
+open import Data.Product.Base using (_,_; <_,_>; proj₁; proj₂)
+
+open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC)
+open import Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using () renaming (Underlying to U)
+
+module CartesianCategory′ {o ℓ e : Level} (C : CartesianCategory o ℓ e) where
+  module CC = CartesianCategory C
+  open import Categories.Object.Terminal using (Terminal)
+  open Terminal CC.terminal public
+  open import Categories.Category.BinaryProducts using (BinaryProducts)
+  open BinaryProducts CC.products public
+  open CC public
+
+module FC = CartesianCategory′ FinitelyCocompletes-CC
+module SMC = CartesianCategory′ SymMonCat-CC
+module U = Functor U
+
+F-resp-⊤ : IsTerminal SMC.U (U.₀ FC.⊤)
+F-resp-⊤ = _
+
+F-resp-× : {A B : FC.Obj} → IsProduct SMC.U (U.₁ (FC.π₁ {A} {B})) (U.₁ (FC.π₂ {A} {B}))
+F-resp-× {A} {B} = record
+    { ⟨_,_⟩ = pairing
+    ; project₁ = λ { {C} {F} {G} → project₁ {C} F G }
+    ; project₂ = λ { {C} {F} {G} → project₂ {C} F G }
+    ; unique = λ { {C} {H} {F} {G} ≃₁ ≃₂ → unique {C} F G H ≃₁ ≃₂ }
+    }
+  where
+    module _ {C : SMC.Obj} (F : Lax.SymmetricMonoidalFunctor C (U.₀ A)) (G : Lax.SymmetricMonoidalFunctor C (U.₀ B)) where
+      module F = Lax.SymmetricMonoidalFunctor F
+      module G = Lax.SymmetricMonoidalFunctor G
+      pairing : Lax.SymmetricMonoidalFunctor C (U.₀ (A FC.× B))
+      pairing = record
+          { F = F.F ※ G.F
+          ; isBraidedMonoidal = record
+              { isMonoidal = record
+                  { ε = F.ε , G.ε
+                  ; ⊗-homo = ntHelper record
+                      { η = < F.⊗-homo.η , G.⊗-homo.η >
+                      ; commute = < F.⊗-homo.commute , G.⊗-homo.commute >
+                      }
+                  ; associativity = F.associativity , G.associativity
+                  ; unitaryˡ = F.unitaryˡ , G.unitaryˡ
+                  ; unitaryʳ = F.unitaryʳ , G.unitaryʳ
+                  }
+              ; braiding-compat = F.braiding-compat , G.braiding-compat
+              }
+          }
+      module pairing = Lax.SymmetricMonoidalFunctor pairing
+      module A = FinitelyCocompleteCategory A
+      module B = FinitelyCocompleteCategory B
+      module C = SymmetricMonoidalCategory C
+      module A′ = SymmetricMonoidalCategory (U.₀ A)
+      module B′ = SymmetricMonoidalCategory (U.₀ B)
+      project₁ : Lax.SymmetricMonoidalNaturalIsomorphism ((U.₁ (FC.π₁ {A} {B})) SMC.∘ pairing) F
+      project₁ = record
+          { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {C.U} {F.F} {G.F}
+          ; F⇒G-isMonoidal = record
+              { ε-compat = ¡-unique₂ (id ∘ F.ε ∘ ¡) F.ε
+              ; ⊗-homo-compat = λ { {X} {Y} → identityˡ ○ refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ) }
+              }
+          }
+        where
+          open FinitelyCocompleteCategory A
+          open HomReasoning
+          open Equiv
+          open ⇒-Reasoning A.U
+      project₂ : Lax.SymmetricMonoidalNaturalIsomorphism (U.₁ {A FC.× B} {B} FC.π₂ SMC.∘ pairing) G
+      project₂ = record
+          { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {C.U} {F.F} {G.F}
+          ; F⇒G-isMonoidal = record
+              { ε-compat = ¡-unique₂ (id ∘ G.ε ∘ ¡) G.ε
+              ; ⊗-homo-compat = λ { {X} {Y} → identityˡ ○ refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ) }
+              }
+          }
+        where
+          open FinitelyCocompleteCategory B
+          open HomReasoning
+          open Equiv
+          open ⇒-Reasoning B.U
+      unique
+          : (H : Lax.SymmetricMonoidalFunctor C (U.F₀ (A FC.× B)))
+          → Lax.SymmetricMonoidalNaturalIsomorphism (U.₁ {A FC.× B} {A} FC.π₁ SMC.∘ H) F
+          → Lax.SymmetricMonoidalNaturalIsomorphism (U.₁ {A FC.× B} {B} FC.π₂ SMC.∘ H) G
+          → Lax.SymmetricMonoidalNaturalIsomorphism pairing H
+      unique H ≃₁ ≃₂ = record
+          { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {C.U} {F.F} {G.F} {H.F} ≃₁.U ≃₂.U
+          ; F⇒G-isMonoidal = record
+              { ε-compat = ε-compat₁ , ε-compat₂
+              ; ⊗-homo-compat =
+                  λ { {X} {Y} → ⊗-homo-compat₁ {X} {Y} , ⊗-homo-compat₂ {X} {Y} }
+              }
+          }
+        where
+          module H = Lax.SymmetricMonoidalFunctor H
+          module ≃₁ = Lax.SymmetricMonoidalNaturalIsomorphism ≃₁
+          module ≃₂ = Lax.SymmetricMonoidalNaturalIsomorphism ≃₂
+          ε-compat₁ : ≃₁.⇐.η C.unit A.∘ F.ε A.≈ proj₁ H.ε
+          ε-compat₁ = refl⟩∘⟨ sym ≃₁.ε-compat ○ cancelˡ (≃₁.iso.isoˡ C.unit) ○ ¡-unique₂ (proj₁ H.ε ∘ ¡) (proj₁ H.ε)
+            where
+              open A
+              open HomReasoning
+              open ⇒-Reasoning A.U
+              open Equiv
+          ε-compat₂ : ≃₂.⇐.η C.unit B.∘ G.ε B.≈ proj₂ H.ε
+          ε-compat₂ = refl⟩∘⟨ sym ≃₂.ε-compat ○ cancelˡ (≃₂.iso.isoˡ C.unit) ○ ¡-unique₂ (proj₂ H.ε ∘ ¡) (proj₂ H.ε)
+            where
+              open B
+              open HomReasoning
+              open ⇒-Reasoning B.U
+              open Equiv
+          ⊗-homo-compat₁
+              : {X Y : C.Obj}
+              → ≃₁.⇐.η (C.⊗.₀ (X , Y))
+              A.∘ F.⊗-homo.η (X , Y)
+              A.≈ proj₁ (H.⊗-homo.η (X , Y))
+              A.∘ (≃₁.⇐.η X A.+₁ ≃₁.⇐.η Y)
+          ⊗-homo-compat₁ {X} {Y} = switch-fromtoʳ (≃₁.FX≅GX ⊗ᵢ ≃₁.FX≅GX) (assoc ○ sym (switch-fromtoˡ ≃₁.FX≅GX (refl⟩∘⟨ introʳ A.+-η ○ ≃₁.⊗-homo-compat)))
+            where
+              open A
+              open HomReasoning
+              open Equiv
+              open ⇒-Reasoning A.U
+              open ⊗-Util A′.monoidal
+          ⊗-homo-compat₂
+              : {X Y : C.Obj}
+              → ≃₂.⇐.η (C.⊗.₀ (X , Y))
+              B.∘ G.⊗-homo.η (X , Y)
+              B.≈ proj₂ (H.⊗-homo.η (X , Y))
+              B.∘ (≃₂.⇐.η X B.+₁ ≃₂.⇐.η Y)
+          ⊗-homo-compat₂ = switch-fromtoʳ (≃₂.FX≅GX ⊗ᵢ ≃₂.FX≅GX) (assoc ○ sym (switch-fromtoˡ ≃₂.FX≅GX (refl⟩∘⟨ introʳ B.+-η ○ ≃₂.⊗-homo-compat)))
+            where
+              open B
+              open HomReasoning
+              open Equiv
+              open ⇒-Reasoning B.U
+              open ⊗-Util B′.monoidal
+
+Underlying : CartesianF FinitelyCocompletes-CC SymMonCat-CC
+Underlying = record
+    { F = U
+    ; isCartesian = record
+        { F-resp-⊤ = F-resp-⊤
+        ; F-resp-× = F-resp-×
+        }
+    }