Add opaqueness to cospans and decorated cospans

2 files changed, 511 insertions, 419 deletions

diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index d54499d..ae6d359 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -7,16 +7,20 @@ open import Level using (_⊔_)
 
 module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
 
-open FinitelyCocompleteCategory 𝒞
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+open 𝒞 using (U; pushout)
+open Category U hiding (_≈_)
 
 open import Categories.Diagram.Pushout U using (Pushout)
 open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso)
+open import Relation.Binary using (IsEquivalence)
 open import Categories.Morphism U using (_≅_; module ≅)
 open import Categories.Morphism.Reasoning U
   using
     ( switch-fromtoˡ
     ; glueTrianglesˡ
     ; pullˡ ; pullʳ
+    ; cancelˡ
     )
 
 open import Category.Diagram.Pushout U 
@@ -26,254 +30,296 @@ open import Category.Diagram.Pushout U 
     ; extend-i₁-iso ; extend-i₂-iso
     )
 
-private
-
-  variable
-    A B C D X Y Z : Obj
-    f g h : A ⇒ B
-
 record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
 
+  constructor cospan
+
   field
     {N} : Obj
     f₁  : A ⇒ N
     f₂  : B ⇒ N
 
+private
+  variable
+    A B C D : Obj
+
 compose : Cospan A B → Cospan B C → Cospan A C
-compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ }
+compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
   where
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module p = pushout C₁.f₂ C₂.f₁
+    open pushout g h
 
-id-Cospan : Cospan A A
-id-Cospan = record { f₁ = id ; f₂ = id }
+identity : Cospan A A
+identity = cospan id id
 
 compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
-compose-3 c₁ c₂ c₃ = record { f₁ = P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ ; f₂ = P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ }
+compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
   where
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module C₃ = Cospan c₃
-    module P₁ = pushout C₁.f₂ C₂.f₁
-    module P₂ = pushout C₂.f₂ C₃.f₁
+    module P₁ = pushout f₂ g₁
+    module P₂ = pushout g₂ h₁
     module P₃ = pushout P₁.i₂ P₂.i₁
 
-record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where
+record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
 
   module C = Cospan C
-  module C′ = Cospan C′
+  module D = Cospan D
 
   field
-    ≅N : C.N ≅ C′.N
+    ≅N : C.N ≅ D.N
 
   open _≅_ ≅N public
   module ≅N = _≅_ ≅N
 
   field
-    from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁
-    from∘f₂≈f₂′ : from ∘ C.f₂ ≈ C′.f₂
+    from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
+    from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
+
+private
+  variable
+    f g h : Cospan A B
 
-same-refl : {C : Cospan A B} → Same C C
-same-refl = record
+≈-refl : f ≈ f
+≈-refl {f = cospan f₁ f₂} = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = identityˡ
-    ; from∘f₂≈f₂′ = identityˡ
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
+  where abstract
+    from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁
+    from∘f₁≈f₁ = identityˡ
+    from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂
+    from∘f₂≈f₂ = identityˡ
 
-same-sym : {C C′ : Cospan A B} → Same C C′ → Same C′ C
-same-sym C≅C′ = record
+≈-sym : f ≈ g → g ≈ f
+≈-sym f≈g = record
     { ≅N = ≅.sym ≅N
-    ; from∘f₁≈f₁′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁′)
-    ; from∘f₂≈f₂′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂′)
+    ; from∘f₁≈f₁ = a
+    ; from∘f₂≈f₂ = b
     }
-  where
-    open Same C≅C′
+  where abstract
+    open _≈_ f≈g
+    a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁
+    a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁)
+    b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂
+    b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂)
 
-same-trans : {C C′ C″ : Cospan A B} → Same C C′ → Same C′ C″ → Same C C″
-same-trans C≈C′ C′≈C″ = record
-    { ≅N = ≅.trans C≈C′.≅N C′≈C″.≅N
-    ; from∘f₁≈f₁′ = glueTrianglesˡ C′≈C″.from∘f₁≈f₁′ C≈C′.from∘f₁≈f₁′
-    ; from∘f₂≈f₂′ = glueTrianglesˡ C′≈C″.from∘f₂≈f₂′ C≈C′.from∘f₂≈f₂′
+≈-trans : f ≈ g → g ≈ h → f ≈ h
+≈-trans f≈g g≈h = record
+    { ≅N = ≅.trans f≈g.≅N g≈h.≅N
+    ; from∘f₁≈f₁ = a
+    ; from∘f₂≈f₂ = b
     }
-  where
-    module C≈C′ = Same C≈C′
-    module C′≈C″ = Same C′≈C″
+  where abstract
+    module f≈g = _≈_ f≈g
+    module g≈h = _≈_ g≈h
+    a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁
+    a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁
+    b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂
+    b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂
 
-compose-idˡ : {C : Cospan A B} → Same (compose C id-Cospan) C
-compose-idˡ {_} {_} {C} = record
+≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
+≈-equiv = record
+    { refl = ≈-refl
+    ; sym = ≈-sym
+    ; trans = ≈-trans
+    }
+
+compose-idˡ : compose f identity ≈ f
+compose-idˡ {f = cospan {N} f₁ f₂} = record
     { ≅N = ≅P
-    ; from∘f₁≈f₁′ = begin
-          ≅P.from ∘ P.i₁ ∘ C.f₁     ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₁) ∘ C.f₁   ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
-          id ∘ C.f₁                 ≈⟨ identityˡ ⟩
-          C.f₁                      ∎
-    ; from∘f₂≈f₂′ = begin
-          ≅P.from ∘ P.i₂ ∘ id       ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          ≅P.from ∘ P.i₂            ≈⟨ P.universal∘i₂≈h₂ ⟩
-          C.f₂                      ∎
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C = Cospan C
-    P = pushout C.f₂ id
+    P P′ : Pushout f₂ id
+    P = pushout f₂ id
+    P′ = pushout-f-id {f = f₂}
     module P = Pushout P
-    P′ = pushout-f-id {f = C.f₂}
+    ≅P : P.Q ≅ N
     ≅P = up-to-iso P P′
     module ≅P = _≅_ ≅P
+    abstract
+      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ f₁ 𝒞.≈ f₁
+      from∘f₁≈f₁ = begin
+          ≅P.from ∘ P.i₁ ∘ f₁ ≈⟨ cancelˡ P.universal∘i₁≈h₁ ⟩
+          f₁                  ∎
+      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ id 𝒞.≈ f₂
+      from∘f₂≈f₂ = begin
+          ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          ≅P.from ∘ P.i₂      ≈⟨ P.universal∘i₂≈h₂ ⟩
+          f₂                  ∎
 
-compose-idʳ : {C : Cospan A B} → Same (compose id-Cospan C) C
-compose-idʳ {_} {_} {C} = record
+compose-idʳ : compose identity f ≈ f
+compose-idʳ {f = cospan {N} f₁ f₂} = record
     { ≅N = ≅P
-    ; from∘f₁≈f₁′ = begin
-          ≅P.from ∘ P.i₁ ∘ id       ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          ≅P.from ∘ P.i₁            ≈⟨ P.universal∘i₁≈h₁ ⟩
-          C.f₁                      ∎
-    ; from∘f₂≈f₂′ = begin
-          ≅P.from ∘ P.i₂ ∘ C.f₂     ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₂) ∘ C.f₂   ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩
-          id ∘ C.f₂                 ≈⟨ identityˡ ⟩
-          C.f₂                      ∎
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C = Cospan C
-    P = pushout id C.f₁
+    P P′ : Pushout id f₁
+    P = pushout id f₁
     module P = Pushout P
-    P′ = pushout-id-g {g = C.f₁}
+    P′ = pushout-id-g {g = f₁}
+    ≅P : P.Q ≅ N
     ≅P = up-to-iso P P′
     module ≅P = _≅_ ≅P
+    abstract
+      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ id 𝒞.≈ f₁
+      from∘f₁≈f₁ = begin
+          ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          ≅P.from ∘ P.i₁      ≈⟨ P.universal∘i₁≈h₁ ⟩
+          f₁                  ∎
+      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ f₂ 𝒞.≈ f₂
+      from∘f₂≈f₂ = begin
+          ≅P.from ∘ P.i₂ ∘ f₂ ≈⟨ cancelˡ P.universal∘i₂≈h₂ ⟩
+          f₂                  ∎
 
-compose-id² : Same {A} (compose id-Cospan id-Cospan) id-Cospan
+compose-id² : compose identity identity ≈ identity {A}
 compose-id² = compose-idˡ
 
-compose-3-right
-    : {c₁ : Cospan A B}
-      {c₂ : Cospan B C}
-      {c₃ : Cospan C D}
-    → Same (compose c₁ (compose c₂ c₃)) (compose-3 c₁ c₂ c₃)
-compose-3-right {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
-    { ≅N = up-to-iso P₄′ P₄
-    ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc
-    ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl
+compose-3-right : compose f (compose g h) ≈ compose-3 f g h
+compose-3-right {f = f} {g = g} {h = h} = record
+    { ≅N = ≅N
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module C₃ = Cospan c₃
+    module C₁ = Cospan f
+    module C₂ = Cospan g
+    module C₃ = Cospan h
+    P₁ : Pushout C₁.f₂ C₂.f₁
     P₁ = pushout C₁.f₂ C₂.f₁
+    P₂ : Pushout C₂.f₂ C₃.f₁
     P₂ = pushout C₂.f₂ C₃.f₁
     module P₁ = Pushout P₁
     module P₂ = Pushout P₂
+    P₃ : Pushout P₁.i₂ P₂.i₁
     P₃ = pushout P₁.i₂ P₂.i₁
     module P₃ = Pushout P₃
+    P₄ P₄′ : Pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
     P₄ = glue-i₂ P₁ P₃
-    module P₄ = Pushout P₄
     P₄′ = pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
+    module P₄ = Pushout P₄
     module P₄′ = Pushout P₄′
+    ≅N : P₄′.Q ≅ P₄.Q
+    ≅N = up-to-iso P₄′ P₄
+    module ≅N = _≅_ ≅N
+    abstract
+      from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ C₁.f₁ 𝒞.≈ P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁
+      from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc
+      from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ P₂.i₂ ∘ C₃.f₂ 𝒞.≈ P₄.i₂ ∘ P₂.i₂ ∘ C₃.f₂
+      from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl
 
-compose-3-left
-    : {c₁ : Cospan A B}
-      {c₂ : Cospan B C}
-      {c₃ : Cospan C D}
-    → Same (compose (compose c₁ c₂) c₃) (compose-3 c₁ c₂ c₃)
-compose-3-left {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
+compose-3-left : compose (compose f g) h ≈ compose-3 f g h
+compose-3-left {f = f} {g = g} {h = h} = record
     { ≅N = up-to-iso P₄′ P₄
-    ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl
-    ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module C₃ = Cospan c₃
+    module C₁ = Cospan f
+    module C₂ = Cospan g
+    module C₃ = Cospan h
+    P₁ : Pushout C₁.f₂ C₂.f₁
     P₁ = pushout C₁.f₂ C₂.f₁
+    P₂ : Pushout C₂.f₂ C₃.f₁
     P₂ = pushout C₂.f₂ C₃.f₁
     module P₁ = Pushout P₁
     module P₂ = Pushout P₂
+    P₃ : Pushout P₁.i₂ P₂.i₁
     P₃ = pushout P₁.i₂ P₂.i₁
     module P₃ = Pushout P₃
+    P₄ P₄′ : Pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
     P₄ = glue-i₁ P₂ P₃
-    module P₄ = Pushout P₄
     P₄′ = pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
+    module P₄ = Pushout P₄
     module P₄′ = Pushout P₄′
+    ≅N : P₄′.Q ≅ P₄.Q
+    ≅N = up-to-iso P₄′ P₄
+    module ≅N = _≅_ ≅N
+    abstract
+      from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ P₁.i₁ ∘ C₁.f₁ 𝒞.≈ P₄.i₁ ∘ P₁.i₁ ∘ C₁.f₁
+      from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl
+      from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ C₃.f₂ 𝒞.≈ P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂
+      from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc
 
 compose-assoc
     : {c₁ : Cospan A B}
       {c₂ : Cospan B C}
       {c₃ : Cospan C D}
-    → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃)
-compose-assoc = same-trans compose-3-right (same-sym compose-3-left)
+    → compose c₁ (compose c₂ c₃) ≈ (compose (compose c₁ c₂) c₃)
+compose-assoc = ≈-trans compose-3-right (≈-sym compose-3-left)
 
 compose-sym-assoc
     : {c₁ : Cospan A B}
       {c₂ : Cospan B C}
       {c₃ : Cospan C D}
-    → Same (compose (compose c₁ c₂) c₃) (compose c₁ (compose c₂ c₃))
-compose-sym-assoc = same-trans compose-3-left (same-sym compose-3-right)
+    → compose (compose c₁ c₂) c₃ ≈ compose c₁ (compose c₂ c₃)
+compose-sym-assoc = ≈-trans compose-3-left (≈-sym compose-3-right)
 
 compose-equiv
     : {c₂ c₂′ : Cospan B C}
       {c₁ c₁′ : Cospan A B}
-    → Same c₂ c₂′
-    → Same c₁ c₁′
-    → Same (compose c₁ c₂) (compose c₁′ c₂′)
+    → c₂ ≈ c₂′
+    → c₁ ≈ c₁′
+    → compose c₁ c₂ ≈ compose c₁′ c₂′
 compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≈C₂ ≈C₁ = record
-    { ≅N = up-to-iso P P″
-    ; from∘f₁≈f₁′ = begin
-          ≅P.from ∘ P.i₁ ∘ C₁.f₁      ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₁) ∘ C₁.f₁    ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
-          (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁  ≈⟨ assoc ⟩
-          P′.i₁ ∘ ≈C₁.from ∘ C₁.f₁    ≈⟨ refl⟩∘⟨ ≈C₁.from∘f₁≈f₁′ ⟩
-          P′.i₁ ∘ C₁′.f₁              ∎
-    ; from∘f₂≈f₂′ = begin
-          ≅P.from ∘ P.i₂ ∘ C₂.f₂      ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₂) ∘ C₂.f₂    ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩
-          (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂  ≈⟨ assoc ⟩
-          P′.i₂ ∘ ≈C₂.from ∘ C₂.f₂    ≈⟨ refl⟩∘⟨ ≈C₂.from∘f₂≈f₂′ ⟩
-          P′.i₂ ∘ C₂′.f₂              ∎
+    { ≅N = ≅P
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     module C₁ = Cospan c₁
     module C₁′ = Cospan c₁′
     module C₂ = Cospan c₂
     module C₂′ = Cospan c₂′
+    P : Pushout C₁.f₂ C₂.f₁
     P = pushout C₁.f₂ C₂.f₁
+    P′ : Pushout C₁′.f₂ C₂′.f₁
     P′ = pushout C₁′.f₂ C₂′.f₁
-    module ≈C₁ = Same ≈C₁
-    module ≈C₂ = Same ≈C₂
+    module ≈C₁ = _≈_ ≈C₁
+    module ≈C₂ = _≈_ ≈C₂
     P′′ : Pushout (≈C₁.to ∘ C₁′.f₂) (≈C₂.to ∘ C₂′.f₁)
     P′′ = extend-i₂-iso (extend-i₁-iso P′ (≅.sym ≈C₁.≅N)) (≅.sym ≈C₂.≅N)
     P″ : Pushout C₁.f₂ C₂.f₁
     P″ =
         pushout-resp-≈
             P′′
-            (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂′))
-            (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁′))
+            (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂))
+            (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁))
     module P = Pushout P
     module P′ = Pushout P′
     ≅P : P.Q ≅ P′.Q
     ≅P = up-to-iso P P″
     module ≅P = _≅_ ≅P
     open HomReasoning
+    abstract
+      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ C₁.f₁ 𝒞.≈ P′.i₁ ∘ C₁′.f₁
+      from∘f₁≈f₁ = begin
+          ≅P.from ∘ P.i₁ ∘ C₁.f₁      ≈⟨ pullˡ P.universal∘i₁≈h₁ ⟩
+          (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁  ≈⟨ pullʳ ≈C₁.from∘f₁≈f₁ ⟩
+          P′.i₁ ∘ C₁′.f₁              ∎
+      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ C₂.f₂ 𝒞.≈ P′.i₂ ∘ C₂′.f₂
+      from∘f₂≈f₂ = begin
+          ≅P.from ∘ P.i₂ ∘ C₂.f₂      ≈⟨ pullˡ P.universal∘i₂≈h₂ ⟩
+          (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂  ≈⟨ pullʳ ≈C₂.from∘f₂≈f₂ ⟩
+          P′.i₂ ∘ C₂′.f₂              ∎
 
 Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e)
 Cospans = record
     { Obj = Obj
     ; _⇒_ = Cospan
-    ; _≈_ = Same
-    ; id = id-Cospan
+    ; _≈_ = _≈_
+    ; id = identity
     ; _∘_ = flip compose
     ; assoc = compose-assoc
     ; sym-assoc = compose-sym-assoc
     ; identityˡ = compose-idˡ
     ; identityʳ = compose-idʳ
     ; identity² = compose-id²
-    ; equiv = record
-        { refl = same-refl
-        ; sym = same-sym
-        ; trans = same-trans
-        }
+    ; equiv = ≈-equiv
     ; ∘-resp-≈ = compose-equiv
     }
diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda
index c0c62c7..7e63f81 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -18,15 +18,17 @@ module Category.Instance.DecoratedCospans
 module 𝒞 = FinitelyCocompleteCategory 𝒞
 module 𝒟 = SymmetricMonoidalCategory 𝒟
 
+import Categories.Category.Monoidal.Utilities as ⊗-Util
 import Category.Instance.Cospans 𝒞 as Cospans
 
 open import Categories.Category using (Category; _[_∘_])
 open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
 open import Categories.Diagram.Pushout using (Pushout)
 open import Categories.Diagram.Pushout.Properties 𝒞.U using (up-to-iso)
-open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Categories.Functor.Properties using ([_]-resp-≅; [_]-resp-square)
 open import Categories.Morphism.Reasoning using (switch-fromtoˡ; glueTrianglesˡ)
 open import Cospan.Decorated 𝒞 F using (DecoratedCospan)
+open import Relation.Binary using (IsEquivalence)
 open import Data.Product using (_,_)
 open import Function using (flip)
 open import Level using (_⊔_)
@@ -67,64 +69,80 @@ compose c₁ c₂ = record
 
 identity : DecoratedCospan A A
 identity = record
-    { cospan = Cospans.id-Cospan
+    { cospan = Cospans.identity
     ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ]
     }
 
-record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where
+record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where
 
-  module C₁ = DecoratedCospan C₁
-  module C₂ = DecoratedCospan C₂
+  private
+    module C₁ = DecoratedCospan C₁
+    module C₂ = DecoratedCospan C₂
 
   field
-    cospans-≈ : Cospans.Same C₁.cospan C₂.cospan
+    cospans-≈ : C₁.cospan Cospans.≈ C₂.cospan
 
-  open Cospans.Same cospans-≈ public
-  open 𝒟
-  open Morphism U using (_≅_)
+  open Cospans._≈_ cospans-≈ public
+  open Morphism 𝒟.U using (_≅_)
 
   field
-    same-deco : F₁ ≅N.from ∘ C₁.decoration ≈ C₂.decoration
+    same-deco : F₁ ≅N.from 𝒟.∘ C₁.decoration 𝒟.≈ C₂.decoration
 
   ≅F[N] : F₀ C₁.N ≅ F₀ C₂.N
   ≅F[N] = [ F′ ]-resp-≅ ≅N
 
-same-refl : {C : DecoratedCospan A B} → Same C C
-same-refl = record
-    { cospans-≈ = Cospans.same-refl
-    ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ
-    }
-  where
-    open 𝒟
-    open HomReasoning
+infix 4 _≈_
 
-same-sym : {C C′ : DecoratedCospan A B} → Same C C′ → Same C′ C
-same-sym C≅C′ = record
-    { cospans-≈ = Cospans.same-sym cospans-≈
-    ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco)
-    }
-  where
-    open Same C≅C′
-    open 𝒟.Equiv
-
-same-trans : {C C′ C″ : DecoratedCospan A B} → Same C C′ → Same C′ C″ → Same C C″
-same-trans C≈C′ C′≈C″ = record
-    { cospans-≈ = Cospans.same-trans C≈C′.cospans-≈ C′≈C″.cospans-≈
-    ; same-deco =
-          homomorphism ⟩∘⟨refl ○
-          glueTrianglesˡ 𝒟.U C′≈C″.same-deco C≈C′.same-deco
-    }
-  where
-    module C≈C′ = Same C≈C′
-    module C′≈C″ = Same C′≈C″
-    open 𝒟.HomReasoning
+module _ where
+
+  open 𝒟.HomReasoning
+  open 𝒟.Equiv
+  open 𝒟 using (identityˡ)
+
+  private
+    variable
+      f g h : DecoratedCospan A B
+
+  abstract
+
+    ≈-refl : f ≈ f
+    ≈-refl = record
+        { cospans-≈ = Cospans.≈-refl
+        ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ
+        }
+
+    ≈-sym : f ≈ g → g ≈ f
+    ≈-sym f≈g = record
+        { cospans-≈ = Cospans.≈-sym cospans-≈
+        ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco)
+        }
+      where
+        open _≈_ f≈g
+
+    ≈-trans : f ≈ g → g ≈ h → f ≈ h
+    ≈-trans f≈g g≈h = record
+        { cospans-≈ = Cospans.≈-trans f≈g.cospans-≈ g≈h.cospans-≈
+        ; same-deco =
+              homomorphism ⟩∘⟨refl ○
+              glueTrianglesˡ 𝒟.U g≈h.same-deco f≈g.same-deco
+        }
+      where
+        module f≈g = _≈_ f≈g
+        module g≈h = _≈_ g≈h
+
+  ≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
+  ≈-equiv = record
+      { refl = ≈-refl
+      ; sym = ≈-sym
+      ; trans = ≈-trans
+      }
 
 compose-assoc
     : {c₁ : DecoratedCospan A B}
       {c₂ : DecoratedCospan B C}
       {c₃ : DecoratedCospan C D}
-    → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃)
-compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
+    → compose c₁ (compose c₂ c₃) ≈ compose (compose c₁ c₂) c₃
+compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record
     { cospans-≈ = Cospans.compose-assoc
     ; same-deco = deco-assoc
     }
@@ -133,14 +151,19 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
     module C₂ = DecoratedCospan c₂
     module C₃ = DecoratedCospan c₃
     open 𝒞 using (+-assoc; pushout; [_,_]; _+₁_; _+_) renaming (_∘_ to _∘′_; id to id′)
+    p₁ : Pushout 𝒞.U C₁.f₂ C₂.f₁
     p₁ = pushout C₁.f₂ C₂.f₁
+    p₂ : Pushout 𝒞.U C₂.f₂ C₃.f₁
     p₂ = pushout C₂.f₂ C₃.f₁
     module P₁ = Pushout p₁
     module P₂ = Pushout p₂
+    p₃ : Pushout 𝒞.U P₁.i₂ P₂.i₁
     p₃ = pushout P₁.i₂ P₂.i₁
+    p₁₃ p₄ : Pushout 𝒞.U C₁.f₂ (P₂.i₁ ∘′ C₂.f₁)
     p₁₃ = glue-i₂ p₁ p₃
-    p₂₃ = glue-i₁ p₂ p₃
     p₄ = pushout C₁.f₂ (P₂.i₁ ∘′ C₂.f₁)
+    p₂₃ p₅ : Pushout 𝒞.U (P₁.i₂ ∘′ C₂.f₂) C₃.f₁
+    p₂₃ = glue-i₁ p₂ p₃
     p₅ = pushout (P₁.i₂ ∘′ C₂.f₂) C₃.f₁
     module P₃ = Pushout p₃
     module P₄ = Pushout p₄
@@ -151,36 +174,50 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
     module P₄≅P₁₃ = _≅_ (up-to-iso p₄ p₁₃)
     module P₅≅P₂₃ = _≅_ (up-to-iso p₅ p₂₃)
 
+    N M P Q R : 𝒞.Obj
     N = C₁.N
     M = C₂.N
     P = C₃.N
     Q = P₁.Q
     R = P₂.Q
-    φ = ⊗-homo.η
-    φ-commute = ⊗-homo.commute
-
-    a = C₁.f₂
-    b = C₂.f₁
-    c = C₂.f₂
-    d = C₂.f₁
 
+    f : N 𝒞.⇒ Q
     f = P₁.i₁
+
+    g : M 𝒞.⇒ Q
     g = P₁.i₂
+
+    h : M 𝒞.⇒ R
     h = P₂.i₁
+
+    i : P 𝒞.⇒ R
     i = P₂.i₂
 
+    j : Q 𝒞.⇒ P₃.Q
     j = P₃.i₁
+
+    k : R 𝒞.⇒ P₃.Q
     k = P₃.i₂
 
+    w : N 𝒞.⇒ P₄.Q
     w = P₄.i₁
+
+    x : R 𝒞.⇒ P₄.Q
     x = P₄.i₂
+
+    y : Q 𝒞.⇒ P₅.Q
     y = P₅.i₁
+
+    z : P 𝒞.⇒ P₅.Q
     z = P₅.i₂
 
+    l : P₂₃.Q 𝒞.⇒ P₅.Q
     l = P₅≅P₂₃.to
+
+    m : P₄.Q 𝒞.⇒ P₁₃.Q
     m = P₄≅P₁₃.from
 
-    module +-assoc = _≅_ +-assoc
+    module +-assoc {m} {n} {o} = _≅_ (+-assoc {m} {n} {o})
 
     module _ where
 
@@ -194,23 +231,19 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
       open 𝒞.HomReasoning
       open 𝒞.Equiv
 
-      copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from
+      copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) 𝒞.≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from
       copairings = begin
-          ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ])     ≈⟨ pushˡ assoc ⟩
-          l ∘ (m ∘ [ w , x ]) ∘ (id +₁ [ h , i ])       ≈⟨ refl⟩∘⟨ ∘[] ⟩∘⟨refl ⟩
-          l ∘ [ m ∘ w , m ∘ x ] ∘ (id +₁ [ h , i ])     ≈⟨ refl⟩∘⟨ []-cong₂ (P₄.universal∘i₁≈h₁) (P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩
-          l ∘ [ j ∘ f , k ] ∘ (id +₁ [ h , i ])         ≈⟨ pullˡ ∘[] ⟩
-          [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ])     ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩
-          [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ])         ≈⟨ []∘+₁ ⟩
-          [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ]        ≈⟨ []-cong₂ identityʳ (pullʳ ∘[]) ⟩
-          [ y ∘ f , l ∘ [ k ∘ h , k ∘ i ] ]             ≈⟨ []-congˡ (refl⟩∘⟨ []-congʳ P₃.commute) ⟨
-          [ y ∘ f , l ∘ [ j ∘ g , k ∘ i ] ]             ≈⟨ []-congˡ ∘[] ⟩
-          [ y ∘ f , [ l ∘ j ∘ g , l ∘ k ∘ i ] ]         ≈⟨ []-congˡ ([]-congˡ P₂₃.universal∘i₂≈h₂) ⟩
-          [ y ∘ f , [ l ∘ j ∘ g , z ] ]                 ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩
-          [ y ∘ f , [ y ∘ g , z ] ]                     ≈⟨ []∘assocˡ ⟨
-          [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from      ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨
-          [ y ∘ [ f ,  g ] , z ∘ id ] ∘ +-assoc.from    ≈⟨ pullˡ []∘+₁ ⟨
-          [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from  ∎
+          ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ])         ≈⟨ ∘[] ⟩∘⟨refl ⟩
+          [(l ∘ m) ∘ w , (l ∘ m) ∘ x ] ∘ (id +₁ [ h , i ])  ≈⟨ []-cong₂ (pullʳ P₄.universal∘i₁≈h₁) (pullʳ P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩
+          [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ])         ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩
+          [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ])             ≈⟨ []∘+₁ ⟩
+          [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ]            ≈⟨ []-cong₂ identityʳ ∘[] ⟩
+          [ y ∘ f , [ (l ∘ k) ∘ h , (l ∘ k) ∘ i ] ]         ≈⟨ []-congˡ ([]-cong₂ (pullʳ (sym P₃.commute)) (assoc ○ P₂₃.universal∘i₂≈h₂)) ⟩
+          [ y ∘ f , [ l ∘ j ∘ g , z ] ]                     ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩
+          [ y ∘ f , [ y ∘ g , z ] ]                         ≈⟨ []∘assocˡ ⟨
+          [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from          ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨
+          [ y ∘ [ f ,  g ] , z ∘ id ] ∘ +-assoc.from        ≈⟨ pullˡ []∘+₁ ⟨
+          [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from      ∎
 
     module _ where
 
@@ -219,153 +252,160 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
       open 𝒟 using (_⊗₀_; _⊗₁_; id; _∘_; _≈_; assoc; sym-assoc; identityʳ; ⊗; identityˡ; triangle; assoc-commute-to; assoc-commute-from)
       open 𝒟 using (_⇒_; unit)
 
-      α⇒ = 𝒟.associator.from
-      α⇐ = 𝒟.associator.to
-
-      λ⇒ = 𝒟.unitorˡ.from
-      λ⇐ = 𝒟.unitorˡ.to
-
-      ρ⇒ = 𝒟.unitorʳ.from
-      ρ⇐ = 𝒟.unitorʳ.to
-
-      module α≅ = 𝒟.associator
-      module λ≅ = 𝒟.unitorˡ
-      module ρ≅ = 𝒟.unitorʳ
+      open ⊗-Util 𝒟.monoidal using (module Shorthands)
+      open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
 
       open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐)
       open 𝒟.Equiv
 
+      +-α⇒ : {m n o : 𝒞.Obj} → m + (n + o) 𝒞.⇒ (m + n) + o
       +-α⇒ = +-assoc.from
+      +-α⇐ : {m n o : 𝒞.Obj} → (m + n) + o 𝒞.⇒ m + (n + o)
       +-α⇐ = +-assoc.to
 
-      s : unit ⇒ F₀ C₁.N
+      s : unit ⇒ F₀ N
       s = C₁.decoration
 
-      t : unit ⇒ F₀ C₂.N
+      t : unit ⇒ F₀ M
       t = C₂.decoration
 
-      u : unit ⇒ F₀ C₃.N
+      u : unit ⇒ F₀ P
       u = C₃.decoration
 
-      F-copairings : F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈ F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ (+-assoc.from)
-      F-copairings = begin
-          F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ])      ≈⟨ pushˡ homomorphism ⟨
-          F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F₁ (id′ +₁ [ h , i ])      ≈⟨ homomorphism ⟨
-          F₁ (((l ∘′ m) ∘′ [ w , x ]) ∘′ (id′ +₁ [ h , i ]))      ≈⟨ F-resp-≈ copairings ⟩
-          F₁ ([ y , z ] ∘′ ([ f , g ] +₁ id′) ∘′ +-assoc.from)     ≈⟨ homomorphism ⟩
-          F₁ [ y , z ] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from)  ≈⟨ refl⟩∘⟨ homomorphism ⟩
-          F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ +-assoc.from  ∎
-
-      coherences : φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈ F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐
-      coherences = begin
-          φ (N , M + P) ∘ id ⊗₁ φ (M , P)                         ≈⟨ insertʳ α≅.isoʳ ⟩
-          ((φ (N , M + P) ∘ id ⊗₁ φ (M , P)) ∘ α⇒) ∘ α⇐           ≈⟨ assoc ⟩∘⟨refl ⟩
-          (φ (N , M + P) ∘ id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐             ≈⟨ assoc ⟩
-          φ (N , M + P) ∘ (id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐             ≈⟨ extendʳ associativity ⟨
-          F₁ +-assoc.to ∘ (φ (N + M , P) ∘ φ (N , M) ⊗₁ id) ∘ α⇐  ≈⟨ refl⟩∘⟨ assoc ⟩
-          F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐    ∎
-
-      triangle-to : α⇒ ∘ ρ⇐ ⊗₁ id ≈ id ⊗₁ λ⇐
-      triangle-to = begin
-          α⇒ ∘ ρ⇐ ⊗₁ id                          ≈⟨ pullˡ identityˡ ⟨
-          id ∘ α⇒ ∘ ρ⇐ ⊗₁ id                     ≈⟨ ⊗.identity ⟩∘⟨refl ⟨
-          id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id               ≈⟨ refl⟩⊗⟨ λ≅.isoˡ ⟩∘⟨refl ⟨
-          id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id        ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨
-          (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩
-          id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id    ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩
-          id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id         ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨
-          id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id)      ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩
-          id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id             ≈⟨ refl⟩∘⟨ ρ≅.isoʳ ⟩⊗⟨refl ⟩
-          id ⊗₁ λ⇐ ∘ id ⊗₁ id                    ≈⟨ refl⟩∘⟨ ⊗.identity ⟩
-          id ⊗₁ λ⇐ ∘ id                          ≈⟨ identityʳ ⟩
-          id ⊗₁ λ⇐                               ∎
-
-      unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐
-      unitors = begin
-          s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐               ≈⟨ pushˡ split₂ʳ ⟩
-          s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐           ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨
-          s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐           ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨
-          s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ extendʳ assoc-commute-from ⟨
-          α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐    ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨
-          α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐          ∎
-
-      F-l∘m = F₁ (l ∘′ m)
+      F[l∘m] : F₀ P₄.Q ⇒ F₀ P₅.Q
+      F[l∘m] = F₁ (l ∘′ m)
+
+      F[w,x] : F₀ (N + R) ⇒ F₀ P₄.Q
       F[w,x] = F₁ [ w , x ]
+
+      F[h,i] : F₀ (M + P) ⇒ F₀ R
       F[h,i] = F₁ [ h , i ]
+
+      F[y,z] : F₀ (Q + P) ⇒ F₀ P₅.Q
       F[y,z] = F₁ [ y , z ]
+
+      F[f,g] : F₀ (N + M) ⇒ F₀ Q
       F[f,g] = F₁ [ f , g ]
-      F-[f,g]+id = F₁ ([ f , g ] +₁ id′)
-      F-id+[h,i] = F₁ (id′ +₁ [ h , i ])
-      φ-N,R = φ (N , R)
-      φ-M,P = φ (M , P)
-      φ-N+M,P = φ (N + M , P)
-      φ-N+M = φ (N , M)
-      φ-N,M+P = φ (N , M + P)
-      φ-N,M = φ (N , M)
-      φ-Q,P = φ (Q , P)
+
+      F[[f,g]+id] : F₀ ((N + M) + P) ⇒ F₀ (Q + P)
+      F[[f,g]+id] = F₁ ([ f , g ] +₁ id′)
+
+      F[id+[h,i]] : F₀ (N + (M + P)) ⇒ F₀ (N + R)
+      F[id+[h,i]] = F₁ (id′ +₁ [ h , i ])
+
+      φ[N,R] : F₀ N ⊗₀ F₀ R 𝒟.⇒ F₀ (N + R)
+      φ[N,R] = ⊗-homo.η (N , R)
+
+      φ[M,P] : F₀ M ⊗₀ F₀ P 𝒟.⇒ F₀ (M + P)
+      φ[M,P] = ⊗-homo.η (M , P)
+
+      φ[N+M,P] : F₀ (N + M) ⊗₀ F₀ P 𝒟.⇒ F₀ ((N + M) + P)
+      φ[N+M,P] = ⊗-homo.η (N + M , P)
+
+      φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M)
+      φ[N,M] = ⊗-homo.η (N , M)
+
+      φ[N,M+P] : F₀ N ⊗₀ F₀ (M + P) 𝒟.⇒ F₀ (N + (M + P))
+      φ[N,M+P] = ⊗-homo.η (N , M + P)
+
+      φ[Q,P] : F₀ Q ⊗₀ F₀ P 𝒟.⇒ F₀ (Q + P)
+      φ[Q,P] = ⊗-homo.η (Q , P)
+
+      s⊗[t⊗u] : unit 𝒟.⇒ F₀ N ⊗₀ (F₀ M ⊗₀ F₀ P)
       s⊗[t⊗u] = s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐
+
+      [s⊗t]⊗u : unit 𝒟.⇒ (F₀ N ⊗₀ F₀ M) ⊗₀ F₀ P
       [s⊗t]⊗u = (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐
 
-      deco-assoc
-          : F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐
-          ≈ F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐
-      deco-assoc = begin
-          F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐                           ≈⟨ pullˡ refl ⟩
-          (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐                         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩
-          (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ-M,P ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩
-          (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc    ⟩
-          (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨ refl ⟨
-          (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐       ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , [ h  , i ])) ⟩
-          (F-l∘m ∘ F[w,x]) ∘ F-id+[h,i] ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐           ≈⟨ pullˡ assoc ⟩
-          (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
-          (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ id ⊗₁ φ-M,P ∘ s⊗[t⊗u]                             ≈⟨ refl⟩∘⟨ sym-assoc ⟩
-          (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ (φ-N,M+P ∘ id ⊗₁ φ-M,P) ∘ s⊗[t⊗u]                           ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩
-          (F[y,z] ∘ F-[f,g]+id ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u     ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩
-          ((F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u   ≈⟨ assoc ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u     ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨
-          (F[y,z] ∘ F-[f,g]+id) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u     ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ F₁ id′ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ id ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                    ≈⟨ refl⟩∘⟨ identityˡ ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                         ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ ((φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                       ≈⟨ refl⟩∘⟨ cancelInner α≅.isoˡ ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ [s⊗t]⊗u                                   ≈⟨ refl⟩∘⟨ assoc ⟩
-          (F[y,z] ∘ F-[f,g]+id) ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u                                     ≈⟨ assoc ⟩
-          F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u                                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨
-          F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐                             ≈⟨ refl⟩∘⟨ extendʳ (φ-commute ([ f  , g ] , id′)) ⟨
-          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
+      abstract
+        F-copairings : F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]] 𝒟.≈ F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-assoc.from
+        F-copairings = begin
+            F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]                     ≈⟨ pushˡ homomorphism ⟨
+            F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F[id+[h,i]]          ≈⟨ [ F′ ]-resp-square copairings ⟩
+            F[y,z] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from)  ≈⟨ refl⟩∘⟨ homomorphism ⟩
+            F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-assoc.from            ∎
+
+        coherences : φ[N,M+P] ∘ id ⊗₁ φ[M,P] 𝒟.≈ F₁ +-assoc.to ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐
+        coherences = begin
+            φ[N,M+P] ∘ id ⊗₁ φ[M,P]                         ≈⟨ refl⟩∘⟨ insertʳ 𝒟.associator.isoʳ ⟩
+            φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ α⇒) ∘ α⇐             ≈⟨ extendʳ associativity ⟨
+            F₁ +-assoc.to ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ α⇐  ≈⟨ refl⟩∘⟨ assoc ⟩
+            F₁ +-assoc.to ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐    ∎
+
+        triangle-to : α⇒ {𝒟.unit} {𝒟.unit} {𝒟.unit} ∘ ρ⇐ ⊗₁ id 𝒟.≈ id ⊗₁ λ⇐
+        triangle-to = begin
+            α⇒ ∘ ρ⇐ ⊗₁ id                          ≈⟨ pullˡ identityˡ ⟨
+            id ∘ α⇒ ∘ ρ⇐ ⊗₁ id                     ≈⟨ ⊗.identity ⟩∘⟨refl ⟨
+            id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id               ≈⟨ refl⟩⊗⟨ 𝒟.unitorˡ.isoˡ ⟩∘⟨refl ⟨
+            id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id        ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨
+            (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩
+            id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id    ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩
+            id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id         ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨
+            id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id)      ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩
+            id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id             ≈⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟩⊗⟨refl ⟩
+            id ⊗₁ λ⇐ ∘ id ⊗₁ id                    ≈⟨ refl⟩∘⟨ ⊗.identity ⟩
+            id ⊗₁ λ⇐ ∘ id                          ≈⟨ identityʳ ⟩
+            id ⊗₁ λ⇐                               ∎
+
+        unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ 𝒟.≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐
+        unitors = begin
+            s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐               ≈⟨ pushˡ split₂ʳ ⟩
+            s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐           ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨
+            s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐           ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨
+            s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ extendʳ assoc-commute-from ⟨
+            α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐    ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨
+            α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐          ∎
+
+        deco-assoc
+            : F[l∘m] ∘ (F[w,x] ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐)
+            𝒟.≈ F[y,z] ∘ φ[Q,P] ∘ (F[f,g] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐
+        deco-assoc = begin
+            F[l∘m] ∘ F[w,x] ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐                          ≈⟨ pullˡ refl ⟩
+            (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩
+            (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩
+            (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
+            (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
+            (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐      ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (id′ , [ h  , i ])) ⟩
+            (F[l∘m] ∘ F[w,x]) ∘ F[id+[h,i]] ∘ φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐         ≈⟨ pullˡ assoc ⟩
+            (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
+            (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ φ[N,M+P] ∘ id ⊗₁ φ[M,P] ∘ s⊗[t⊗u]                           ≈⟨ refl⟩∘⟨ sym-assoc ⟩
+            (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ (φ[N,M+P] ∘ id ⊗₁ φ[M,P]) ∘ s⊗[t⊗u]                         ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩
+            (F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u    ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩
+            ((F[y,z] ∘ F[[f,g]+id]) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u  ≈⟨ assoc ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u    ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨
+            (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u    ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ id′ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u               ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ id ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                   ≈⟨ refl⟩∘⟨ identityˡ ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                        ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ ((φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u                      ≈⟨ refl⟩∘⟨ cancelInner 𝒟.associator.isoˡ ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ [s⊗t]⊗u                                  ≈⟨ refl⟩∘⟨ assoc ⟩
+            (F[y,z] ∘ F[[f,g]+id]) ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ [s⊗t]⊗u                                    ≈⟨ assoc ⟩
+            F[y,z] ∘ F[[f,g]+id] ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ [s⊗t]⊗u                                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨
+            F[y,z] ∘ F[[f,g]+id] ∘ φ[N+M,P] ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐                            ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute ([ f  , g ] , id′)) ⟨
+            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} → compose identity C ≈ C
 compose-idʳ {A} {_} {C} = record
     { cospans-≈ = Cospans.compose-idʳ
     ; same-deco = deco-id
     }
   where
-
     open DecoratedCospan C
-
-    open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡)
-
+    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
@@ -374,17 +414,13 @@ compose-idʳ {A} {_} {C} = record
           ; ∘[] ; []∘+₁ ; 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 : ((≅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 ⟩
@@ -394,62 +430,54 @@ compose-idʳ {A} {_} {C} = record
         [ 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ʳ
+          ; 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 ⊗-Util 𝒟.monoidal using (module Shorthands)
+      open Shorthands using (λ⇒; λ⇐; ρ⇐)
+      open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐)
       open 𝒟.Equiv
-
       s : unit ⇒ F₀ N
       s = decoration
-
-      cohere-s : φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈ F₁ ⊥+A≅A.to ∘ s
-      cohere-s = begin
-          φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐                                               ≈⟨ identityˡ ⟨
-          id ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐                                          ≈⟨ F-identity ⟩∘⟨refl ⟨
-          F₁ id′ ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐                                      ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨
-          F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐                 ≈⟨ pushˡ homomorphism ⟩
-          F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
-          F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε ⊗₁ id) ∘ (id ⊗₁ s) ∘ ρ⇐    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
-          F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ (⊥ , N) ∘ (ε ⊗₁ 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₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s
-      deco-id = begin
-          F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐             ≈⟨ pushˡ homomorphism ⟨
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ id) ∘ (ε ⊗₁ s) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , id′)) ⟩
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐    ≈⟨ pushˡ homomorphism ⟨
-          F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ (⊥ , N) ∘ (ε ⊗₁ 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
+      φ[⊥,N] : F₀ ⊥ ⊗₀ F₀ N ⇒ F₀ (⊥ + N)
+      φ[⊥,N] = ⊗-homo.η (⊥ , N)
+      φ[A,N] : F₀ A ⊗₀ F₀ N ⇒ F₀ (A + N)
+      φ[A,N] = ⊗-homo.η (A , N)
+      abstract
+        cohere-s : φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ 𝒟.≈ F₁ ⊥+A≅A.to ∘ s
+        cohere-s = begin
+            φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐                                            ≈⟨ identityˡ ⟨
+            id ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐                                       ≈⟨ F-identity ⟩∘⟨refl ⟨
+            F₁ id′ ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐                                   ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨
+            F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐              ≈⟨ pushˡ homomorphism ⟩
+            F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+            F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ[⊥,N] ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
+            F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ[⊥,N] ∘ ε ⊗₁ 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ˡ 𝒟.unitorˡ.isoʳ ⟩
+            F₁ ⊥+A≅A.to ∘ s                                                 ∎
+        deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ 𝒟.≈ s
+        deco-id = begin
+            F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐             ≈⟨ pushˡ homomorphism ⟨
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ⊗₁ id) ∘ (ε ⊗₁ s) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (¡ , id′)) ⟩
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ[⊥,N] ∘ (ε ⊗₁ s) ∘ ρ⇐    ≈⟨ pushˡ homomorphism ⟨
+            F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ[⊥,N] ∘ (ε ⊗₁ 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} → compose C identity ≈ C
 compose-idˡ {_} {B} {C} = record
     { cospans-≈ = Cospans.compose-idˡ
     ; same-deco = deco-id
@@ -497,7 +525,7 @@ compose-idˡ {_} {B} {C} = record
       open ⇒-Reasoning U
       open HomReasoning
 
-      copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to ≈ id
+      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 ⟩
@@ -510,11 +538,12 @@ compose-idˡ {_} {B} {C} = record
 
     module _ where
 
+      open 𝒞 using (_+_)
       open 𝒟
         using
           ( id ; _∘_ ; _≈_ ; _⇒_ ; U
           ; assoc ; sym-assoc; identityˡ
-          ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ
+          ; monoidal ; _⊗₀_; _⊗₁_ ; unit ; unitorˡ ; unitorʳ
           ; unitorʳ-commute-to
           ; module Equiv
           )
@@ -523,129 +552,146 @@ compose-idˡ {_} {B} {C} = record
       open ⊗-Reasoning monoidal
       open ⇒-Reasoning U
 
-      φ = ⊗-homo.η
-      φ-commute = ⊗-homo.commute
+      φ[N,⊥] : F₀ N ⊗₀ F₀ ⊥ 𝒟.⇒ F₀ (N + ⊥)
+      φ[N,⊥] = ⊗-homo.η (N , ⊥)
 
-      module ρ≅ = unitorʳ
-      ρ⇒ = ρ≅.from
-      ρ⇐ = ρ≅.to
+      φ[N,B] : F₀ N ⊗₀ F₀ B 𝒟.⇒ F₀ (N + B)
+      φ[N,B] = ⊗-homo.η (N , B)
 
       s : unit ⇒ F₀ N
       s = decoration
 
-      cohere-s : φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈ F₁ A+⊥≅A.to ∘ s
-      cohere-s = begin
-          φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐                                               ≈⟨ identityˡ ⟨
-          id ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐                                          ≈⟨ F-identity ⟩∘⟨refl ⟨
-          F₁ id′ ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐                                      ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨
-          F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐                 ≈⟨ pushˡ homomorphism ⟩
-          F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
-          F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (id ⊗₁ ε) ∘ (s ⊗₁ id) ∘ ρ⇐    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
-          F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ (N , ⊥) ∘ (id ⊗₁ ε)) ∘ (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₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s
-      deco-id = begin
-          F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐             ≈⟨ pushˡ homomorphism ⟨
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (id ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε) ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (F₁ id′ ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , ¡)) ⟩
-          F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐    ≈⟨ pushˡ homomorphism ⟨
-          F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ (N , ⊥) ∘ (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² : Same {A} (compose identity identity) identity
+      open ⊗-Util 𝒟.monoidal using (module Shorthands)
+      open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
+
+      abstract
+        cohere-s : φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ 𝒟.≈ F₁ A+⊥≅A.to ∘ s
+        cohere-s = begin
+            φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐                                            ≈⟨ identityˡ ⟨
+            id ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐                                       ≈⟨ F-identity ⟩∘⟨refl ⟨
+            F₁ id′ ∘ φ[N,⊥] ∘ (s ⊗₁ ε) ∘ ρ⇐                                 ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨
+            F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐              ≈⟨ pushˡ homomorphism ⟩
+            F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
+            F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ[N,⊥] ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
+            F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ[N,⊥] ∘ id ⊗₁ ε) ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryʳ ⟩
+            F₁ A+⊥≅A.to ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐                                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-to ⟨
+            F₁ A+⊥≅A.to ∘ ρ⇒ ∘ ρ⇐ ∘ s                                       ≈⟨ refl⟩∘⟨ cancelˡ unitorʳ.isoʳ ⟩
+            F₁ A+⊥≅A.to ∘ s                                                 ∎
+
+        deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ 𝒟.≈ s
+        deco-id = begin
+            F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐         ≈⟨ pushˡ homomorphism ⟨
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐         ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ F₁ id′ ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (id′ , ¡)) ⟩
+            F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐  ≈⟨ pushˡ homomorphism ⟨
+            F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ[N,⊥] ∘ 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² : compose identity identity ≈ identity {A}
 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₂′)
+    → c₂ ≈ c₂′
+    → c₁ ≈ c₁′
+    → 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₁ = _≈_ ≅C₁
+    module ≅C₂ = _≈_ ≅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₁
+    module ≅C₂∘C₁ = Cospans._≈_ ≅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 M N′ M′ : 𝒞.Obj
     N = C₁.N
     M = C₂.N
     N′ = C₁′.N
     M′ = C₂′.N
 
-    φ = ⊗-homo.η
-    φ-commute = ⊗-homo.commute
+    s : 𝒟.unit 𝒟.⇒ F₀ N
+    s = C₁.decoration
 
+    t : 𝒟.unit 𝒟.⇒ F₀ M
+    t = C₂.decoration
+
+    s′ : 𝒟.unit 𝒟.⇒ F₀ N′
+    s′ = C₁′.decoration
+
+    t′ : 𝒟.unit 𝒟.⇒ F₀ M′
+    t′ = C₂′.decoration
+
+    Q⇒ : ≅C₂∘C₁.C.N 𝒞.⇒ ≅C₂∘C₁.D.N
     Q⇒ = ≅C₂∘C₁.≅N.from
+
+    N⇒ : ≅C₁.C.N 𝒞.⇒ ≅C₁.D.N
     N⇒ = ≅C₁.≅N.from
+
+    M⇒ : ≅C₂.C.N 𝒞.⇒ ≅C₂.D.N
     M⇒ = ≅C₂.≅N.from
 
     module _ where
 
-      ρ⇒ = 𝒟.unitorʳ.from
-      ρ⇐ = 𝒟.unitorʳ.to
+      open ⊗-Util 𝒟.monoidal using (module Shorthands)
+      open Shorthands using (ρ⇒; ρ⇐)
 
-      open 𝒞 using ([_,_]; ∘[]; _+₁_; []∘+₁) renaming (_∘_ to _∘′_)
+      open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁) renaming (_∘_ to _∘′_)
       open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian
           using ()
           renaming (⟨⟩-cong₂ to []-cong₂)
 
       open 𝒟
 
+      φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M)
+      φ[N,M] = ⊗-homo.η (N , M)
+
+      φ[N′,M′] : F₀ N′ ⊗₀ F₀ M′ 𝒟.⇒ F₀ (N′ + M′)
+      φ[N′,M′] = ⊗-homo.η (N′ , M′)
+
       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′ ∘ ρ⇐                    ∎
+      abstract
+        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ʳ (⊗-homo.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′ ∘ ρ⇐                    ∎
 
 DecoratedCospans : Category o (o ⊔ ℓ ⊔ ℓ′) (ℓ ⊔ e ⊔ e′)
 DecoratedCospans = record
     { Obj = 𝒞.Obj
     ; _⇒_ = DecoratedCospan
-    ; _≈_ = Same
+    ; _≈_ = _≈_
     ; id = identity
     ; _∘_ = flip compose
     ; assoc = compose-assoc
-    ; sym-assoc = same-sym (compose-assoc)
+    ; sym-assoc = ≈-sym compose-assoc
     ; identityˡ = compose-idˡ
     ; identityʳ = compose-idʳ
     ; identity² = compose-id²
-    ; equiv = record
-        { refl = same-refl
-        ; sym = same-sym
-        ; trans = same-trans
-        }
+    ; equiv = ≈-equiv
     ; ∘-resp-≈ = compose-equiv
     }