Show category of cospans is monoidal

1 files changed, 71 insertions, 0 deletions

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ʳ)