Category of decorated cospans is symmetric monoidal

4 files changed, 673 insertions, 1 deletions

diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda
index b7664dc..03cca1f 100644
--- a/Functor/Instance/Cospan/Stack.agda
+++ b/Functor/Instance/Cospan/Stack.agda
@@ -13,7 +13,7 @@ open import Categories.Category.Core using (Category)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same; id-Cospan; compose)
 open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using () renaming (_×_ to _×′_)
-open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC)
+open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC)
 open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂)
 open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout)
 open import Level using (Level; _⊔_; suc)
diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda
new file mode 100644
index 0000000..e87f20c
--- /dev/null
+++ b/Functor/Instance/Decorate.agda
@@ -0,0 +1,168 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Data.Product.Base using (_,_)
+
+open Lax using (SymmetricMonoidalFunctor)
+open FinitelyCocompleteCategory
+  using ()
+  renaming (symmetricMonoidalCategory to smc)
+
+module Functor.Instance.Decorate
+    {o o′ ℓ ℓ′ e e′}
+    (𝒞 : FinitelyCocompleteCategory o ℓ e)
+    {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
+    (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Diagram.Pushout as DiagramPushout
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Function.Base using () renaming (id to idf)
+open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same)
+open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans)
+open import Functor.Instance.Cospan.Stack using (⊗)
+open import Functor.Instance.DecoratedCospan.Stack using () renaming (⊗ to ⊗′)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+module 𝒟 = SymmetricMonoidalCategory 𝒟
+module F = SymmetricMonoidalFunctor F
+module Cospans = Category Cospans
+module DecoratedCospans = Category DecoratedCospans
+module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian
+
+-- For every cospan there exists a free decorated cospan
+-- i.e. the original cospan with the empty decoration
+
+private
+  variable
+    A A′ B B′ C C′ D : 𝒞.Obj
+    f : Cospans [ A , B ]
+    g : Cospans [ C , D ]
+
+decorate : Cospans [ A , B ] → DecoratedCospans [ A , B ]
+decorate f = record
+    { cospan = f
+    ; decoration = F₁ ¡ ∘ ε
+    }
+  where
+    open 𝒞 using (¡)
+    open 𝒟 using (_∘_)
+    open F using (ε; F₁)
+
+identity : DecoratedCospans [ decorate (Cospans.id {A}) ≈ DecoratedCospans.id ]
+identity = record
+    { cospans-≈ = Cospans.Equiv.refl
+    ; same-deco = elimˡ F.identity
+    }
+  where
+    open ⇒-Reasoning 𝒟.U
+
+homomorphism : DecoratedCospans [ decorate (Cospans [ g ∘ f ]) ≈ DecoratedCospans [ decorate g ∘ decorate f ] ]
+homomorphism {B} {C} {g} {A} {f} = record
+    { cospans-≈ = Cospans.Equiv.refl
+    ; same-deco = same-deco
+    }
+  where
+
+    open Cospan f using (N; f₂)
+    open Cospan g using () renaming (N to M; f₁ to g₁)
+
+    open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-)
+    open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+    open Category U
+    open Equiv
+    open ⇒-Reasoning U
+    open ⊗-Reasoning monoidal
+    open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+    open F using (F₁; ε)
+    open Shorthands monoidal
+
+    open DiagramPushout 𝒞.U using (Pushout)
+    open Pushout (pushout f₂ g₁) using (i₁; i₂)
+    open mc𝒞 using (unitorˡ)
+    open unitorˡ using () renaming (to to λ⇐′)
+
+    same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ F.ε ≈ F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐
+    same-deco = begin
+        F₁ 𝒞.id ∘ F₁ ¡ ∘ ε                                                  ≈⟨ elimˡ F.identity ⟩
+        F₁ ¡ ∘ ε                                                            ≈⟨ F.F-resp-≈ (¡-unique _) ⟩∘⟨refl ⟩
+        F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε                            ≈⟨ refl⟩∘⟨ introʳ λ-.isoʳ ⟩
+        F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩
+        F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐                  ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨
+        F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐            ≈⟨ pushˡ F.homomorphism ⟩
+        F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐           ≈⟨ push-center (sym F.homomorphism) ⟩
+        F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨
+        F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩
+        F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐             ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , ¡)) ⟨
+        F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩
+        F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐         ∎
+
+F-resp-≈ : Cospans [ f ≈ g ] → DecoratedCospans [ decorate f ≈ decorate g ]
+F-resp-≈ f≈g = record
+    { cospans-≈ = f≈g
+    ; same-deco = pullˡ (sym F.homomorphism) ○ sym (F.F-resp-≈ (¡-unique _)) ⟩∘⟨refl
+    }
+  where
+    open ⇒-Reasoning 𝒟.U
+    open 𝒟.Equiv
+    open 𝒟.HomReasoning
+    open 𝒞 using (¡-unique)
+
+Decorate : Functor Cospans DecoratedCospans
+Decorate = record
+    { F₀ = idf
+    ; F₁ = decorate
+    ; identity = identity
+    ; homomorphism = homomorphism
+    ; F-resp-≈ = F-resp-≈
+    }
+
+module ⊗ = Functor (⊗ 𝒞)
+module ⊗′ = Functor (⊗′ 𝒞 F)
+open 𝒞 using (_+₁_)
+
+Decorate-resp-⊗ : DecoratedCospans [ decorate (⊗.₁ (f , g)) ≈ ⊗′.₁ (decorate f , decorate g) ]
+Decorate-resp-⊗ {f = f} {g = g} = record
+    { cospans-≈ = Cospans.Equiv.refl
+    ; same-deco = same-deco
+    }
+  where
+
+    open Cospan f using (N)
+    open Cospan g using () renaming (N to M)
+
+    open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-)
+    open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+    open Category U
+    open Equiv
+    open ⇒-Reasoning U
+    open ⊗-Reasoning monoidal
+    open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+    open F using (F₁; ε)
+    open Shorthands monoidal
+    open mc𝒞 using (unitorˡ)
+    open unitorˡ using () renaming (to to λ⇐′)
+
+    same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐
+    same-deco = begin
+        F₁ 𝒞.id ∘ F₁ ¡ ∘ ε                                ≈⟨ elimˡ F.identity ⟩
+        F₁ ¡ ∘ ε                                          ≈⟨ F.F-resp-≈ (¡-unique _) ⟩∘⟨refl ⟩
+        F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε                           ≈⟨ refl⟩∘⟨ introʳ λ-.isoʳ ⟩
+        F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩
+        F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨
+        F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐           ≈⟨ pushˡ F.homomorphism ⟩
+        F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐          ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨
+        F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩
+        F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐             ≈⟨ extendʳ (φ-commute (¡ , ¡)) ⟨
+        φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐            ≈⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩
+        φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐         ∎
+
diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda
new file mode 100644
index 0000000..4595a8f
--- /dev/null
+++ b/Functor/Instance/DecoratedCospan/Embed.agda
@@ -0,0 +1,275 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+open Lax using (SymmetricMonoidalFunctor)
+open FinitelyCocompleteCategory
+  using ()
+  renaming (symmetricMonoidalCategory to smc)
+
+module Functor.Instance.DecoratedCospan.Embed
+    {o o′ ℓ ℓ′ e e′}
+    (𝒞 : FinitelyCocompleteCategory o ℓ e)
+    {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
+    (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Diagram.Pushout.Properties as PushoutProperties
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Category.Diagram.Pushout as Pushout′
+import Functor.Instance.Cospan.Embed 𝒞 as Embed
+
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
+open import Categories.Category.Monoidal.Properties using (coherence-inv₃)
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Category.Instance.Cospans 𝒞 using (Cospans)
+open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans)
+
+import Categories.Diagram.Pushout as DiagramPushout
+import Categories.Diagram.Pushout.Properties as PushoutProperties
+import Categories.Morphism as Morphism
+
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Functor using (Functor; _∘F_)
+open import Data.Product.Base using (_,_)
+open import Function.Base using () renaming (id to idf)
+open import Functor.Instance.DecoratedCospan.Stack using (⊗)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+module 𝒟 = SymmetricMonoidalCategory 𝒟
+module F = SymmetricMonoidalFunctor F
+module Cospans = Category Cospans
+module DecoratedCospans = Category DecoratedCospans
+module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian
+
+open import Functor.Instance.Decorate 𝒞 F using (Decorate; Decorate-resp-⊗)
+
+private
+  variable
+    A B C D E H : 𝒞.Obj
+    f : 𝒞.U [ A , B ]
+    g : 𝒞.U [ C , D ]
+    h : 𝒞.U [ E , H ]
+
+L : Functor 𝒞.U DecoratedCospans
+L = Decorate ∘F Embed.L
+
+R : Functor 𝒞.op DecoratedCospans
+R = Decorate ∘F Embed.R
+
+B₁ : 𝒞.U [ A , C ] → 𝒞.U [ B , C ] → 𝒟.U [ 𝒟.unit , F.F₀ C ] → DecoratedCospans [ A , B ]
+B₁ f g s = record
+    { cospan = Embed.B₁ f g
+    ; decoration = s
+    }
+
+module _ where
+
+  module L = Functor L
+  module R = Functor R
+
+  module Codiagonal where
+
+    open mc𝒞 using (unitorˡ; unitorʳ; +-monoidal) public
+    open unitorˡ using () renaming (to to λ⇐′) public
+    open unitorʳ using () renaming (to to ρ⇐′) public
+    open 𝒞 using (U; _+_; []-cong₂; []∘+₁; ∘-distribˡ-[]; inject₁; inject₂; ¡)
+      renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+    open Category U
+    open Equiv
+    open HomReasoning
+    open ⇒-Reasoning 𝒞.U
+
+    μ : {X : Obj} → X + X ⇒ X
+    μ = [ id , id ]′
+
+    μ∘+ : {X Y Z : Obj} {f : X ⇒ Z} {g : Y ⇒ Z} → [ f , g ]′ ≈ μ ∘ f +₁ g
+    μ∘+ = []-cong₂ (sym identityˡ) (sym identityˡ) ○ sym []∘+₁
+
+    μ∘¡ˡ : {X : Obj} → μ ∘ ¡ +₁ id ∘ λ⇐′ ≈ id {X}
+    μ∘¡ˡ = begin
+        μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩
+        [ ¡ , id ]′ ∘ λ⇐′ ≈⟨ inject₂ ⟩
+        id                ∎
+
+    μ∘¡ʳ : {X : Obj} → μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈ id {X}
+    μ∘¡ʳ = begin
+        μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩
+        [ id , ¡ ]′ ∘ ρ⇐′ ≈⟨ inject₁ ⟩
+        id                ∎
+
+
+    μ-natural : {X Y : Obj} {f : X ⇒ Y} → f ∘ μ ≈ μ ∘ f +₁ f
+    μ-natural = ∘-distribˡ-[] ○ []-cong₂ (identityʳ ○ sym identityˡ) (identityʳ ○ sym identityˡ) ○ sym []∘+₁
+
+  B∘L : {A B M C : 𝒞.Obj}
+      → {f : 𝒞.U [ A , B ]}
+      → {g : 𝒞.U [ B , M ]}
+      → {h : 𝒞.U [ C , M ]}
+      → {s : 𝒟.U [ 𝒟.unit , F.₀ M ]}
+      → DecoratedCospans [ DecoratedCospans [ B₁ g h s ∘ L.₁ f ] ≈ B₁ (𝒞.U [ g ∘ f ]) h s ]
+  B∘L {A} {B} {M} {C} {f} {g} {h} {s} = record
+      { cospans-≈ = Embed.B∘L
+      ; same-deco = same-deco
+      }
+    where
+
+      module _ where
+        open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+        open 𝒞 using (U)
+        open Category U
+        open mc𝒞 using (unitorˡ; unitorˡ-commute-to; +-monoidal) public
+        open unitorˡ using () renaming (to to λ⇐′) public
+        open ⊗-Reasoning +-monoidal
+        open ⇒-Reasoning 𝒞.U
+        open Equiv
+
+        open Pushout′ 𝒞.U using (pushout-id-g)
+        open PushoutProperties 𝒞.U using (up-to-iso)
+        open DiagramPushout 𝒞.U using (Pushout)
+        P P′ : Pushout 𝒞.id g
+        P = pushout 𝒞.id g
+        P′ = pushout-id-g
+        module P = Pushout P
+        module P′ = Pushout P′
+        open Morphism 𝒞.U using (_≅_)
+        open _≅_ using (from)
+        open P using (i₁ ; i₂; universal∘i₂≈h₂) public
+
+        open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ˡ)
+
+        ≅ : P.Q ⇒ M
+        ≅ = up-to-iso P P′ .from
+
+        ≅∘[]∘¡+id : ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈ id
+        ≅∘[]∘¡+id = begin
+          ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′  ≈⟨ assoc²αε ⟩
+          ≅ ∘ [ i₁ , i₂ ]′ ∘ ¡ +₁ id ∘ λ⇐′      ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩
+          ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ ¡ +₁ id ∘ λ⇐′      ≈⟨ refl⟩∘⟨ pull-center (sym split₁ʳ) ⟩
+          ≅ ∘ μ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′          ≈⟨ extendʳ μ-natural ⟩
+          μ ∘ ≅ +₁ ≅ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′     ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩
+          μ ∘ (≅ ∘ i₁ ∘ ¡) +₁ (≅ ∘ i₂) ∘ λ⇐′    ≈⟨ refl⟩∘⟨ sym (¡-unique (≅ ∘ i₁ ∘ ¡)) ⟩⊗⟨ universal∘i₂≈h₂ ⟩∘⟨refl ⟩
+          μ ∘ ¡ +₁ id ∘ λ⇐′                     ≈⟨ μ∘¡ˡ ⟩
+          id                                    ∎
+
+      open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-)
+      open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+      open Category U
+      open Equiv
+      open ⇒-Reasoning U
+      open ⊗-Reasoning monoidal
+      open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+      open F using (F₁; ε)
+      open Shorthands monoidal
+
+      same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s
+      same-deco = begin
+          F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐                     ≈⟨ pullˡ (sym F.homomorphism) ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ id ∘ ε ⊗₁ s ∘ ρ⇐                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym F.identity ⟩∘⟨refl ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ F₁ 𝒞.id ∘ ε ⊗₁ s ∘ ρ⇐           ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , 𝒞.id)) ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐            ≈⟨ pullˡ (sym F.homomorphism) ⟩
+          F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
+          F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐  ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟩
+          F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐          ≈⟨ pullˡ (sym F.homomorphism) ⟩
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐         ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟩
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ ρ⇐               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟨
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ λ⇐               ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ λ-.isoʳ) ⟩
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s                         ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘¡+id ○ F.identity) ⟩
+          s                                                                             ∎
+
+  R∘B : {A N B C : 𝒞.Obj}
+      → {f : 𝒞.U [ A , N ]}
+      → {g : 𝒞.U [ B , N ]}
+      → {h : 𝒞.U [ C , B ]}
+      → {s : 𝒟.U [ 𝒟.unit , F.₀ N ]}
+      → DecoratedCospans [ DecoratedCospans [ R.₁ h ∘ B₁ f g s ] ≈ B₁ f (𝒞.U [ g ∘ h ]) s ]
+  R∘B {A} {N} {B} {C} {f} {g} {h} {s} = record
+      { cospans-≈ = Embed.R∘B
+      ; same-deco = same-deco
+      }
+    where
+
+      module _ where
+        open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+        open 𝒞 using (U)
+        open Category U
+        open mc𝒞 using (unitorʳ; unitorˡ; unitorˡ-commute-to; +-monoidal) public
+        open unitorˡ using () renaming (to to λ⇐′) public
+        open unitorʳ using () renaming (to to ρ⇐′) public
+        open ⊗-Reasoning +-monoidal
+        open ⇒-Reasoning 𝒞.U
+        open Equiv
+
+        open Pushout′ 𝒞.U using (pushout-f-id)
+        open PushoutProperties 𝒞.U using (up-to-iso)
+        open DiagramPushout 𝒞.U using (Pushout)
+        P P′ : Pushout g 𝒞.id
+        P = pushout g 𝒞.id
+        P′ = pushout-f-id
+        module P = Pushout P
+        module P′ = Pushout P′
+        open Morphism 𝒞.U using (_≅_)
+        open _≅_ using (from)
+        open P using (i₁ ; i₂; universal∘i₁≈h₁) public
+
+        open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ʳ)
+
+        ≅ : P.Q ⇒ N
+        ≅ = up-to-iso P P′ .from
+
+        ≅∘[]∘id+¡ : ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈ id
+        ≅∘[]∘id+¡ = begin
+          ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′  ≈⟨ assoc²αε ⟩
+          ≅ ∘ [ i₁ , i₂ ]′ ∘ id +₁ ¡ ∘ ρ⇐′      ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩
+          ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ id +₁ ¡ ∘ ρ⇐′      ≈⟨ refl⟩∘⟨ pull-center merge₂ʳ ⟩
+          ≅ ∘ μ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′          ≈⟨ extendʳ μ-natural ⟩
+          μ ∘ ≅ +₁ ≅ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′     ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩
+          μ ∘ (≅ ∘ i₁) +₁ (≅ ∘ i₂ ∘ ¡) ∘ ρ⇐′    ≈⟨ refl⟩∘⟨ universal∘i₁≈h₁ ⟩⊗⟨ sym (¡-unique (≅ ∘ i₂ ∘ ¡)) ⟩∘⟨refl ⟩
+          μ ∘ id +₁ ¡ ∘ ρ⇐′                     ≈⟨ μ∘¡ʳ ⟩
+          id                                    ∎
+
+      open 𝒟 using (U; monoidal; _⊗₁_; unitorʳ-commute-from) renaming (module unitorˡ to λ-; module unitorʳ to ρ)
+      open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ )
+      open Category U
+      open Equiv
+      open ⇒-Reasoning U
+      open ⊗-Reasoning monoidal
+      open F.⊗-homo using () renaming (η to φ; commute to φ-commute)
+      open F using (F₁; ε)
+      open Shorthands monoidal
+
+      same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s
+      same-deco = begin
+          F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐                        ≈⟨ pullˡ (sym F.homomorphism) ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ F₁ 𝒞.id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐              ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (𝒞.id , ¡)) ⟩
+          F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐               ≈⟨ pullˡ (sym F.homomorphism) ⟩
+          F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
+          F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐     ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorʳ) F.unitaryʳ) ⟩
+          F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ F₁ ρ⇐′ ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐             ≈⟨ pullˡ (sym F.homomorphism) ⟩
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐            ≈⟨ refl⟩∘⟨ extendʳ unitorʳ-commute-from ⟩
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ∘ ρ⇒ ∘ ρ⇐                  ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ ρ.isoʳ) ⟩
+          F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s                            ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘id+¡ ○ F.identity) ⟩
+          s                                                                                ∎
+
+  open Morphism 𝒞.U using (_≅_)
+  open _≅_
+
+  ≅-L-R : (X≅Y : A ≅ B) → DecoratedCospans [ L.₁ (to X≅Y) ≈ R.₁ (from X≅Y) ]
+  ≅-L-R X≅Y = Decorate.F-resp-≈ (Embed.≅-L-R X≅Y)
+    where
+      module Decorate = Functor Decorate
+
+  module ⊗ = Functor (⊗ 𝒞 F)
+  open 𝒞 using (_+₁_)
+
+  L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ]
+  L-resp-⊗ = Decorate.F-resp-≈ Embed.L-resp-⊗ ○ Decorate-resp-⊗
+    where
+      module Decorate = Functor Decorate
+      open DecoratedCospans.HomReasoning
diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
new file mode 100644
index 0000000..80b7b2f
--- /dev/null
+++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda
@@ -0,0 +1,229 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --no-require-unique-meta-solutions #-}
+
+open import Level using (Level)
+module Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o ℓ e : Level} where
+
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Object.Coproduct as Coproduct
+import Categories.Object.Initial as Initial
+
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘)
+open import Categories.Functor.Monoidal using (IsMonoidalFunctor)
+open import Categories.Functor.Monoidal.Braided using (module Lax)
+open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_])
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory; MonoidalCategory)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Morphism using (_≅_)
+open import Categories.Morphism.Notation using (_[_≅_])
+open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper) renaming (refl to ≃-refl)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using (module Lax)
+open import Data.Product.Base using (_,_)
+
+open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat)
+open import Functor.Exact using (RightExactFunctor; idREF; ∘-RightExactFunctor)
+
+open FinitelyCocompleteCategory using () renaming (symmetricMonoidalCategory to smc)
+open SymmetricMonoidalCategory using (unit) renaming (braidedMonoidalCategory to bmc)
+open BraidedMonoidalCategory using () renaming (monoidalCategory to mc)
+
+private
+  variable
+    A B C : FinitelyCocompleteCategory o ℓ e
+
+F₀ : FinitelyCocompleteCategory o ℓ e → SymmetricMonoidalCategory o ℓ e
+F₀ C = smc C
+{-# INJECTIVE_FOR_INFERENCE F₀ #-}
+
+F₁ : RightExactFunctor A B → Lax.SymmetricMonoidalFunctor (F₀ A) (F₀ B)
+F₁ {A} {B} F = record
+    { F = F.F
+    ; isBraidedMonoidal = record
+        { isMonoidal = record
+            { ε = ε-iso.from
+            ; ⊗-homo = ⊗-homo
+            ; associativity = assoc
+            ; unitaryˡ = unitaryˡ
+            ; unitaryʳ = unitaryʳ
+            }
+        ; braiding-compat = braiding-compat
+        }
+    }
+  where
+    module F = RightExactFunctor F
+    module A = SymmetricMonoidalCategory (F₀ A)
+    module B = SymmetricMonoidalCategory (F₀ B)
+    module A′ = FinitelyCocompleteCategory A
+    module B′ = FinitelyCocompleteCategory B
+    ε-iso : B.U [ B.unit ≅ F.₀ A.unit ]
+    ε-iso = Initial.up-to-iso B.U B′.initial (record { ⊥ = F.₀ A′.⊥ ; ⊥-is-initial = F.F-resp-⊥ A′.⊥-is-initial })
+    module ε-iso = _≅_ ε-iso
+    +-iso : ∀ {X Y} → B.U [ F.₀ X B′.+ F.₀ Y ≅ F.₀ (X A′.+ Y) ]
+    +-iso = Coproduct.up-to-iso B.U B′.coproduct (Coproduct.IsCoproduct⇒Coproduct B.U (F.F-resp-+ (Coproduct.Coproduct⇒IsCoproduct A.U A′.coproduct)))
+    module +-iso {X Y} = _≅_ (+-iso {X} {Y})
+    module B-proofs where
+      open ⇒-Reasoning B.U
+      open B.HomReasoning
+      open B.Equiv
+      open B using (_∘_; _≈_)
+      open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂)
+      open A′ using (_+_; i₁; i₂)
+      ⊗-homo : NaturalTransformation (B.⊗ ∘F (F.F ⁂ F.F)) (F.F ∘F A.⊗)
+      ⊗-homo = ntHelper record
+          { η = λ { (X , Y) → +-iso.from {X} {Y} }
+          ; commute = λ { {X , Y} {X′ , Y′} (f , g) →
+              B′.coproduct.∘-distribˡ-[]
+              ○ B′.coproduct.[]-cong₂
+                  (pullˡ B′.coproduct.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₁))
+                  (pullˡ B′.coproduct.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₂))
+              ○ sym B′.coproduct.∘-distribˡ-[] }
+          }
+      assoc
+          : {X Y Z : A.Obj}
+          → F.₁ A′.+-assocˡ
+          ∘ +-iso.from {X + Y} {Z}
+          ∘ (+-iso.from {X} {Y} +₁ B.id {F.₀ Z})
+          ≈ +-iso.from {X} {Y + Z}
+          ∘ (B.id {F.₀ X} +₁ +-iso.from {Y} {Z})
+          ∘ B′.+-assocˡ
+      assoc {X} {Y} {Z} = begin
+          F.₁ A′.+-assocˡ ∘ +-iso.from ∘ (+-iso.from +₁ B.id)                               ≈⟨ refl⟩∘⟨ B′.[]∘+₁ ⟩
+          F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ]                      ≈⟨ refl⟩∘⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩
+          F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
+          B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ]             ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩
+          B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ]         ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩
+          B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ]       ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ]                      ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ]                    ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ]         ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ (i₂ A′.∘ i₂) ∘ B.id ]                 ≈⟨ []-cong₂ ([]-congˡ F.homomorphism) (B.identityʳ ○ F.homomorphism) ⟩
+          B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ]                       ≈⟨ []-congʳ ([]-congˡ B′.coproduct.inject₁) ⟨
+          B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁  , _ ] ∘ B′.i₁ ] , _ ]                 ≈⟨ []-congʳ ([]-cong₂ (sym B′.coproduct.inject₁) (pushˡ (sym B′.coproduct.inject₂))) ⟩
+          B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ]   ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟨
+          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ]         ≈⟨ []-congˡ B′.coproduct.inject₂ ⟨
+          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ]      ≈⟨ []-congˡ (pushˡ (sym B′.coproduct.inject₂)) ⟩
+          B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ]       ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨
+          B′.[ F.₁ i₁ ,  B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ           ≈⟨ []-cong₂ B.identityʳ (B′.coproduct.∘-distribˡ-[]) ⟩∘⟨refl ⟨
+          B′.[ F.₁ i₁ B′.∘ B′.id , F.₁ i₂ ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ] ∘ B′.+-assocˡ          ≈⟨ pushˡ (sym B′.[]∘+₁) ⟩
+          +-iso.from ∘ (B.id +₁ +-iso.from) ∘ B′.+-assocˡ                                   ∎
+      unitaryˡ
+          : {X : A.Obj}
+          → F.₁ A′.[ A′.initial.! , A.id {X} ]
+          ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]
+          ∘ B′.[ B′.i₁ ∘ B′.initial.! , B′.i₂ ∘ B.id ]
+          ≈ B′.[ B′.initial.! , B.id ]
+      unitaryˡ {X} = begin
+          F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ]   ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩
+          _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.initial.! , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ]         ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.coproduct.inject₂) ⟩
+          F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ B′.initial.! , F.₁ i₂ ∘  B.id ]               ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
+          B′.[ _ ∘ B′.initial.! , F.₁ A′.[ A′.initial.! , A.id ] ∘ F.₁ i₂ ∘  B.id ]           ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩
+          B′.[ B′.initial.! , F.₁ A.id ∘  B.id ]                                              ≈⟨ []-congˡ (elimˡ F.identity) ⟩
+          B′.[ B′.initial.! , B.id ]                                                          ∎
+      unitaryʳ
+          : {X : A.Obj}
+          → F.₁ A′.[ A′.id {X} , A′.initial.! ]
+          ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]
+          ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.initial.! ]
+          ≈ B′.[ B.id , B′.initial.! ]
+      unitaryʳ {X} = begin
+          F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ]   ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩
+          _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.initial.! ]         ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.coproduct.inject₁) (sym (B′.¡-unique _)) ⟩
+          F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ ∘  B.id , B′.initial.! ]               ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
+          B′.[ F.₁ A′.[ A.id , A′.initial.! ] ∘ F.₁ i₁ ∘  B.id , _ ∘ B′.initial.! ]           ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) (sym (B′.¡-unique _)) ⟩
+          B′.[ F.₁ A.id ∘  B.id , B′.initial.! ]                                              ≈⟨ []-congʳ (elimˡ F.identity) ⟩
+          B′.[ B.id , B′.initial.! ]                                                          ∎
+      braiding-compat
+          : {X Y : A.Obj}
+          → F.₁ A′.[ i₂ {X} {Y} , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]
+          ≈ B′.[ F.F₁ i₁ , F.F₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ]
+      braiding-compat = begin
+          F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ]                             ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩
+          B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ]        ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.coproduct.inject₁) ([ F.F ]-resp-∘ A′.coproduct.inject₂) ⟩
+          B′.[ F.₁ i₂ , F.₁ i₁ ]                                                  ≈⟨ []-cong₂ B′.coproduct.inject₂ B′.coproduct.inject₁ ⟨
+          B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ]  ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨
+          B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ]   ∎
+    open B-proofs
+
+identity : Lax.SymmetricMonoidalNaturalIsomorphism (F₁ (Functor.Exact.idREF {o} {ℓ} {e} {A})) (idF-SymmetricMonoidal (F₀ A))
+identity {A} = record
+    { U = ≃-refl
+    ; F⇒G-isMonoidal = record
+        { ε-compat = ¡-unique₂ (id ∘ ¡) id
+        ; ⊗-homo-compat = refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ)
+        }
+    }
+  where
+    open FinitelyCocompleteCategory A
+    open HomReasoning
+    open Equiv
+
+homomorphism
+    : {F : RightExactFunctor A B}
+      {G : RightExactFunctor B C}
+    → Lax.SymmetricMonoidalNaturalIsomorphism
+        (F₁ {A} {C} (∘-RightExactFunctor G F))
+        (∘-SymmetricMonoidal (F₁ {B} {C} G) (F₁ {A} {B} F))
+homomorphism {A} {B} {C} {F} {G} = record
+    { U = ≃-refl
+    ; F⇒G-isMonoidal = record
+        { ε-compat = ¡-unique₂ (id ∘ ¡) (G.₁ B.¡ ∘ ¡)
+        ; ⊗-homo-compat =
+            identityˡ
+            ○ sym
+                ([]-cong₂
+                    ([ G.F ]-resp-∘ B.coproducts.inject₁)
+                    ([ G.F ]-resp-∘ B.coproducts.inject₂))
+            ○ sym ∘-distribˡ-[]
+            ○ pushʳ (introʳ C.⊗.identity)
+        }
+    }
+  where
+    module A = FinitelyCocompleteCategory A
+    module B = FinitelyCocompleteCategory B
+    open FinitelyCocompleteCategory C
+    module C = SymmetricMonoidalCategory (F₀ C)
+    open HomReasoning
+    open Equiv
+    open ⇒-Reasoning U
+    module F = RightExactFunctor F
+    module G = RightExactFunctor G
+
+module _ {F G : RightExactFunctor A B} where
+
+  module F = RightExactFunctor F
+  module G = RightExactFunctor G
+
+  F-resp-≈
+      : NaturalIsomorphism F.F G.F
+      → Lax.SymmetricMonoidalNaturalIsomorphism (F₁ {A} {B} F) (F₁ {A} {B} G)
+  F-resp-≈ F≃G = record
+      { U = F≃G
+      ; F⇒G-isMonoidal = record
+          { ε-compat = sym (¡-unique (⇒.η A.⊥ ∘ ¡))
+          ; ⊗-homo-compat =
+              ∘-distribˡ-[]
+              ○ []-cong₂ (⇒.commute A.i₁) (⇒.commute A.i₂)
+              ○ sym []∘+₁
+          }
+      }
+    where
+      module A = FinitelyCocompleteCategory A
+      open NaturalIsomorphism F≃G
+      open FinitelyCocompleteCategory B
+      open HomReasoning
+      open Equiv
+
+Underlying : Functor FinitelyCocompletes SymMonCat
+Underlying = record
+    { F₀ = F₀
+    ; F₁ = F₁
+    ; identity = λ { {X} → identity {X} }
+    ; homomorphism = λ { {X} {Y} {Z} {F} {G} → homomorphism {X} {Y} {Z} {F} {G} }
+    ; F-resp-≈ = λ { {X} {Y} {F} {G} → F-resp-≈ {X} {Y} {F} {G} }
+    }