Show category of cospans is monoidal

3 files changed, 148 insertions, 1 deletions

diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda
index 9f848f4..dedfa16 100644
--- a/Category/Instance/Properties/FinitelyCocompletes.agda
+++ b/Category/Instance/Properties/FinitelyCocompletes.agda
@@ -36,7 +36,9 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
 
   open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-)
   open Equiv
-  module -+- = Functor -+-
+
+  private
+    module -+- = Functor -+-
 
   +-resp-⊥
       : {(A , B) : 𝒞×𝒞.Obj}
diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda
new file mode 100644
index 0000000..c2ab8ed
--- /dev/null
+++ b/Category/Monoidal/Instance/Cospans.agda
@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+module Category.Monoidal.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning.Iso as IsoReasoning
+
+open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Core using (Monoidal)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Category.Instance.Cospans 𝒞 using (Cospans)
+open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC)
+open import Category.Monoidal.Instance.Cospans.Newsquare {o} {ℓ} {e} using (module NewSquare)
+open import Data.Product.Base using (_,_)
+open import Functor.Instance.Cospan.Stack 𝒞 using (⊗)
+open import Functor.Instance.Cospan.Embed 𝒞 using (L; L-resp-⊗)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
+
+open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent)
+open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-naturalIsomorphism)
+
+module _ where
+
+  open CartesianCategory FinitelyCocompletes-CC using (products)
+  open BinaryProducts products using (_×_)
+
+  [𝒞×𝒞]×𝒞 : FinitelyCocompleteCategory o ℓ e
+  [𝒞×𝒞]×𝒞 = (𝒞 × 𝒞) × 𝒞
+
+CospansMonoidal : Monoidal Cospans
+CospansMonoidal = record
+    { ⊗ = ⊗
+    ; unit = ⊥
+    ; unitorˡ = [ L ]-resp-≅ ⊥+A≅A
+    ; unitorʳ = [ L ]-resp-≅ A+⊥≅A
+    ; associator = [ L ]-resp-≅ (≅.sym +-assoc)
+    ; unitorˡ-commute-from = λ { {X} {Y} {f} → Unitorˡ.from f }
+    ; unitorˡ-commute-to = λ { {X} {Y} {f} → Unitorˡ.to f }
+    ; unitorʳ-commute-from = λ { {X} {Y} {f} → Unitorʳ.from f }
+    ; unitorʳ-commute-to = λ { {X} {Y} {f} → Unitorʳ.to f }
+    ; assoc-commute-from = Associator.from _
+    ; assoc-commute-to = Associator.to _
+    ; triangle = triangle
+    ; pentagon = pentagon
+    }
+  where
+    module ⊗ = Functor ⊗
+    module Cospans = Category Cospans
+    module Unitorˡ = NewSquare ⊥+--id
+    module Unitorʳ = NewSquare -+⊥-id
+    module Associator = NewSquare {[𝒞×𝒞]×𝒞} {𝒞} associator-naturalIsomorphism
+    open Cospans.HomReasoning
+    open Cospans using (id)
+    open Cospans.Equiv
+    open Functor L renaming (F-resp-≈ to L-resp-≈)
+    open 𝒞 using (⊥; Obj; U; +-assoc)
+    open Morphism U using (module ≅)
+    λ⇒ = Unitorˡ.FX≅GX′.from
+    ρ⇒ = Unitorʳ.FX≅GX′.from
+    α⇒ = Associator.FX≅GX′.from
+    triangle : {X Y : Obj} → Cospans [ Cospans [ ⊗.₁ (id {X} , λ⇒) ∘ α⇒ ] ≈ ⊗.₁ (ρ⇒ , id {Y}) ]
+    triangle = sym L-resp-⊗ ⟩∘⟨refl ○ sym homomorphism ○ L-resp-≈ tri ○ L-resp-⊗
+    pentagon : {W X Y Z : Obj} → Cospans [ Cospans [ ⊗.₁ (id {W} , α⇒ {(X , Y) , Z}) ∘ Cospans [ α⇒ ∘ ⊗.₁ (α⇒ , id) ] ] ≈ Cospans [ α⇒ ∘ α⇒ ] ]
+    pentagon = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym homomorphism ○ sym homomorphism ○ L-resp-≈ pent ○ homomorphism
diff --git a/Category/Monoidal/Instance/Cospans/Lift.agda b/Category/Monoidal/Instance/Cospans/Lift.agda
new file mode 100644
index 0000000..fa31fcb
--- /dev/null
+++ b/Category/Monoidal/Instance/Cospans/Lift.agda
@@ -0,0 +1,71 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+module Category.Monoidal.Instance.Cospans.Lift {o ℓ e} where
+
+open import Category.Instance.Cospans using (Cospans; Cospan; Same)
+
+open import Categories.Category.Core using (Category)
+
+import Categories.Diagram.Pushout as PushoutDiagram
+import Categories.Diagram.Pushout.Properties as PushoutProperties
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Category.Diagram.Pushout as PushoutDiagram′
+import Functor.Instance.Cospan.Embed as CospanEmbed
+
+open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; module Definitions)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_)
+open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout)
+
+module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} {𝒟 : FinitelyCocompleteCategory o ℓ e} where
+
+  module 𝒞 = FinitelyCocompleteCategory 𝒞
+  module 𝒟 = FinitelyCocompleteCategory 𝒟
+
+  open CospanEmbed 𝒟 using (L; B₁; B∘L; R∘B; ≅-L-R)
+
+  module Square {F G : Functor 𝒞.U 𝒟.U} (F≃G : F ≃ G) where
+
+    module L = Functor L
+    module F = Functor F
+    module G = Functor G
+
+    open NaturalIsomorphism F≃G
+
+    open Morphism using (module ≅) renaming (_≅_ to _[_≅_])
+    FX≅GX′ : ∀ {Z : 𝒞.Obj} → Cospans 𝒟 [ F.₀ Z ≅ G.₀ Z ]
+    FX≅GX′ = [ L ]-resp-≅ FX≅GX
+    module FX≅GX {Z} = _[_≅_] (FX≅GX {Z})
+    module FX≅GX′ {Z} = _[_≅_] (FX≅GX′ {Z})
+
+    module _ {X Y : 𝒞.Obj} (fg : Cospans 𝒞 [ X , Y ]) where
+
+      open ⇒-Reasoning (Cospans 𝒟) using (switch-tofromˡ; switch-fromtoʳ)
+      open ⇒-Reasoning 𝒟.U using (switch-fromtoˡ)
+      module Cospans = Category (Cospans 𝒟)
+      open Cospans.HomReasoning using (refl⟩∘⟨_; _○_; _⟩∘⟨refl)
+      open Cospan fg renaming (f₁ to f; f₂ to g)
+      open 𝒟 using (_∘_)
+
+      squares⇒cospan : Cospans 𝒟 [ B₁ (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) ≈ B₁ (F.₁ f) (F.₁ g) ]
+      squares⇒cospan = record
+          { ≅N = ≅.sym 𝒟.U FX≅GX
+          ; from∘f₁≈f₁′ = sym (switch-fromtoˡ FX≅GX (⇒.commute f))
+          ; from∘f₂≈f₂′ = sym (switch-fromtoˡ FX≅GX (⇒.commute g))
+          }
+        where
+          open 𝒟.Equiv using (sym)
+
+      from : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇒.η Y) ∘ B₁ (F.₁ f) (F.₁ g) ] ≈ Cospans 𝒟 [ B₁ (G.₁ f) (G.₁ g) ∘ L.₁ (⇒.η X) ] ]
+      from = sym (switch-tofromˡ FX≅GX′ (refl⟩∘⟨ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan))
+        where
+          open Cospans.Equiv using (sym)
+
+      to : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇐.η Y) ∘ B₁ (G.₁ f) (G.₁ g) ] ≈ Cospans 𝒟 [ B₁ (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.η X) ] ]
+      to = switch-fromtoʳ FX≅GX′ (pullʳ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan)
+        where
+          open ⇒-Reasoning (Cospans 𝒟) using (pullʳ)