Finish category of decorated cospans

2 files changed, 338 insertions, 106 deletions

diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index ccefcf5..0dee26c 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -9,24 +9,23 @@ module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o
 
 open FinitelyCocompleteCategory 𝒞
 
-open import Categories.Diagram.Duality U using (Pushout⇒coPullback)
 open import Categories.Diagram.Pushout U using (Pushout)
-open import Categories.Diagram.Pushout.Properties U using (glue; swap; pushout-resp-≈)
+open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈)
 open import Categories.Morphism U using (_≅_; module ≅)
-open import Categories.Morphism.Duality U using (op-≅⇒≅)
-open import Categories.Morphism.Reasoning U using
+open import Categories.Morphism.Reasoning U
+  using
     ( switch-fromtoˡ
     ; glueTrianglesˡ
-    ; id-comm
-    ; id-comm-sym
-    ; pullˡ
-    ; pullʳ
-    ; assoc²''
-    ; assoc²'
+    ; pullˡ ; pullʳ
     )
 
-import Categories.Diagram.Pullback op as Pb using (up-to-iso)
-
+open import Category.Diagram.Pushout U 
+  using
+    ( glue-i₁ ; glue-i₂
+    ; up-to-iso
+    ; pushout-f-id ; pushout-id-g
+    ; extend-i₁-iso ; extend-i₂-iso
+    )
 
 private
 
@@ -102,89 +101,6 @@ same-trans C≈C′ C′≈C″ = record
     module C≈C′ = Same C≈C′
     module C′≈C″ = Same C′≈C″
 
-glue-i₁ : (p : Pushout f g) → Pushout h (Pushout.i₁ p) → Pushout (h ∘ f) g
-glue-i₁ p = glue p
-
-glue-i₂ : (p₁ : Pushout f g) → Pushout (Pushout.i₂ p₁) h → Pushout f (h ∘ g)
-glue-i₂ p₁ p₂ = swap (glue (swap p₁) (swap p₂))
-
-up-to-iso : (p p′ : Pushout f g) → Pushout.Q p ≅ Pushout.Q p′
-up-to-iso p p′ = op-≅⇒≅ (Pb.up-to-iso (Pushout⇒coPullback p) (Pushout⇒coPullback p′))
-
-pushout-f-id : Pushout f id
-pushout-f-id {_} {_} {f} = record
-    { i₁ = id
-    ; i₂ = f
-    ; commute = id-comm-sym
-    ; universal = λ {B} {h₁} {h₂} eq → h₁
-    ; unique = λ {E} {h₁} {h₂} {eq} {j} j∘i₁≈h₁ j∘i₂≈h₂ → Equiv.sym identityʳ ○ j∘i₁≈h₁
-    ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → identityʳ
-    ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → eq ○ identityʳ
-    }
-  where
-    open HomReasoning
-
-pushout-id-g : Pushout id g
-pushout-id-g {_} {_} {g} = record
-    { i₁ = g
-    ; i₂ = id
-    ; commute = id-comm
-    ; universal = λ {B} {h₁} {h₂} eq → h₂
-    ; unique = λ {E} {h₁} {h₂} {eq} {j} j∘i₁≈h₁ j∘i₂≈h₂ → Equiv.sym identityʳ ○ j∘i₂≈h₂
-    ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → Equiv.sym eq ○ identityʳ
-    ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → identityʳ
-    }
-  where
-    open HomReasoning
-
-extend-i₁-iso
-    : {f : A ⇒ B}
-      {g : A ⇒ C}
-      (p : Pushout f g)
-      (B≅D : B ≅ D)
-    → Pushout (_≅_.from B≅D ∘ f) g
-extend-i₁-iso {_} {_} {_} {_} {f} {g} p B≅D = record
-    { i₁ = P.i₁ ∘ B≅D.to
-    ; i₂ = P.i₂
-    ; commute = begin
-          (P.i₁ ∘ B≅D.to) ∘ B≅D.from ∘ f  ≈⟨ assoc²'' ⟨
-          P.i₁ ∘ (B≅D.to ∘ B≅D.from) ∘ f  ≈⟨ refl⟩∘⟨ B≅D.isoˡ ⟩∘⟨refl ⟩
-          P.i₁ ∘ id ∘ f                   ≈⟨ refl⟩∘⟨ identityˡ ⟩
-          P.i₁ ∘ f                        ≈⟨ P.commute ⟩
-          P.i₂ ∘ g                        ∎
-    ; universal = λ { eq → P.universal (assoc ○ eq) }
-    ; unique = λ {_} {h₁} {_} {j} ≈₁ ≈₂ →
-          let
-            ≈₁′ = begin
-                j ∘ P.i₁                        ≈⟨ refl⟩∘⟨ identityʳ ⟨
-                j ∘ P.i₁ ∘ id                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ B≅D.isoˡ ⟨
-                j ∘ P.i₁ ∘ B≅D.to ∘ B≅D.from    ≈⟨ assoc²' ⟨
-                (j ∘ P.i₁ ∘ B≅D.to) ∘ B≅D.from  ≈⟨ ≈₁ ⟩∘⟨refl ⟩
-                h₁ ∘ B≅D.from                   ∎
-          in P.unique ≈₁′ ≈₂
-    ; universal∘i₁≈h₁ = λ {E} {h₁} {_} {eq} →
-        begin
-            P.universal (assoc ○ eq) ∘ P.i₁ ∘ B≅D.to    ≈⟨ sym-assoc ⟩
-            (P.universal (assoc ○ eq) ∘ P.i₁) ∘ B≅D.to  ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
-            (h₁ ∘ B≅D.from) ∘ B≅D.to                    ≈⟨ assoc ⟩
-            h₁ ∘ B≅D.from ∘ B≅D.to                      ≈⟨ refl⟩∘⟨ B≅D.isoʳ ⟩
-            h₁ ∘ id                                     ≈⟨ identityʳ ⟩
-            h₁                                          ∎
-    ; universal∘i₂≈h₂ = P.universal∘i₂≈h₂
-    }
-  where
-    module P = Pushout p
-    module B≅D = _≅_ B≅D
-    open HomReasoning
-
-extend-i₂-iso
-    : {f : A ⇒ B}
-      {g : A ⇒ C}
-      (p : Pushout f g)
-      (C≅D : C ≅ D)
-    → Pushout f (_≅_.from C≅D ∘ g)
-extend-i₂-iso {_} {_} {_} {_} {f} {g} p C≅D = swap (extend-i₁-iso (swap p) C≅D)
-
 compose-idˡ : {C : Cospan A B} → Same (compose C identity) C
 compose-idˡ {_} {_} {C} = record
     { ≅N = ≅P
diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda
index 8d67536..92a1de9 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -15,17 +15,23 @@ module Category.Instance.DecoratedCospans
     {𝒟 : SymmetricMonoidalCategory o ℓ e}
     (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
 
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+module 𝒟 = SymmetricMonoidalCategory 𝒟
+
 import Category.Instance.Cospans 𝒞 as Cospans
 
-open import Categories.Category
-  using (Category; _[_∘_]; _[_≈_])
+open import Categories.Category using (Category; _[_∘_])
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
 open import Categories.Diagram.Pushout using (Pushout)
 open import Categories.Functor.Properties using ([_]-resp-≅)
 open import Categories.Morphism.Reasoning using (switch-fromtoˡ; glueTrianglesˡ)
 open import Cospan.Decorated 𝒞 F using (DecoratedCospan)
 open import Data.Product using (_,_)
+open import Function using (flip)
 open import Level using (_⊔_)
 
+open import Category.Diagram.Pushout 𝒞.U using (glue-i₁; glue-i₂; pushout-id-g; pushout-f-id; up-to-iso)
+
 import Category.Monoidal.Coherence as Coherence
 
 import Categories.Morphism as Morphism
@@ -33,11 +39,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning
 import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
 
 
-module 𝒞 = FinitelyCocompleteCategory 𝒞
-module 𝒟 = SymmetricMonoidalCategory 𝒟
-
 open SymmetricMonoidalFunctor F
-  -- using (F₀; F₁; ⊗-homo; ε; homomorphism)
   renaming (identity to F-identity; F to F′)
 
 private
@@ -76,7 +78,7 @@ record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e) where
   field
     cospans-≈ : Cospans.Same C₁.cospan C₂.cospan
 
-  open Cospans.Same cospans-≈
+  open Cospans.Same cospans-≈ public
   open 𝒟
   open Morphism U using (_≅_)
 
@@ -135,8 +137,8 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
     module P₁ = Pushout p₁
     module P₂ = Pushout p₂
     p₃ = pushout P₁.i₂ P₂.i₁
-    p₁₃ = Cospans.glue-i₂ p₁ p₃
-    p₂₃ = Cospans.glue-i₁ p₂ p₃
+    p₁₃ = glue-i₂ p₁ p₃
+    p₂₃ = glue-i₁ p₂ p₃
     p₄ = pushout C₁.f₂ (P₂.i₁ ∘′ C₂.f₁)
     p₅ = pushout (P₁.i₂ ∘′ C₂.f₂) C₃.f₁
     module P₃ = Pushout p₃
@@ -145,8 +147,8 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
     module P₁₃ = Pushout p₁₃
     module P₂₃ = Pushout p₂₃
     open Morphism 𝒞.U using (_≅_)
-    module P₄≅P₁₃ = _≅_ (Cospans.up-to-iso p₄ p₁₃)
-    module P₅≅P₂₃ = _≅_ (Cospans.up-to-iso p₅ p₂₃)
+    module P₄≅P₁₃ = _≅_ (up-to-iso p₄ p₁₃)
+    module P₅≅P₂₃ = _≅_ (up-to-iso p₅ p₂₃)
 
     N = C₁.N
     M = C₂.N
@@ -332,3 +334,317 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
           F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ F₁ id′ ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐                         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨ refl ⟩
           F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ id ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨
           F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐                                   ∎
+
+compose-idʳ : {C : DecoratedCospan A B} → Same (compose identity C) C
+compose-idʳ {A} {_} {C} = record
+    { cospans-≈ = Cospans.compose-idʳ
+    ; same-deco = deco-id
+    }
+  where
+
+    open DecoratedCospan C
+
+    open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡)
+
+    P = pushout 𝒞.id f₁
+    P′ = pushout-id-g {g = f₁}
+    ≅P = up-to-iso P P′
+
+    open Morphism 𝒞.U using (_≅_)
+    module ≅P = _≅_ ≅P
+
+    open Pushout P
+
+    open 𝒞
+      using (cocartesian)
+      renaming (id to id′; _∘_ to _∘′_)
+
+    open CocartesianMonoidal 𝒞.U cocartesian using (⊥+A≅A)
+
+    module ⊥+A≅A {a} = _≅_ (⊥+A≅A {a})
+
+    module _ where
+
+      open 𝒞
+        using
+          ( _⇒_ ; _∘_ ; _≈_ ; id ; U
+          ; identity²
+          ; cocartesian ; initial ; ¡-unique
+          ; ∘[] ; []∘+₁ ; inject₂ ; assoc
+          ; module HomReasoning ; module Dual ; module Equiv
+          )
+
+      open Equiv
+
+      open Dual.op-binaryProducts cocartesian
+        using ()
+        renaming (⟨⟩-cong₂ to []-cong₂)
+
+      open ⇒-Reasoning U
+      open HomReasoning
+
+      copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to ≈ id
+      copairing-id = begin
+        ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to        ≈⟨ assoc ⟩
+        (≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id) ∘ ⊥+A≅A.to          ≈⟨ assoc ⟩
+        ≅P.from ∘ [ i₁ , i₂ ] ∘ (¡ +₁ id) ∘ ⊥+A≅A.to            ≈⟨ pullˡ ∘[] ⟩
+        [ ≅P.from ∘ i₁ , ≅P.from ∘ i₂ ] ∘ (¡ +₁ id) ∘ ⊥+A≅A.to  ≈⟨ pullˡ []∘+₁ ⟩
+        [ (≅P.from ∘ i₁) ∘ ¡ , (≅P.from ∘ i₂) ∘ id ] ∘ ⊥+A≅A.to ≈⟨ []-cong₂ (universal∘i₁≈h₁ ⟩∘⟨refl) (universal∘i₂≈h₂ ⟩∘⟨refl) ⟩∘⟨refl ⟩
+        [ f₁ ∘ ¡ , id ∘ id ] ∘ ⊥+A≅A.to                         ≈⟨ []-cong₂ (sym (¡-unique (f₁ ∘ ¡))) identity² ⟩∘⟨refl ⟩
+        [ ¡ , id ] ∘ ⊥+A≅A.to                                   ≈⟨ inject₂ ⟩
+        id                                                      ∎
+
+    module _ where
+
+      open 𝒟
+        using
+          ( id ; _∘_ ; _≈_ ; _⇒_ ; U
+          ; assoc ; sym-assoc; identityˡ
+          ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ
+          )
+
+      open ⊗-Reasoning monoidal
+      open ⇒-Reasoning U
+
+      φ = ⊗-homo.⇒.η
+      φ-commute = ⊗-homo.⇒.commute
+
+      module λ≅ = unitorˡ
+      λ⇒ = λ≅.from
+      λ⇐ = unitorˡ.to
+      ρ⇐ = unitorʳ.to
+
+      open Coherence monoidal using (λ₁≅ρ₁⇐)
+      open 𝒟.Equiv
+
+      s : unit ⇒ F₀ N
+      s = decoration
+
+      cohere-s : φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐ ≈ F₁ ⊥+A≅A.to ∘ s
+      cohere-s = begin
+          φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐                                                  ≈⟨ identityˡ ⟨
+          id ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐                                             ≈⟨ F-identity ⟩∘⟨refl ⟨
+          F₁ id′ ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐                                         ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨
+          F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐                    ≈⟨ pushˡ homomorphism ⟩
+          F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+          F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ id) ∘ (id ⊗₁ s) ∘ ρ⇐       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
+          F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ (⊥ , N) ∘ (ε.from ⊗₁ id)) ∘ (id ⊗₁ s) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ pullˡ unitaryˡ ⟩
+          F₁ ⊥+A≅A.to ∘ λ⇒ ∘ (id ⊗₁ s) ∘ ρ⇐                                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ λ₁≅ρ₁⇐ ⟨
+          F₁ ⊥+A≅A.to ∘ λ⇒ ∘ (id ⊗₁ s) ∘ λ⇐                                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-to ⟨
+          F₁ ⊥+A≅A.to ∘ λ⇒ ∘ λ⇐ ∘ s                                                       ≈⟨ refl⟩∘⟨ cancelˡ λ≅.isoʳ ⟩
+          F₁ ⊥+A≅A.to ∘ s                                                                 ∎
+
+      deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε.from) ⊗₁ s ∘ ρ⇐ ≈ s
+      deco-id = begin
+          F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε.from) ⊗₁ s ∘ ρ⇐             ≈⟨ pushˡ homomorphism ⟨
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε.from) ⊗₁ s ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ id) ∘ (ε.from ⊗₁ s) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε.from ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , id′)) ⟩
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐    ≈⟨ pushˡ homomorphism ⟨
+          F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐    ≈⟨ refl⟩∘⟨ cohere-s ⟩
+          F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ F₁ ⊥+A≅A.to ∘ s                   ≈⟨ pushˡ homomorphism ⟨
+          F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘′ ⊥+A≅A.to) ∘ s                   ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩
+          F₁ id′ ∘ s                                                                      ≈⟨ F-identity ⟩∘⟨refl ⟩
+          id ∘ s                                                                          ≈⟨ identityˡ ⟩
+          s                                                                               ∎
+
+compose-idˡ : {C : DecoratedCospan A B} → Same (compose C identity) C
+compose-idˡ {_} {B} {C} = record
+    { cospans-≈ = Cospans.compose-idˡ
+    ; same-deco = deco-id
+    }
+  where
+
+    open DecoratedCospan C
+
+    open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡)
+
+    P = pushout f₂ 𝒞.id
+    P′ = pushout-f-id {f = f₂}
+    ≅P = up-to-iso P P′
+
+    open Morphism 𝒞.U using (_≅_)
+    module ≅P = _≅_ ≅P
+
+    open Pushout P
+
+    open 𝒞
+      using (cocartesian)
+      renaming (id to id′; _∘_ to _∘′_)
+
+    open CocartesianMonoidal 𝒞.U cocartesian using (A+⊥≅A)
+
+    module A+⊥≅A {a} = _≅_ (A+⊥≅A {a})
+
+    module _ where
+
+      open 𝒞
+        using
+          ( _⇒_ ; _∘_ ; _≈_ ; id ; U
+          ; identity²
+          ; cocartesian ; initial ; ¡-unique
+          ; ∘[] ; []∘+₁ ; inject₁ ; assoc
+          ; module HomReasoning ; module Dual ; module Equiv
+          )
+
+      open Equiv
+
+      open Dual.op-binaryProducts cocartesian
+        using ()
+        renaming (⟨⟩-cong₂ to []-cong₂)
+
+      open ⇒-Reasoning U
+      open HomReasoning
+
+      copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to ≈ id
+      copairing-id = begin
+        ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to        ≈⟨ assoc ⟩
+        (≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡) ∘ A+⊥≅A.to          ≈⟨ assoc ⟩
+        ≅P.from ∘ [ i₁ , i₂ ] ∘ (id +₁ ¡) ∘ A+⊥≅A.to            ≈⟨ pullˡ ∘[] ⟩
+        [ ≅P.from ∘ i₁ , ≅P.from ∘ i₂ ] ∘ (id +₁ ¡) ∘ A+⊥≅A.to  ≈⟨ pullˡ []∘+₁ ⟩
+        [ (≅P.from ∘ i₁) ∘ id , (≅P.from ∘ i₂) ∘ ¡ ] ∘ A+⊥≅A.to ≈⟨ []-cong₂ (universal∘i₁≈h₁ ⟩∘⟨refl) (universal∘i₂≈h₂ ⟩∘⟨refl) ⟩∘⟨refl ⟩
+        [ id ∘ id , f₂ ∘ ¡ ] ∘ A+⊥≅A.to                         ≈⟨ []-cong₂ identity² (sym (¡-unique (f₂ ∘ ¡))) ⟩∘⟨refl ⟩
+        [ id , ¡ ] ∘ A+⊥≅A.to                                   ≈⟨ inject₁ ⟩
+        id                                                      ∎
+
+    module _ where
+
+      open 𝒟
+        using
+          ( id ; _∘_ ; _≈_ ; _⇒_ ; U
+          ; assoc ; sym-assoc; identityˡ
+          ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ
+          ; unitorʳ-commute-to
+          ; module Equiv
+          )
+
+      open Equiv
+      open ⊗-Reasoning monoidal
+      open ⇒-Reasoning U
+
+      φ = ⊗-homo.⇒.η
+      φ-commute = ⊗-homo.⇒.commute
+
+      module ρ≅ = unitorʳ
+      ρ⇒ = ρ≅.from
+      ρ⇐ = ρ≅.to
+
+      s : unit ⇒ F₀ N
+      s = decoration
+
+      cohere-s : φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐ ≈ F₁ A+⊥≅A.to ∘ s
+      cohere-s = begin
+          φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐                                                  ≈⟨ identityˡ ⟨
+          id ∘ φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐                                             ≈⟨ F-identity ⟩∘⟨refl ⟨
+          F₁ id′ ∘ φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐                                         ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨
+          F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐                    ≈⟨ pushˡ homomorphism ⟩
+          F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
+          F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (id ⊗₁ ε.from) ∘ (s ⊗₁ id) ∘ ρ⇐       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
+          F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ (N , ⊥) ∘ (id ⊗₁ ε.from)) ∘ (s ⊗₁ id) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ pullˡ unitaryʳ ⟩
+          F₁ A+⊥≅A.to ∘ ρ⇒ ∘ (s ⊗₁ id) ∘ ρ⇐                                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-to ⟨
+          F₁ A+⊥≅A.to ∘ ρ⇒ ∘ ρ⇐ ∘ s                                                       ≈⟨ refl⟩∘⟨ cancelˡ ρ≅.isoʳ ⟩
+          F₁ A+⊥≅A.to ∘ s                                                                 ∎
+
+      deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε.from) ∘ ρ⇐ ≈ s
+      deco-id = begin
+          F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε.from) ∘ ρ⇐             ≈⟨ pushˡ homomorphism ⟨
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε.from) ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (id ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε.from) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (F₁ id′ ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε.from) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , ¡)) ⟩
+          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐    ≈⟨ pushˡ homomorphism ⟨
+          F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐    ≈⟨ refl⟩∘⟨ cohere-s ⟩
+          F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ F₁ A+⊥≅A.to ∘ s                   ≈⟨ pushˡ homomorphism ⟨
+          F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘′ A+⊥≅A.to) ∘ s                   ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩
+          F₁ id′ ∘ s                                                                      ≈⟨ F-identity ⟩∘⟨refl ⟩
+          id ∘ s                                                                          ≈⟨ identityˡ ⟩
+          s                                                                               ∎
+
+compose-id² : Same {A} (compose identity identity) identity
+compose-id² = compose-idˡ
+
+compose-equiv
+    : {c₂ c₂′ : DecoratedCospan B C}
+      {c₁ c₁′ : DecoratedCospan A B}
+    → Same c₂ c₂′
+    → Same c₁ c₁′
+    → Same (compose c₁ c₂) (compose c₁′ c₂′)
+compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = record
+    { cospans-≈ = ≅C₂∘C₁
+    ; same-deco = F≅N∘C₂∘C₁≈C₂′∘C₁′
+    }
+  where
+    module ≅C₁ = Same ≅C₁
+    module ≅C₂ = Same ≅C₂
+    module C₁ = DecoratedCospan c₁
+    module C₁′ = DecoratedCospan c₁′
+    module C₂ = DecoratedCospan c₂
+    module C₂′ = DecoratedCospan c₂′
+    ≅C₂∘C₁ = Cospans.compose-equiv ≅C₂.cospans-≈ ≅C₁.cospans-≈
+    module ≅C₂∘C₁ = Cospans.Same ≅C₂∘C₁
+    P = 𝒞.pushout C₁.f₂ C₂.f₁
+    P′ = 𝒞.pushout C₁′.f₂ C₂′.f₁
+    module P = Pushout P
+    module P′ = Pushout P′
+
+    s = C₁.decoration
+    t = C₂.decoration
+    s′ = C₁′.decoration
+    t′ = C₂′.decoration
+    N = C₁.N
+    M = C₂.N
+    N′ = C₁′.N
+    M′ = C₂′.N
+
+    φ = ⊗-homo.⇒.η
+    φ-commute = ⊗-homo.⇒.commute
+
+    Q⇒ = ≅C₂∘C₁.≅N.from
+    N⇒ = ≅C₁.≅N.from
+    M⇒ = ≅C₂.≅N.from
+
+    module _ where
+
+      ρ⇒ = 𝒟.unitorʳ.from
+      ρ⇐ = 𝒟.unitorʳ.to
+
+      open 𝒞 using ([_,_]; ∘[]; _+₁_; []∘+₁) renaming (_∘_ to _∘′_)
+      open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian
+          using ()
+          renaming (⟨⟩-cong₂ to []-cong₂)
+
+      open 𝒟
+
+      open ⊗-Reasoning monoidal
+      open ⇒-Reasoning U
+
+      F≅N∘C₂∘C₁≈C₂′∘C₁′ : F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈ F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐
+      F≅N∘C₂∘C₁≈C₂′∘C₁′ = begin
+          F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐                  ≈⟨ pushˡ homomorphism ⟨
+          F₁ (Q⇒ ∘′ [ P.i₁ , P.i₂ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐                  ≈⟨ F-resp-≈ ∘[] ⟩∘⟨refl ⟩
+          F₁ ([ Q⇒ ∘′ P.i₁ , Q⇒ ∘′ P.i₂ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐            ≈⟨ F-resp-≈ ([]-cong₂ P.universal∘i₁≈h₁ P.universal∘i₂≈h₂) ⟩∘⟨refl ⟩
+          F₁ ([ P′.i₁ ∘′ N⇒ , P′.i₂ ∘′ M⇒ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐          ≈⟨ F-resp-≈ []∘+₁ ⟩∘⟨refl ⟨
+          F₁ ([ P′.i₁ , P′.i₂ ] ∘′ (N⇒ +₁ M⇒)) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐        ≈⟨ pushˡ homomorphism ⟩
+          F₁ [ P′.i₁ , P′.i₂ ] ∘ F₁ (N⇒ +₁ M⇒) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐        ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (N⇒ , M⇒)) ⟨
+          F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ F₁ N⇒ ⊗₁ F₁ M⇒ ∘ s ⊗₁ t ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟨
+          F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ (F₁ N⇒ ∘ s) ⊗₁ (F₁ M⇒ ∘ t) ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ≅C₁.same-deco ⟩⊗⟨ ≅C₂.same-deco ⟩∘⟨refl ⟩
+          F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐                    ∎
+
+Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e)
+Cospans = record
+    { Obj = 𝒞.Obj
+    ; _⇒_ = DecoratedCospan
+    ; _≈_ = Same
+    ; id = identity
+    ; _∘_ = flip compose
+    ; assoc = compose-assoc
+    ; sym-assoc = same-sym (compose-assoc)
+    ; identityˡ = compose-idˡ
+    ; identityʳ = compose-idʳ
+    ; identity² = compose-id²
+    ; equiv = record
+        { refl = same-refl
+        ; sym = same-sym
+        ; trans = same-trans
+        }
+    ; ∘-resp-≈ = compose-equiv
+    }