diff options
| -rw-r--r-- | Category/Instance/Properties/FinitelyCocompletes.agda | 4 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/Cospans.agda | 74 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/Cospans/Lift.agda | 71 | ||||
| -rw-r--r-- | Functor/Instance/Cospan/Embed.agda | 185 | ||||
| -rw-r--r-- | Functor/Instance/Cospan/Stack.agda | 144 |
5 files changed, 477 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ʳ) diff --git a/Functor/Instance/Cospan/Embed.agda b/Functor/Instance/Cospan/Embed.agda new file mode 100644 index 0000000..77f0361 --- /dev/null +++ b/Functor/Instance/Cospan/Embed.agda @@ -0,0 +1,185 @@ +{-# OPTIONS --without-K --safe #-} + +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +module Functor.Instance.Cospan.Embed {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where + +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Category.Diagram.Pushout as Pushout′ + +open import Categories.Category using (_[_,_]; _[_∘_]; _[_≈_]) +open import Categories.Category.Core using (Category) +open import Categories.Functor.Core using (Functor) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Data.Product.Base using (_,_) +open import Function.Base using (id) +open import Functor.Instance.Cospan.Stack using (⊗) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module Cospans = Category Cospans + +open 𝒞 using (U; pushout; _+₁_) +open Cospans using (_≈_) +open DiagramPushout U using (Pushout) +open Morphism U using (module ≅; _≅_) +open PushoutProperties U using (up-to-iso) +open Pushout′ U using (pushout-id-g; pushout-f-id) + +L₁ : {A B : 𝒞.Obj} → U [ A , B ] → Cospans [ A , B ] +L₁ f = record + { f₁ = f + ; f₂ = 𝒞.id + } + +L-identity : {A : 𝒞.Obj} → L₁ 𝒞.id ≈ Cospans.id {A} +L-identity = record + { ≅N = ≅.refl + ; from∘f₁≈f₁′ = 𝒞.identity² + ; from∘f₂≈f₂′ = 𝒞.identity² + } + +L-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] +L-homomorphism {X} {Y} {Z} {f} {g} = record + { ≅N = up-to-iso P′ P + ; from∘f₁≈f₁′ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) + ; from∘f₂≈f₂′ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ + } + where + open ⇒-Reasoning U + open 𝒞.HomReasoning + open 𝒞.Equiv + P P′ : Pushout 𝒞.id g + P = pushout 𝒞.id g + P′ = pushout-id-g + module P = Pushout P + module P′ = Pushout P′ + +L-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] +L-resp-≈ {A} {B} {f} {g} f≈g = record + { ≅N = ≅.refl + ; from∘f₁≈f₁′ = 𝒞.identityˡ ○ f≈g + ; from∘f₂≈f₂′ = 𝒞.identity² + } + where + open 𝒞.HomReasoning + +L : Functor U Cospans +L = record + { F₀ = id + ; F₁ = L₁ + ; identity = L-identity + ; homomorphism = L-homomorphism + ; F-resp-≈ = L-resp-≈ + } + +R₁ : {A B : 𝒞.Obj} → U [ B , A ] → Cospans [ A , B ] +R₁ g = record + { f₁ = 𝒞.id + ; f₂ = g + } + +R-identity : {A : 𝒞.Obj} → R₁ 𝒞.id ≈ Cospans.id {A} +R-identity = record + { ≅N = ≅.refl + ; from∘f₁≈f₁′ = 𝒞.identity² + ; from∘f₂≈f₂′ = 𝒞.identity² + } + +R-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] +R-homomorphism {X} {Y} {Z} {f} {g} = record + { ≅N = up-to-iso P′ P + ; from∘f₁≈f₁′ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₂≈f₂′ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) + } + where + open ⇒-Reasoning U + open 𝒞.HomReasoning + open 𝒞.Equiv + P P′ : Pushout f 𝒞.id + P = pushout f 𝒞.id + P′ = pushout-f-id + module P = Pushout P + module P′ = Pushout P′ + +R-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] +R-resp-≈ {A} {B} {f} {g} f≈g = record + { ≅N = ≅.refl + ; from∘f₁≈f₁′ = 𝒞.identity² + ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ f≈g + } + where + open 𝒞.HomReasoning + +R : Functor 𝒞.op Cospans +R = record + { F₀ = id + ; F₁ = R₁ + ; identity = R-identity + ; homomorphism = R-homomorphism + ; F-resp-≈ = R-resp-≈ + } + +B₁ : {A B C : 𝒞.Obj} → U [ A , C ] → U [ B , C ] → Cospans [ A , B ] +B₁ f g = record + { f₁ = f + ; f₂ = g + } + +B∘L : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ B₁ g h ∘ L₁ f ] ≈ B₁ (U [ g ∘ f ]) h +B∘L {W} {X} {Y} {Z} {f} {g} {h} = record + { ≅N = up-to-iso P P′ + ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) + ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ + } + where + open ⇒-Reasoning U + open 𝒞.HomReasoning + open 𝒞.Equiv + P P′ : Pushout 𝒞.id g + P = pushout 𝒞.id g + P′ = pushout-id-g + module P = Pushout P + module P′ = Pushout P′ + +R∘B : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ B₁ f g ] ≈ B₁ f (U [ g ∘ h ]) +R∘B {W} {X} {Y} {Z} {f} {g} {h} = record + { ≅N = up-to-iso P P′ + ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) + } + where + open ⇒-Reasoning U + open 𝒞.HomReasoning + open 𝒞.Equiv + P P′ : Pushout g 𝒞.id + P = pushout g 𝒞.id + P′ = pushout-f-id + module P = Pushout P + module P′ = Pushout P′ + +module _ where + + open _≅_ + + ≅-L-R : ∀ {X Y : 𝒞.Obj} (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) + ≅-L-R {X} {Y} X≅Y = record + { ≅N = X≅Y + ; from∘f₁≈f₁′ = isoʳ X≅Y + ; from∘f₂≈f₂′ = 𝒞.identityʳ + } + +module ⊗ = Functor (⊗ 𝒞) + +L-resp-⊗ : {X Y X′ Y′ : 𝒞.Obj} {a : U [ X , X′ ]} {b : U [ Y , Y′ ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) +L-resp-⊗ {X} {Y} {X′} {Y′} {a} {b} = record + { ≅N = ≅.refl + ; from∘f₁≈f₁′ = 𝒞.identityˡ + ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) + } + where + open 𝒞.HomReasoning + open 𝒞.Equiv + open 𝒞 using (+-η; []-cong₂; identityˡ; identityʳ) diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda new file mode 100644 index 0000000..b7664dc --- /dev/null +++ b/Functor/Instance/Cospan/Stack.agda @@ -0,0 +1,144 @@ +{-# OPTIONS --without-K --safe #-} + +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +module Functor.Instance.Cospan.Stack {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where + +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category.Core using (Category) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same; id-Cospan; compose) +open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using () renaming (_×_ to _×′_) +open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) +open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout) +open import Level using (Level; _⊔_; suc) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module Cospans = Category Cospans + +open 𝒞 using (U; _+_; _+₁_; pushout; coproduct; [_,_]; ⊥; cocartesianCategory; monoidal) +open Category U +open DiagramPushout U using (Pushout) +open PushoutProperties U using (up-to-iso) + +module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 ×′ 𝒞) +open 𝒞×𝒞 using () renaming (pushout to pushout′; U to U×U) +open DiagramPushout U×U using () renaming (Pushout to Pushout′) + +open import Categories.Category.Monoidal.Utilities monoidal using (_⊗ᵢ_) + +together : {A A′ B B′ : Obj} → Cospan A B → Cospan A′ B′ → Cospan (A + A′) (B + B′) +together A⇒B A⇒B′ = record + { f₁ = f₁ A⇒B +₁ f₁ A⇒B′ + ; f₂ = f₂ A⇒B +₁ f₂ A⇒B′ + } + where + open Cospan + +id⊗id≈id : {A B : Obj} → Same (together (id-Cospan {A}) (id-Cospan {B})) (id-Cospan {A + B}) +id⊗id≈id {A} {B} = record + { ≅N = ≅.refl + ; from∘f₁≈f₁′ = from∘f≈f′ + ; from∘f₂≈f₂′ = from∘f≈f′ + } + where + open Morphism U using (module ≅) + open HomReasoning + open 𝒞 using (+-η; []-cong₂) + open coproduct {A} {B} using (i₁; i₂) + from∘f≈f′ : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id + from∘f≈f′ = begin + id ∘ [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ identityˡ ⟩ + [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ []-cong₂ identityʳ identityʳ ⟩ + [ i₁ , i₂ ] ≈⟨ +-η ⟩ + id ∎ + +homomorphism + : {A A′ B B′ C C′ : Obj} + → (A⇒B : Cospan A B) + → (B⇒C : Cospan B C) + → (A⇒B′ : Cospan A′ B′) + → (B⇒C′ : Cospan B′ C′) + → Same (together (compose A⇒B B⇒C) (compose A⇒B′ B⇒C′)) (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′) ) +homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record + { ≅N = ≅N + ; from∘f₁≈f₁′ = from∘f₁≈f₁′ + ; from∘f₂≈f₂′ = from∘f₂≈f₂′ + } + where + open Cospan + open Pushout + open HomReasoning + open ⇒-Reasoning U + open Morphism U using (_≅_) + open _≅_ + open 𝒞 using (+₁∘+₁) + module -+- = RightExactFunctor (-+- {𝒞}) + P₁ = pushout (f₂ A⇒B) (f₁ B⇒C) + P₂ = pushout (f₂ A⇒B′) (f₁ B⇒C′) + module P₁ = Pushout P₁ + module P₂ = Pushout P₂ + P₁×P₂ = pushout′ (f₂ A⇒B , f₂ A⇒B′) (f₁ B⇒C , f₁ B⇒C′) + module P₁×P₂ = Pushout′ P₁×P₂ + P₃ = pushout (f₂ A⇒B +₁ f₂ A⇒B′) (f₁ B⇒C +₁ f₁ B⇒C′) + P₃′ = IsPushout⇒Pushout (-+-.F-resp-pushout P₁×P₂.isPushout) + ≅N : Q P₃′ ≅ Q P₃ + ≅N = up-to-iso P₃′ P₃ + from∘f₁≈f₁′ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′)) + from∘f₁≈f₁′ = begin + from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈⟨ Equiv.refl ⟩ + from ≅N ∘ ((i₁ P₁ ∘ f₁ A⇒B) +₁ (i₁ P₂ ∘ f₁ A⇒B′)) ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨ + from ≅N ∘ (i₁ P₁ +₁ i₁ P₂) ∘ (f₁ A⇒B +₁ f₁ A⇒B′) ≈⟨ Equiv.refl ⟩ + from ≅N ∘ i₁ P₃′ ∘ f₁ (together A⇒B A⇒B′) ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩ + i₁ P₃ ∘ f₁ (together A⇒B A⇒B′) ∎ + from∘f₂≈f₂′ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′)) + from∘f₂≈f₂′ = begin + from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈⟨ Equiv.refl ⟩ + from ≅N ∘ ((i₂ P₁ ∘ f₂ B⇒C) +₁ (i₂ P₂ ∘ f₂ B⇒C′)) ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨ + from ≅N ∘ (i₂ P₁ +₁ i₂ P₂) ∘ (f₂ B⇒C +₁ f₂ B⇒C′) ≈⟨ Equiv.refl ⟩ + from ≅N ∘ i₂ P₃′ ∘ f₂ (together B⇒C B⇒C′) ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩ + i₂ P₃ ∘ f₂ (together B⇒C B⇒C′) ∎ + +⊗-resp-≈ + : {A A′ B B′ : Obj} + {f f′ : Cospan A B} + {g g′ : Cospan A′ B′} + → Same f f′ + → Same g g′ + → Same (together f g) (together f′ g′) +⊗-resp-≈ {_} {_} {_} {_} {f} {f′} {g} {g′} ≈f ≈g = record + { ≅N = ≈f.≅N ⊗ᵢ ≈g.≅N + ; from∘f₁≈f₁′ = from∘f₁≈f₁′ + ; from∘f₂≈f₂′ = from∘f₂≈f₂′ + } + where + open 𝒞 using (-+-) + module ≈f = Same ≈f + module ≈g = Same ≈g + open HomReasoning + open Cospan + open 𝒞 using (+₁-cong₂; +₁∘+₁) + from∘f₁≈f₁′ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′ + from∘f₁≈f₁′ = begin + (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈⟨ +₁∘+₁ ⟩ + (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g) ≈⟨ +₁-cong₂ (≈f.from∘f₁≈f₁′) (≈g.from∘f₁≈f₁′) ⟩ + f₁ f′ +₁ f₁ g′ ∎ + from∘f₂≈f₂′ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′ + from∘f₂≈f₂′ = begin + (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈⟨ +₁∘+₁ ⟩ + (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g) ≈⟨ +₁-cong₂ (≈f.from∘f₂≈f₂′) (≈g.from∘f₂≈f₂′) ⟩ + f₂ f′ +₁ f₂ g′ ∎ + +⊗ : Bifunctor Cospans Cospans Cospans +⊗ = record + { F₀ = λ { (A , A′) → A + A′ } + ; F₁ = λ { (f , g) → together f g } + ; identity = λ { {x , y} → id⊗id≈id {x} {y} } + ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } + ; F-resp-≈ = λ { (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g } + } |