aboutsummaryrefslogtreecommitdiff
path: root/Functor
diff options
context:
space:
mode:
Diffstat (limited to 'Functor')
-rw-r--r--Functor/Instance/DecoratedCospan/Stack.agda425
1 files changed, 425 insertions, 0 deletions
diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda
new file mode 100644
index 0000000..5c3c232
--- /dev/null
+++ b/Functor/Instance/DecoratedCospan/Stack.agda
@@ -0,0 +1,425 @@
+{-# 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.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; Same to Same′)
+open import Category.Instance.Cospans 𝒞 using (Same; compose)
+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 = Stack.together A⇒B.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-≈ : Same (Stack.together _ _) (compose (Stack.together _ _) (Stack.together _ _))
+ cospans-≈ = Stack.homomorphism (f .cospan) (g .cospan) (f′ .cospan) (g′ .cospan)
+ open Same 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 (sym μ∘+) ⟩
+ ≅ ∘ μ ∘ (ι₁ +₁ ι₂) ∘ (μ ∘ 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 (sym 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 (sym 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 (sym 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 Same′ using (cospans-≈)
+
+ module SameNames where
+ open Same′ ≈f using () renaming (same-deco to ≅∘s≈t) public
+ open Same′ ≈g using () renaming (same-deco to ≅∘s≈t′) public
+ open Same (≈f .cospans-≈) using (module ≅N) public
+ open Same (≈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 }
+ }
generated by cgit v1.2.3 (git 2.39.1) at 2025-04-19 18:46:00 +0000