aboutsummaryrefslogtreecommitdiff
path: root/Functor/Instance/DecoratedCospan
diff options
context:
space:
mode:
Diffstat (limited to 'Functor/Instance/DecoratedCospan')
-rw-r--r--Functor/Instance/DecoratedCospan/Embed.agda275
-rw-r--r--Functor/Instance/DecoratedCospan/Stack.agda430
2 files changed, 705 insertions, 0 deletions
diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda
new file mode 100644
index 0000000..77b16fa
--- /dev/null
+++ b/Functor/Instance/DecoratedCospan/Embed.agda
@@ -0,0 +1,275 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+open Lax using (SymmetricMonoidalFunctor)
+open FinitelyCocompleteCategory
+ using ()
+ renaming (symmetricMonoidalCategory to smc)
+
+module Functor.Instance.DecoratedCospan.Embed
+ {o o′ ℓ ℓ′ e e′}
+ (𝒞 : FinitelyCocompleteCategory o ℓ e)
+ {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
+ (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Diagram.Pushout.Properties as PushoutProperties
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Category.Diagram.Pushout as Pushout′
+import Category.Diagram.Cospan as Cospan
+import Functor.Instance.Cospan.Embed 𝒞 as Embed
+
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
+open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Category.Instance.Cospans 𝒞 using (Cospans)
+open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans)
+
+import Categories.Diagram.Pushout as DiagramPushout
+import Categories.Diagram.Pushout.Properties as PushoutProperties
+import Categories.Morphism as Morphism
+
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Functor using (Functor; _∘F_)
+open import Data.Product using (_,_)
+open import Function using () renaming (id to idf)
+open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+module 𝒟 = SymmetricMonoidalCategory 𝒟
+module F = SymmetricMonoidalFunctor F
+module Cospans = Category Cospans
+module DecoratedCospans = Category DecoratedCospans
+module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian
+
+open import Functor.Instance.Decorate 𝒞 F using (Decorate; Decorate-resp-⊗)
+
+private
+ variable
+ A B C D E H : 𝒞.Obj
+ f : 𝒞.U [ A , B ]
+ g : 𝒞.U [ C , D ]
+ h : 𝒞.U [ E , H ]
+
+L : Functor 𝒞.U DecoratedCospans
+L = Decorate ∘F Embed.L
+
+R : Functor 𝒞.op DecoratedCospans
+R = Decorate ∘F Embed.R
+
+B₁ : 𝒞.U [ A , C ] → 𝒞.U [ B , C ] → 𝒟.U [ 𝒟.unit , F.F₀ C ] → DecoratedCospans [ A , B ]
+B₁ f g s = record
+ { cospan = Cospan.cospan f g
+ ; decoration = s
+ }
+
+module _ where
+
+ module L = Functor L
+ module R = Functor R
+
+ module Codiagonal where
+
+ open mc𝒞 using (unitorˡ; unitorʳ; +-monoidal) public
+ open unitorˡ using () renaming (to to λ⇐′) public
+ open unitorʳ using () renaming (to to ρ⇐′) public
+ open 𝒞 using (U; _+_; []-cong₂; []∘+₁; ∘-distribˡ-[]; inject₁; inject₂; ¡)
+ renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+ open Category U
+ open Equiv
+ open HomReasoning
+ open ⇒-Reasoning 𝒞.U
+
+ μ : {X : Obj} → X + X ⇒ X
+ μ = [ id , id ]′
+
+ μ∘+ : {X Y Z : Obj} {f : X ⇒ Z} {g : Y ⇒ Z} → [ f , g ]′ ≈ μ ∘ f +₁ g
+ μ∘+ = []-cong₂ (sym identityˡ) (sym identityˡ) ○ sym []∘+₁
+
+ μ∘¡ˡ : {X : Obj} → μ ∘ ¡ +₁ id ∘ λ⇐′ ≈ id {X}
+ μ∘¡ˡ = begin
+ μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩
+ [ ¡ , id ]′ ∘ λ⇐′ ≈⟨ inject₂ ⟩
+ id ∎
+
+ μ∘¡ʳ : {X : Obj} → μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈ id {X}
+ μ∘¡ʳ = begin
+ μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩
+ [ id , ¡ ]′ ∘ ρ⇐′ ≈⟨ inject₁ ⟩
+ id ∎
+
+
+ μ-natural : {X Y : Obj} {f : X ⇒ Y} → f ∘ μ ≈ μ ∘ f +₁ f
+ μ-natural = ∘-distribˡ-[] ○ []-cong₂ (identityʳ ○ sym identityˡ) (identityʳ ○ sym identityˡ) ○ sym []∘+₁
+
+ B∘L : {A B M C : 𝒞.Obj}
+ → {f : 𝒞.U [ A , B ]}
+ → {g : 𝒞.U [ B , M ]}
+ → {h : 𝒞.U [ C , M ]}
+ → {s : 𝒟.U [ 𝒟.unit , F.₀ M ]}
+ → DecoratedCospans [ DecoratedCospans [ B₁ g h s ∘ L.₁ f ] ≈ B₁ (𝒞.U [ g ∘ f ]) h s ]
+ B∘L {A} {B} {M} {C} {f} {g} {h} {s} = record
+ { cospans-≈ = Embed.B∘L
+ ; same-deco = same-deco
+ }
+ where
+
+ module _ where
+ open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+ open 𝒞 using (U)
+ open Category U
+ open mc𝒞 using (unitorˡ; unitorˡ-commute-to; +-monoidal) public
+ open unitorˡ using () renaming (to to λ⇐′) public
+ open ⊗-Reasoning +-monoidal
+ open ⇒-Reasoning 𝒞.U
+ open Equiv
+
+ open Pushout′ 𝒞.U using (pushout-id-g)
+ open PushoutProperties 𝒞.U using (up-to-iso)
+ open DiagramPushout 𝒞.U using (Pushout)
+ P P′ : Pushout 𝒞.id g
+ P = pushout 𝒞.id g
+ P′ = pushout-id-g
+ module P = Pushout P
+ module P′ = Pushout P′
+ open Morphism 𝒞.U using (_≅_)
+ open _≅_ using (from)
+ open P using (i₁ ; i₂; universal∘i₂≈h₂) public
+
+ open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ˡ)
+
+ ≅ : P.Q ⇒ M
+ ≅ = up-to-iso P P′ .from
+
+ ≅∘[]∘¡+id : ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈ id
+ ≅∘[]∘¡+id = begin
+ ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈⟨ assoc²αε ⟩
+ ≅ ∘ [ i₁ , i₂ ]′ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩
+ ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ refl⟩∘⟨ pull-center (sym split₁ʳ) ⟩
+ ≅ ∘ μ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′ ≈⟨ extendʳ μ-natural ⟩
+ μ ∘ ≅ +₁ ≅ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩
+ μ ∘ (≅ ∘ i₁ ∘ ¡) +₁ (≅ ∘ i₂) ∘ λ⇐′ ≈⟨ refl⟩∘⟨ sym (¡-unique (≅ ∘ i₁ ∘ ¡)) ⟩⊗⟨ universal∘i₂≈h₂ ⟩∘⟨refl ⟩
+ μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ μ∘¡ˡ ⟩
+ id ∎
+
+ open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-)
+ open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+ open Category U
+ open Equiv
+ open ⇒-Reasoning U
+ open ⊗-Reasoning monoidal
+ open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+ open F using (F₁; ε)
+ open Shorthands monoidal
+
+ same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s
+ same-deco = begin
+ F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ id ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym F.identity ⟩∘⟨refl ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ F₁ 𝒞.id ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , 𝒞.id)) ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩
+ F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+ F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟩
+ F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟩
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟨
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ λ-.isoʳ) ⟩
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘¡+id ○ F.identity) ⟩
+ s ∎
+
+ R∘B : {A N B C : 𝒞.Obj}
+ → {f : 𝒞.U [ A , N ]}
+ → {g : 𝒞.U [ B , N ]}
+ → {h : 𝒞.U [ C , B ]}
+ → {s : 𝒟.U [ 𝒟.unit , F.₀ N ]}
+ → DecoratedCospans [ DecoratedCospans [ R.₁ h ∘ B₁ f g s ] ≈ B₁ f (𝒞.U [ g ∘ h ]) s ]
+ R∘B {A} {N} {B} {C} {f} {g} {h} {s} = record
+ { cospans-≈ = Embed.R∘B
+ ; same-deco = same-deco
+ }
+ where
+
+ module _ where
+ open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+ open 𝒞 using (U)
+ open Category U
+ open mc𝒞 using (unitorʳ; unitorˡ; unitorˡ-commute-to; +-monoidal) public
+ open unitorˡ using () renaming (to to λ⇐′) public
+ open unitorʳ using () renaming (to to ρ⇐′) public
+ open ⊗-Reasoning +-monoidal
+ open ⇒-Reasoning 𝒞.U
+ open Equiv
+
+ open Pushout′ 𝒞.U using (pushout-f-id)
+ open PushoutProperties 𝒞.U using (up-to-iso)
+ open DiagramPushout 𝒞.U using (Pushout)
+ P P′ : Pushout g 𝒞.id
+ P = pushout g 𝒞.id
+ P′ = pushout-f-id
+ module P = Pushout P
+ module P′ = Pushout P′
+ open Morphism 𝒞.U using (_≅_)
+ open _≅_ using (from)
+ open P using (i₁ ; i₂; universal∘i₁≈h₁) public
+
+ open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ʳ)
+
+ ≅ : P.Q ⇒ N
+ ≅ = up-to-iso P P′ .from
+
+ ≅∘[]∘id+¡ : ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈ id
+ ≅∘[]∘id+¡ = begin
+ ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈⟨ assoc²αε ⟩
+ ≅ ∘ [ i₁ , i₂ ]′ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩
+ ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ pull-center merge₂ʳ ⟩
+ ≅ ∘ μ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ extendʳ μ-natural ⟩
+ μ ∘ ≅ +₁ ≅ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩
+ μ ∘ (≅ ∘ i₁) +₁ (≅ ∘ i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ universal∘i₁≈h₁ ⟩⊗⟨ sym (¡-unique (≅ ∘ i₂ ∘ ¡)) ⟩∘⟨refl ⟩
+ μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ μ∘¡ʳ ⟩
+ id ∎
+
+ open 𝒟 using (U; monoidal; _⊗₁_; unitorʳ-commute-from) renaming (module unitorˡ to λ-; module unitorʳ to ρ)
+ open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+ open Category U
+ open Equiv
+ open ⇒-Reasoning U
+ open ⊗-Reasoning monoidal
+ open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+ open F using (F₁; ε)
+ open Shorthands monoidal
+
+ same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s
+ same-deco = begin
+ F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ F₁ 𝒞.id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (𝒞.id , ¡)) ⟩
+ F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩
+ F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
+ F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorʳ) F.unitaryʳ) ⟩
+ F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ F₁ ρ⇐′ ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorʳ-commute-from ⟩
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ∘ ρ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ ρ.isoʳ) ⟩
+ F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘id+¡ ○ F.identity) ⟩
+ s ∎
+
+ open Morphism 𝒞.U using (_≅_)
+ open _≅_
+
+ ≅-L-R : (X≅Y : A ≅ B) → DecoratedCospans [ L.₁ (to X≅Y) ≈ R.₁ (from X≅Y) ]
+ ≅-L-R X≅Y = Decorate.F-resp-≈ (Embed.≅-L-R X≅Y)
+ where
+ module Decorate = Functor Decorate
+
+ open 𝒞 using (_+₁_)
+
+ L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ]
+ L-resp-⊗ = Decorate.F-resp-≈ Embed.L-resp-⊗ ○ Decorate-resp-⊗
+ where
+ module Decorate = Functor Decorate
+ open DecoratedCospans.HomReasoning
diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda
new file mode 100644
index 0000000..381ee06
--- /dev/null
+++ b/Functor/Instance/DecoratedCospan/Stack.agda
@@ -0,0 +1,430 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+open Lax using (SymmetricMonoidalFunctor)
+open FinitelyCocompleteCategory
+ using ()
+ renaming (symmetricMonoidalCategory to smc)
+
+module Functor.Instance.DecoratedCospan.Stack
+ {o o′ ℓ ℓ′ e e′}
+ (𝒞 : FinitelyCocompleteCategory o ℓ e)
+ {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
+ (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
+
+import Categories.Diagram.Pushout as DiagramPushout
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+
+import Functor.Instance.Cospan.Stack 𝒞 as Stack
+
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
+open import Categories.Category.Monoidal.Braided.Properties using (braiding-coherence-inv)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Object.Initial using (Initial)
+open import Categories.Object.Duality using (Coproduct⇒coProduct)
+open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; _≈_ to _≈_′)
+
+import Category.Diagram.Cospan 𝒞 as Cospan
+
+open import Cospan.Decorated 𝒞 F using (DecoratedCospan)
+open import Data.Product.Base using (_,_)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+module 𝒟 = SymmetricMonoidalCategory 𝒟
+module F = SymmetricMonoidalFunctor F
+module Cospans = Category Cospans
+
+open 𝒞 using (Obj; _+_; cocartesian)
+
+module mc𝒞 = CocartesianMonoidal 𝒞.U cocartesian
+module smc𝒞 = CocartesianSymmetricMonoidal 𝒞.U cocartesian
+
+open DiagramPushout 𝒞.U using (Pushout)
+
+private
+ variable
+ A A′ B B′ C C′ : Obj
+
+together : Cospans [ A , B ] → Cospans [ A′ , B′ ] → Cospans [ A + A′ , B + B′ ]
+together A⇒B A⇒B′ = record
+ { cospan = A⇒B.cospan Cospan.⊗ A⇒B′.cospan
+ ; decoration = ⊗-homo.η (A⇒B.N , A⇒B′.N) ∘ A⇒B.decoration ⊗₁ A⇒B′.decoration ∘ unitorʳ.to
+ }
+ where
+ module A⇒B = DecoratedCospan A⇒B
+ module A⇒B′ = DecoratedCospan A⇒B′
+ open 𝒟 using (_∘_; _⊗₁_; module unitorʳ)
+ open F using (module ⊗-homo)
+
+id⊗id≈id : Cospans [ together (Cospans.id {A}) (Cospans.id {B}) ≈ Cospans.id ]
+id⊗id≈id {A} {B} = record
+ { cospans-≈ = Stack.id⊗id≈id
+ ; same-deco = F.identity ⟩∘⟨refl
+ ○ identityˡ
+ ○ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl
+ ○ extendʳ (extendʳ (⊗-homo.commute (! , !)))
+ ○ refl⟩∘⟨ pullʳ (pushˡ serialize₂₁ ○ refl⟩∘⟨ sym unitorʳ-commute-to)
+ ○ pushˡ (F-resp-≈ !+!≈! ○ homomorphism)
+ ○ refl⟩∘⟨ (refl⟩∘⟨ sym-assoc ○ pullˡ unitaryʳ ○ cancelˡ unitorʳ.isoʳ)
+ }
+ where
+ open 𝒞 using (_+₁_; ¡-unique)
+ open 𝒟 using (identityˡ; U; monoidal; module unitorʳ; unitorʳ-commute-to; assoc; sym-assoc)
+ open 𝒟.Equiv
+ open ⇒-Reasoning U
+ open ⇒-Reasoning 𝒞.U using () renaming (flip-iso to flip-iso′)
+ open ⊗-Reasoning monoidal
+ open F using (module ⊗-homo; F-resp-≈; homomorphism; unitaryʳ)
+ open 𝒞 using (initial)
+ open Initial initial using (!; !-unique₂)
+ open Morphism using (_≅_; module ≅)
+ open mc𝒞 using (A+⊥≅A)
+ module A+⊥≅A = _≅_ A+⊥≅A
+ !+!≈! : 𝒞.U [ (! {A} +₁ ! {B}) ≈ ! {A + B} 𝒞.∘ A+⊥≅A.from ]
+ !+!≈! = 𝒞.Equiv.sym (flip-iso′ (≅.sym 𝒞.U A+⊥≅A) (¡-unique ((! +₁ !) 𝒞.∘ A+⊥≅A.to)))
+
+homomorphism
+ : (A⇒B : Cospans [ A , B ])
+ → (B⇒C : Cospans [ B , C ])
+ → (A⇒B′ : Cospans [ A′ , B′ ])
+ → (B⇒C′ : Cospans [ B′ , C′ ])
+ → Cospans
+ [ together (Cospans [ B⇒C ∘ A⇒B ]) (Cospans [ B⇒C′ ∘ A⇒B′ ])
+ ≈ Cospans [ together B⇒C B⇒C′ ∘ together A⇒B A⇒B′ ]
+ ]
+homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record
+ { cospans-≈ = cospans-≈
+ ; same-deco = same-deco
+ }
+ where
+
+ module _ where
+ open DecoratedCospan using (cospan)
+ cospans-≈ : _ Cospan.⊗ _ Cospan.≈ Cospan.compose (_ Cospan.⊗ _) (_ Cospan.⊗ _)
+ cospans-≈ = Stack.homomorphism (f .cospan) (g .cospan) (f′ .cospan) (g′ .cospan)
+ open Cospan._≈_ cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public
+
+ module DecorationNames where
+ open DecoratedCospan f using (N) renaming (decoration to s) public
+ open DecoratedCospan g using () renaming (decoration to t; N to M) public
+ open DecoratedCospan f′ using () renaming (decoration to s′; N to N′) public
+ open DecoratedCospan g′ using () renaming (decoration to t′; N to M′) public
+
+ module PushoutNames where
+ open DecoratedCospan using (f₁; f₂)
+ open 𝒞 using (pushout)
+ open Pushout (pushout (f .f₂) (g .f₁)) using (i₁; i₂; Q) public
+ open Pushout (pushout (f′ .f₂) (g′ .f₁)) using () renaming (i₁ to i₁′; i₂ to i₂′; Q to Q′) public
+ open Pushout (pushout (together f f′ .f₂) (together g g′ .f₁))
+ using (universal∘i₁≈h₁; universal∘i₂≈h₂)
+ renaming (i₁ to i₁″; i₂ to i₂″; Q to Q″) public
+
+ module _ where
+
+ open DecorationNames
+ open PushoutNames
+ open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+
+ open 𝒞 using () renaming ([_,_] to [_,_]′)
+
+ module _ where
+
+ open 𝒞
+ using (U; +-swap; inject₁; inject₂; +-η)
+ renaming (i₁ to ι₁; i₂ to ι₂; _+₁_ to infixr 10 _+₁_)
+ open Category U hiding (Obj)
+ open Equiv
+ open Shorthands mc𝒞.+-monoidal
+ open ⊗-Reasoning mc𝒞.+-monoidal
+ open ⇒-Reasoning U
+ open mc𝒞 using (assoc-commute-from; assoc-commute-to; module ⊗; associator)
+ open smc𝒞 using () renaming (module braiding to σ)
+
+ module Codiagonal where
+
+ open 𝒞 using (coproduct; +-unique; []-cong₂; []∘+₁; ∘-distribˡ-[])
+ μ : {X : Obj} → X + X ⇒ X
+ μ = [ id , id ]′
+
+ μ∘+ : {X Y Z : Obj} {f : X ⇒ Z} {g : Y ⇒ Z} → [ f , g ]′ ≈ μ ∘ f +₁ g
+ μ∘+ = []-cong₂ (sym identityˡ) (sym identityˡ) ○ sym []∘+₁
+
+ μ∘σ : {X : Obj} → μ ∘ +-swap ≈ μ {X}
+ μ∘σ = sym (+-unique (pullʳ inject₁ ○ inject₂) (pullʳ inject₂ ○ inject₁) )
+
+ op-binaryProducts : BinaryProducts op
+ op-binaryProducts = record { product = Coproduct⇒coProduct U coproduct }
+
+ module op-binaryProducts = BinaryProducts op-binaryProducts
+ open op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []∘assocˡ)
+
+ μ-assoc : {X : Obj} → μ {X} ∘ μ +₁ (id {X}) ≈ μ ∘ (id {X}) +₁ μ ∘ α⇒
+ μ-assoc = begin
+ μ ∘ μ +₁ id ≈⟨ μ∘+ ⟨
+ [ [ id , id ]′ , id ]′ ≈⟨ []∘assocˡ ⟨
+ [ id , [ id , id ]′ ]′ ∘ α⇒ ≈⟨ pushˡ μ∘+ ⟩
+ μ ∘ id +₁ μ ∘ α⇒ ∎
+
+ μ-natural : {X Y : Obj} {f : X ⇒ Y} → f ∘ μ ≈ μ ∘ f +₁ f
+ μ-natural = ∘-distribˡ-[] ○ []-cong₂ (identityʳ ○ sym identityˡ) (identityʳ ○ sym identityˡ) ○ sym []∘+₁
+
+ open Codiagonal
+
+ ≅ : Q + Q′ ⇒ Q″
+ ≅ = Q+Q′≅Q″.from
+
+ ≅∘[]+[]≈μ∘μ+μ : ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′ ≈ (μ ∘ (μ +₁ μ)) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂))
+ ≅∘[]+[]≈μ∘μ+μ = begin
+ ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′ ≈⟨ refl⟩∘⟨ μ∘+ ⟩⊗⟨ μ∘+ ⟩
+ ≅ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ introˡ +-η ⟩
+ ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ push-center μ∘+ ⟩
+ ≅ ∘ μ ∘ (ι₁ +₁ ι₂) ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ⊗-distrib-over-∘ ⟩
+ ≅ ∘ μ ∘ (ι₁ ∘ μ ∘ i₁ +₁ i₂) +₁ (ι₂ ∘ μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ μ-natural) ⟩⊗⟨ (extendʳ μ-natural) ⟩
+ ≅ ∘ μ ∘ (μ ∘ ι₁ +₁ ι₁ ∘ i₁ +₁ i₂) +₁ (μ ∘ ι₂ +₁ ι₂ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩⊗⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩
+ ≅ ∘ μ ∘ (μ ∘ (ι₁ ∘ i₁) +₁ (ι₁ ∘ i₂)) +₁ (μ ∘ (ι₂ ∘ i₁′) +₁ (ι₂ ∘ i₂′)) ≈⟨ extendʳ μ-natural ⟩
+ μ ∘ ≅ +₁ ≅ ∘ (μ ∘ _) +₁ (μ ∘ _) ≈⟨ refl⟩∘⟨ sym ⊗-distrib-over-∘ ⟩
+ μ ∘ (≅ ∘ μ ∘ _) +₁ (≅ ∘ μ ∘ _) ≈⟨ refl⟩∘⟨ extendʳ μ-natural ⟩⊗⟨ extendʳ μ-natural ⟩
+ μ ∘ (μ ∘ ≅ +₁ ≅ ∘ _) +₁ (μ ∘ ≅ +₁ ≅ ∘ _) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩⊗⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩
+ μ ∘ (μ ∘ (≅ ∘ ι₁ ∘ i₁) +₁ (≅ ∘ ι₁ ∘ i₂)) +₁ (μ ∘ (≅ ∘ ι₂ ∘ i₁′) +₁ (≅ ∘ ι₂ ∘ i₂′)) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ eq₁ ⟩⊗⟨ eq₂ ) ⟩⊗⟨ (refl⟩∘⟨ eq₃ ⟩⊗⟨ eq₄ ) ⟩
+ μ ∘ (μ ∘ (i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ (μ ∘ (i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩
+ μ ∘ (μ +₁ μ) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ≈⟨ sym-assoc ⟩
+ (μ ∘ (μ +₁ μ)) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ∎
+ where
+ eq₁ : ≅ ∘ ι₁ ∘ i₁ ≈ i₁″ ∘ ι₁
+ eq₁ = refl⟩∘⟨ sym inject₁ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₁≈h₁))
+ eq₂ : ≅ ∘ ι₁ ∘ i₂ ≈ i₂″ ∘ ι₁
+ eq₂ = refl⟩∘⟨ sym inject₁ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₂≈h₂))
+ eq₃ : ≅ ∘ ι₂ ∘ i₁′ ≈ i₁″ ∘ ι₂
+ eq₃ = refl⟩∘⟨ sym inject₂ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₁≈h₁))
+ eq₄ : ≅ ∘ ι₂ ∘ i₂′ ≈ i₂″ ∘ ι₂
+ eq₄ = refl⟩∘⟨ sym inject₂ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₂≈h₂))
+
+ swap-inner : {W X Y Z : Obj} → (W + X) + (Y + Z) ⇒ (W + Y) + (X + Z)
+ swap-inner = α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒
+
+ swap-inner-natural
+ : {W X Y Z W′ X′ Y′ Z′ : Obj}
+ {w : W ⇒ W′} {x : X ⇒ X′} {y : Y ⇒ Y′} {z : Z ⇒ Z′}
+ → (w +₁ x) +₁ (y +₁ z) ∘ swap-inner
+ ≈ swap-inner ∘ (w +₁ y) +₁ (x +₁ z)
+ swap-inner-natural {w = w} {x = x} {y = y} {z = z} = begin
+ (w +₁ x) +₁ (y +₁ z) ∘ α⇐ ∘ _ ≈⟨ extendʳ assoc-commute-to ⟨
+ α⇐ ∘ w +₁ (x +₁ _) ∘ id +₁ _ ∘ α⇒ ≈⟨ pull-center merge₂ʳ ⟩
+ α⇐ ∘ w +₁ (x +₁ _ ∘ α⇒ ∘ _) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ assoc-commute-from ⟩∘⟨refl ⟨
+ α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y) +₁ z ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pushˡ split₁ʳ) ⟩∘⟨refl ⟨
+ α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y ∘ +-swap) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ σ.⇒.sym-commute _ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩
+ α⇐ ∘ w +₁ (α⇒ ∘ (+-swap ∘ y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center split₁ˡ ⟩∘⟨refl ⟩
+ α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ (y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ assoc-commute-to) ⟩∘⟨refl ⟨
+ α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐ ∘ y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc²εβ ⟩∘⟨refl ⟩
+ α⇐ ∘ w +₁ ((α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ w +₁ (y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟨
+ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ∘ (w +₁ y) +₁ (x +₁ z) ≈⟨ assoc²εβ ⟩
+ swap-inner ∘ (w +₁ y) +₁ (x +₁ z) ∎
+
+ μ∘μ+μ∘swap-inner : {X : Obj} → μ {X} ∘ μ +₁ μ ∘ swap-inner ≈ μ ∘ μ +₁ μ {X}
+ μ∘μ+μ∘swap-inner = begin
+ μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ push-center serialize₁₂ ⟩
+ μ ∘ μ +₁ id ∘ id +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
+ μ ∘ μ +₁ id ∘ (id +₁ id) +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-to ⟨
+ μ ∘ μ +₁ id ∘ α⇐ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ pullˡ μ-assoc ⟩
+ (μ ∘ id +₁ μ ∘ α⇒) ∘ α⇐ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ extendʳ (pullʳ (cancelʳ associator.isoʳ)) ⟩
+ μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ pull-center merge₂ˡ ⟩
+ μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ ∘ α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ pull-center merge₂ʳ ⟩
+ μ ∘ id +₁ (μ ∘ id +₁ μ ∘ α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pull-center refl ⟩∘⟨refl ⟩
+ μ ∘ id +₁ (μ ∘ (id +₁ μ ∘ α⇒) ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ μ-assoc ⟩∘⟨refl ⟨
+ μ ∘ id +₁ (μ ∘ μ +₁ id ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pull-center (sym split₁ˡ) ⟩∘⟨refl ⟩
+ μ ∘ id +₁ (μ ∘ (μ ∘ +-swap) +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ μ∘σ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩
+ μ ∘ id +₁ (μ ∘ μ +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (sym-assoc ○ flip-iso associator (μ-assoc ○ sym-assoc)) ⟩∘⟨refl ⟩
+ μ ∘ id +₁ (μ ∘ id +₁ μ) ∘ α⇒ ≈⟨ push-center split₂ʳ ⟩
+ μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟨
+ μ ∘ id +₁ μ ∘ α⇒ ∘ (id +₁ id) +₁ μ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩
+ μ ∘ id +₁ μ ∘ α⇒ ∘ id +₁ μ ≈⟨ refl⟩∘⟨ sym-assoc ⟩
+ μ ∘ (id +₁ μ ∘ α⇒) ∘ id +₁ μ ≈⟨ extendʳ μ-assoc ⟨
+ μ ∘ μ +₁ id ∘ id +₁ μ ≈⟨ refl⟩∘⟨ serialize₁₂ ⟨
+ μ ∘ μ +₁ μ ∎
+
+ ≅∘[]+[]∘σ₄ : (Q+Q′≅Q″.from ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′) ∘ swap-inner ≈ [ i₁″ , i₂″ ]′
+ ≅∘[]+[]∘σ₄ = begin
+ (≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′) ∘ _ ≈⟨ pushˡ ≅∘[]+[]≈μ∘μ+μ ⟩
+ (μ ∘ (μ +₁ μ)) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ∘ (α⇐ ∘ _) ≈⟨ refl⟩∘⟨ swap-inner-natural ⟩
+ (μ ∘ (μ +₁ μ)) ∘ swap-inner ∘ _ ≈⟨ pullˡ assoc ⟩
+ (μ ∘ (μ +₁ μ) ∘ swap-inner) ∘ _ ≈⟨ pushˡ μ∘μ+μ∘swap-inner ⟩
+ μ ∘ (μ +₁ μ) ∘ ((i₁″ ∘ ι₁) +₁ (i₁″ ∘ ι₂)) +₁ ((i₂″ ∘ ι₁) +₁ (i₂″ ∘ ι₂)) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩⊗⟨ ⊗-distrib-over-∘ ⟩
+ μ ∘ (μ +₁ μ) ∘ (i₁″ +₁ i₁″ ∘ ι₁ +₁ ι₂) +₁ (i₂″ +₁ i₂″ ∘ ι₁ +₁ ι₂) ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨
+ μ ∘ (μ ∘ i₁″ +₁ i₁″ ∘ ι₁ +₁ ι₂) +₁ (μ ∘ i₂″ +₁ i₂″ ∘ ι₁ +₁ ι₂) ≈⟨ refl⟩∘⟨ extendʳ μ-natural ⟩⊗⟨ extendʳ μ-natural ⟨
+ μ ∘ (i₁″ ∘ μ ∘ ι₁ +₁ ι₂) +₁ (i₂″ ∘ μ ∘ ι₁ +₁ ι₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ μ∘+) ⟩⊗⟨ (refl⟩∘⟨ μ∘+) ⟨
+ μ ∘ (i₁″ ∘ [ ι₁ , ι₂ ]′) +₁ (i₂″ ∘ [ ι₁ , ι₂ ]′) ≈⟨ refl⟩∘⟨ elimʳ +-η ⟩⊗⟨ elimʳ +-η ⟩
+ μ ∘ i₁″ +₁ i₂″ ≈⟨ μ∘+ ⟨
+ [ i₁″ , i₂″ ]′ ∎
+
+ module _ where
+
+ open 𝒟 using (U; _⊗₁_; module ⊗; module unitorˡ; module unitorʳ; monoidal; assoc-commute-from; assoc-commute-to)
+ open Category U
+ open ⇒-Reasoning U
+ open Equiv
+ open ⊗-Reasoning monoidal
+ open smc𝒞 using () renaming (associator to α)
+ open 𝒟 using () renaming (associator to α′)
+ open Morphism._≅_
+
+ swap-unit : 𝒟.braiding.⇐.η (𝒟.unit , 𝒟.unit) ≈ 𝒟.id
+ swap-unit = cancel-toʳ 𝒟.unitorˡ
+ ( braiding-coherence-inv 𝒟.braided
+ ○ sym (coherence-inv₃ monoidal)
+ ○ sym 𝒟.identityˡ)
+
+ φ-swap-inner : φ (N + M , N′ + M′) ∘ (φ (N , M) ∘ s ⊗₁ t) ⊗₁ (φ (N′ , M′) ∘ s′ ⊗₁ t′)
+ ≈ F.F₁ swap-inner ∘ φ (N + N′ , M + M′) ∘ (φ (N , N′) ∘ s ⊗₁ s′) ⊗₁ (φ (M , M′) ∘ t ⊗₁ t′)
+ φ-swap-inner = refl⟩∘⟨ ⊗-distrib-over-∘
+   ○ extendʳ
+ ( insertˡ ([ F.F ]-resp-≅ α .isoˡ) ⟩∘⟨ serialize₁₂
+ ○ center (assoc ○ F.associativity)
+ ○ refl⟩∘⟨
+ (extendˡ
+ ( refl⟩∘⟨ sym ⊗.identity ⟩⊗⟨refl
+ ○ extendˡ assoc-commute-from
+ ○ ( merge₂ʳ
+ ○ sym F.identity ⟩⊗⟨
+ ( switch-fromtoʳ α′ (assoc ○ (sym F.associativity))
+ ○ ( refl⟩∘⟨
+ ( refl⟩∘⟨
+ ( switch-fromtoʳ 𝒟.braiding.FX≅GX (sym F.braiding-compat) ⟩⊗⟨refl
+ ○ assoc ⟩⊗⟨refl
+ ○ split₁ʳ
+ ○ refl⟩⊗⟨ sym F.identity ⟩∘⟨refl)
+ ○ extendʳ (φ-commute (_ , 𝒞.id))
+ ○ refl⟩∘⟨
+ ( refl⟩∘⟨ split₁ˡ
+ ○ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α) F.associativity))
+ ○ pullˡ (sym F.homomorphism))
+ ○ pullˡ (sym F.homomorphism)) ⟩∘⟨refl
+ ○ assoc)
+ ○ split₂ʳ) ⟩∘⟨refl)
+ ○ ( extendʳ (φ-commute (𝒞.id , _))
+ ○ refl⟩∘⟨
+ ( refl⟩∘⟨ split₂ʳ
+ ○ extendʳ
+ ( refl⟩∘⟨ (refl⟩⊗⟨ assoc ○ split₂ʳ)
+ ○ extendʳ (switch-fromtoʳ α′ (assoc ○ (sym F.associativity)))
+ ○ refl⟩∘⟨
+ ( refl⟩∘⟨ (refl⟩⊗⟨ assoc ○ split₂ʳ)
+ ○ extendʳ assoc-commute-to
+ ○ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl)
+ ○ extendʳ (assoc ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym serialize₁₂))))
+ ○ pullˡ (sym F.homomorphism)
+ ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ pullʳ merge₂ʳ) ) ⟩∘⟨refl )
+ ○ center⁻¹ (sym F.homomorphism) assoc)
+ ○ refl⟩∘⟨
+ ( pullʳ
+ ( extendˡ assoc-commute-from
+ ○ ( pullʳ
+ ( merge₂ˡ
+ ○ refl⟩⊗⟨
+ ( extendˡ assoc-commute-to
+ ○ ( pullʳ (sym split₁ˡ ○ (𝒟.braiding.⇐.commute (s′ , t) ○ elimʳ swap-unit) ⟩⊗⟨refl)
+ ○ assoc-commute-from ) ⟩∘⟨refl
+ ○ cancelʳ 𝒟.associator.isoʳ))
+ ○ assoc-commute-to) ⟩∘⟨refl
+ ○ cancelʳ 𝒟.associator.isoˡ)
+ ○ pullʳ (sym ⊗-distrib-over-∘))
+
+ open Shorthands monoidal
+
+ same-deco
+ : (F.₁ Q+Q′≅Q″.from ∘ φ (Q , Q′) ∘ (F.₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ (F.₁ [ i₁′ , i₂′ ]′ ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐) ∘ ρ⇐)
+ ≈ (F.₁ [ i₁″ , i₂″ ]′ ∘ φ (N + N′ , M + M′) ∘ (φ (N , N′) ∘ s ⊗₁ s′ ∘ ρ⇐) ⊗₁ (φ (M , M′) ∘ t ⊗₁ t′ ∘ ρ⇐) ∘ ρ⇐)
+ same-deco =
+ refl⟩∘⟨
+ ( refl⟩∘⟨ pushˡ ⊗-distrib-over-∘
+ ○ extendʳ (φ-commute ([ i₁ , i₂ ]′ , [ i₁′ , i₂′ ]′))
+ ○ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩⊗⟨ sym-assoc ⟩∘⟨refl
+ ○ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘
+ ○ refl⟩∘⟨ sym-assoc)
+ ○ pullˡ (sym F.homomorphism)
+ ○ extendʳ (pushʳ φ-swap-inner)
+ ○ (sym F.homomorphism ○ F.F-resp-≈ ≅∘[]+[]∘σ₄) ⟩∘⟨refl
+ ○ refl⟩∘⟨
+ ( assoc
+ ○ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘)
+ ○ refl⟩∘⟨ assoc ⟩⊗⟨ assoc ⟩∘⟨refl)
+
+⊗-resp-≈
+ : {A A′ B B′ : Obj}
+ {f f′ : Cospans [ A , B ]}
+ {g g′ : Cospans [ A′ , B′ ]}
+ → Cospans [ f ≈ f′ ]
+ → Cospans [ g ≈ g′ ]
+ → Cospans [ together f g ≈ together f′ g′ ]
+⊗-resp-≈ {_} {_} {_} {_} {f} {f′} {g} {g′} ≈f ≈g = record
+ { cospans-≈ = Stack.⊗-resp-≈ (≈f .cospans-≈) (≈g .cospans-≈)
+ ; same-deco = same-deco
+ }
+ where
+
+ open _≈_′ using (cospans-≈)
+
+ module SameNames where
+ open _≈_′ ≈f using () renaming (same-deco to ≅∘s≈t) public
+ open _≈_′ ≈g using () renaming (same-deco to ≅∘s≈t′) public
+ open Cospan._≈_ (≈f .cospans-≈) using (module ≅N) public
+ open Cospan._≈_ (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public
+
+ open SameNames
+
+ module DecorationNames where
+ open DecoratedCospan f using (N) renaming (decoration to s) public
+ open DecoratedCospan f′ using () renaming (decoration to t; N to M) public
+ open DecoratedCospan g using () renaming (decoration to s′; N to N′) public
+ open DecoratedCospan g′ using () renaming (decoration to t′; N to M′) public
+
+ open DecorationNames
+
+ module _ where
+ open 𝒞 using (_⇒_)
+ ≅ : N ⇒ M
+ ≅ = ≅N.from
+ ≅′ : N′ ⇒ M′
+ ≅′ = ≅N′.from
+
+ open 𝒞 using (_+₁_)
+
+ module _ where
+
+ open 𝒟 using (U; monoidal; _⊗₁_)
+ open Category U
+ open Equiv
+ open ⇒-Reasoning U
+ open ⊗-Reasoning monoidal
+ open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+ open F using (F₁)
+ open Shorthands monoidal
+
+ same-deco : F₁ (≅ +₁ ≅′) ∘ φ (N , N′) ∘ s ⊗₁ s′ ∘ ρ⇐ ≈ φ (M , M′) ∘ t ⊗₁ t′ ∘ ρ⇐
+ same-deco = begin
+ F₁ (≅ +₁ ≅′) ∘ φ (N , N′) ∘ s ⊗₁ s′ ∘ ρ⇐ ≈⟨ extendʳ (φ-commute (_ , _)) ⟨
+ φ (M , M′) ∘ F₁ ≅ ⊗₁ F₁ ≅′ ∘ s ⊗₁ s′ ∘ ρ⇐ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩
+ φ (M , M′) ∘ (F₁ ≅ ∘ s) ⊗₁ (F₁ ≅′ ∘ s′) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ ≅∘s≈t ⟩⊗⟨ ≅∘s≈t′ ⟩∘⟨refl ⟩
+ φ (M , M′) ∘ t ⊗₁ t′ ∘ ρ⇐ ∎
+
+⊗ : 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
+ }
+
+module ⊗ = Functor ⊗
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 22:09:55 +0000