Switch decoration functor from strong to lax

1 files changed, 65 insertions, 65 deletions

diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda
index 92a1de9..3f9b6ee 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -1,18 +1,18 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Functor.Monoidal.Symmetric using (module Strong)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
 
-open Strong using (SymmetricMonoidalFunctor)
+open Lax using (SymmetricMonoidalFunctor)
 open FinitelyCocompleteCategory
   using ()
   renaming (symmetricMonoidalCategory to smc)
 
 module Category.Instance.DecoratedCospans
-    {o ℓ e}
+    {o o′ ℓ ℓ′ e e′}
     (𝒞 : FinitelyCocompleteCategory o ℓ e)
-    {𝒟 : SymmetricMonoidalCategory o ℓ e}
+    {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
     (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
 
 module 𝒞 = FinitelyCocompleteCategory 𝒞
@@ -60,17 +60,17 @@ compose c₁ c₂ = record
     module p = 𝒞.pushout C₁.f₂ C₂.f₁
     open p using (i₁; i₂)
     φ : F₀ C₁.N ⊗₀ F₀ C₂.N ⇒ F₀ (C₁.N + C₂.N)
-    φ = ⊗-homo.⇒.η (C₁.N , C₂.N)
+    φ = ⊗-homo.η (C₁.N , C₂.N)
     s⊗t : unit ⇒ F₀ C₁.N ⊗₀ F₀ C₂.N
     s⊗t = C₁.decoration ⊗₁ C₂.decoration ∘ unitorʳ.to
 
 identity : DecoratedCospan A A
 identity = record
     { cospan = Cospans.identity
-    ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε.from ]
+    ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ]
     }
 
-record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e) where
+record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where
 
   module C₁ = DecoratedCospan C₁
   module C₂ = DecoratedCospan C₂
@@ -155,8 +155,8 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
     P = C₃.N
     Q = P₁.Q
     R = P₂.Q
-    φ = ⊗-homo.⇒.η
-    φ-commute = ⊗-homo.⇒.commute
+    φ = ⊗-homo.η
+    φ-commute = ⊗-homo.commute
 
     a = C₁.f₂
     b = C₂.f₁
@@ -406,8 +406,8 @@ compose-idʳ {A} {_} {C} = record
       open ⊗-Reasoning monoidal
       open ⇒-Reasoning U
 
-      φ = ⊗-homo.⇒.η
-      φ-commute = ⊗-homo.⇒.commute
+      φ = ⊗-homo.η
+      φ-commute = ⊗-homo.commute
 
       module λ≅ = unitorˡ
       λ⇒ = λ≅.from
@@ -420,33 +420,33 @@ compose-idʳ {A} {_} {C} = record
       s : unit ⇒ F₀ N
       s = decoration
 
-      cohere-s : φ (⊥ , N) ∘ (ε.from ⊗₁ s) ∘ ρ⇐ ≈ F₁ ⊥+A≅A.to ∘ s
+      cohere-s : φ (⊥ , N) ∘ (ε ⊗₁ 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
+          φ (⊥ , 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₁ ¡ ∘ ε.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                                                                               ∎
+          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
 compose-idˡ {_} {B} {C} = record
@@ -522,8 +522,8 @@ compose-idˡ {_} {B} {C} = record
       open ⊗-Reasoning monoidal
       open ⇒-Reasoning U
 
-      φ = ⊗-homo.⇒.η
-      φ-commute = ⊗-homo.⇒.commute
+      φ = ⊗-homo.η
+      φ-commute = ⊗-homo.commute
 
       module ρ≅ = unitorʳ
       ρ⇒ = ρ≅.from
@@ -532,32 +532,32 @@ compose-idˡ {_} {B} {C} = record
       s : unit ⇒ F₀ N
       s = decoration
 
-      cohere-s : φ (N , ⊥) ∘ (s ⊗₁ ε.from) ∘ ρ⇐ ≈ F₁ A+⊥≅A.to ∘ s
+      cohere-s : φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈ 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
+          φ (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₁ ¡ ∘ ε.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                                                                               ∎
+          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
 compose-id² = compose-idˡ
@@ -595,8 +595,8 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re
     N′ = C₁′.N
     M′ = C₂′.N
 
-    φ = ⊗-homo.⇒.η
-    φ-commute = ⊗-homo.⇒.commute
+    φ = ⊗-homo.η
+    φ-commute = ⊗-homo.commute
 
     Q⇒ = ≅C₂∘C₁.≅N.from
     N⇒ = ≅C₁.≅N.from
@@ -629,7 +629,7 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re
           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 : Category o (o ⊔ ℓ ⊔ ℓ′) (ℓ ⊔ e ⊔ e′)
 Cospans = record
     { Obj = 𝒞.Obj
     ; _⇒_ = DecoratedCospan