Category of decorated cospans is symmetric monoidal

3 files changed, 633 insertions, 0 deletions

diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda
new file mode 100644
index 0000000..c570e54
--- /dev/null
+++ b/Category/Monoidal/Instance/DecoratedCospans.agda
@@ -0,0 +1,415 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+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 Category.Monoidal.Instance.DecoratedCospans
+    {o o′ ℓ ℓ′ e e′}
+    (𝒞 : FinitelyCocompleteCategory o ℓ e)
+    {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
+    (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
+
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Category.Monoidal.Properties as ⊗-Properties
+import Categories.Category.Monoidal.Braided.Properties as σ-Properties
+
+open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Core using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Hom using (Hom[_][_,-])
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Categories.Functor.Monoidal.Construction.Product using (⁂-SymmetricMonoidalFunctor)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _ⓘˡ_; niHelper)
+open import Categories.NaturalTransformation.Core using (NaturalTransformation; _∘ᵥ_; ntHelper)
+open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≋_)
+open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans)
+open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (module x+y; module y+x; [x+y]+z; x+[y+z]; assoc-≃)
+open import Category.Monoidal.Instance.DecoratedCospans.Lift {o} {ℓ} {e} {o′} {ℓ′} {e′} using (module Square)
+open import Cospan.Decorated 𝒞 F using (DecoratedCospan)
+open import Data.Product.Base using (_,_)
+open import Function.Base using () renaming (id to idf)
+open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗)
+open import Functor.Instance.DecoratedCospan.Embed 𝒞 F using (L; L-resp-⊗; B₁)
+
+open import Category.Monoidal.Instance.DecoratedCospans.Products 𝒞 F
+open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
+open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-naturalIsomorphism)
+
+module LiftUnitorˡ where
+    module ⊗ = Functor ⊗
+    module F = SymmetricMonoidalFunctor F
+    open 𝒞 using (⊥; _+-; i₂; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
+    open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐; λ⇒)
+    ≃₁ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (⊥ +-))
+    ≃₁ = ntHelper record
+        { η = λ { X → record
+            { to = λ { f → 𝒟.U [ F.⊗-homo.η (⊥ , X) ∘ 𝒟.U [ 𝒟.⊗.₁ (𝒟.U [ F.₁ 𝒞.initial.! ∘ F.ε ] , f) ∘ ρ⇐ ] ] }
+            ; cong = λ { x → refl⟩∘⟨ refl⟩⊗⟨ x ⟩∘⟨refl } }
+            }
+        ; commute = ned
+        }
+      where
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+        ned : {X Y : 𝒞.Obj} (f : X 𝒞.⇒ Y) {x : 𝒟.unit 𝒟.⇒ F.₀ X}
+            → F.⊗-homo.η (⊥ , Y) ∘ (F.₁ ¡ 𝒟.∘ F.ε) ⊗₁ (F.F₁ f ∘ x ∘ id) ∘ ρ⇐
+            𝒟.≈ F.₁ (𝒞.id +₁ f) ∘ (F.⊗-homo.η (𝒞.⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐) ∘ id
+        ned {X} {Y} f {x} = begin
+              F.⊗-homo.η (⊥ , Y) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ (F.₁ f ∘ x ∘ id) ∘ ρ⇐            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl ⟩
+              F.⊗-homo.η (⊥ , Y) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ (F.₁ f ∘ x) ∘ ρ⇐                 ≈⟨ push-center (sym split₂ˡ) ⟩
+              F.⊗-homo.η (⊥ , Y) ∘ id ⊗₁ F.₁ f ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐             ≈⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟨
+              F.⊗-homo.η (⊥ , Y) ∘ F.₁ 𝒞.id ⊗₁ F.₁ f ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐       ≈⟨ extendʳ (F.⊗-homo.commute (𝒞.id , f)) ⟩
+              F.₁ (𝒞.id +₁ f) ∘ F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐         ≈⟨ refl⟩∘⟨ identityʳ ⟨
+              F.₁ (𝒞.id +₁ f) ∘ (F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐) ∘ id  ∎
+    ≃₂ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F idF)
+    ≃₂ = ntHelper record
+        { η = λ { X → record { to = idf ; cong = idf } }
+        ; commute = λ { f → refl }
+        }
+      where
+        open 𝒟.Equiv
+    open NaturalIsomorphism using (F⇐G)
+    ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ ⊥+--id))) ∘ᵥ ≃₂ ≋ ≃₁
+    ≃₂≋≃₁ {X} {f} = begin
+        F.₁ λ⇐ ∘ f ∘ id                                                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟨
+        F.₁ λ⇐ ∘ f ∘ ρ⇒ ∘ ρ⇐                                            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ coherence₃ ⟩∘⟨refl ⟨
+        F.₁ λ⇐ ∘ f ∘ λ⇒ ∘ ρ⇐                                            ≈⟨ refl⟩∘⟨ extendʳ 𝒟.unitorˡ-commute-from ⟨
+        F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐                                      ≈⟨ pushˡ (introˡ F.identity) ⟩
+        F.₁ 𝒞.id ∘ F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐                           ≈⟨ F.F-resp-≈ (-+-.identity) ⟩∘⟨refl ⟨
+        F.₁ (𝒞.id +₁ 𝒞.id) ∘ F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐                 ≈⟨ F.F-resp-≈ (+₁-cong₂ (¡-unique 𝒞.id) 𝒞.Equiv.refl) ⟩∘⟨refl ⟨
+        F.₁ (¡ +₁ 𝒞.id) ∘ F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐                    ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ)  ⟨
+        F.₁ (¡ +₁ 𝒞.id) ∘ F.⊗-homo.η (⊥ , X) ∘ F.ε ⊗₁ id ∘ id ⊗₁ f ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩
+        F.₁ (¡ +₁ 𝒞.id) ∘ F.⊗-homo.η (⊥ , X) ∘ F.ε ⊗₁ f ∘ ρ⇐            ≈⟨ extendʳ (F.⊗-homo.commute (¡ , 𝒞.id)) ⟨
+        F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ⊗₁ F.₁ 𝒞.id) ∘ F.ε ⊗₁ f ∘ ρ⇐        ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ F.identity ⟩∘⟨refl ⟩
+        F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ⊗₁ id) ∘ F.ε ⊗₁ f ∘ ρ⇐              ≈⟨ pull-center (sym split₁ˡ) ⟩
+        F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ f ∘ ρ⇐                    ∎
+      where
+        open Shorthands 𝒞.monoidal using (λ⇐)
+        open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (unitorˡ)
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⊗-Properties 𝒟.monoidal using (coherence₃)
+        open ⇒-Reasoning 𝒟.U
+        module -+- = Functor -+-
+    module Unitorˡ = Square {𝒞} {𝒞} {𝒟} {𝒟} {F} {F} ⊥+--id ≃₁ ≃₂ ≃₂≋≃₁
+open LiftUnitorˡ using (module Unitorˡ)
+
+module LiftUnitorʳ where
+    module ⊗ = Functor ⊗
+    module F = SymmetricMonoidalFunctor F
+    open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
+    open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐)
+    ≃₁ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (-+ ⊥))
+    ≃₁ = ntHelper record
+        { η = λ { X → record
+            { to = λ { f → 𝒟.U [ F.⊗-homo.η (X , ⊥) ∘ 𝒟.U [ 𝒟.⊗.₁ (f , 𝒟.U [ F.₁ 𝒞.initial.! ∘ F.ε ]) ∘ ρ⇐ ] ] }
+            ; cong = λ { x → refl⟩∘⟨ x ⟩⊗⟨refl ⟩∘⟨refl } }
+            }
+        ; commute = ned
+        }
+      where
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+        ned : {X Y : 𝒞.Obj} (f : X 𝒞.⇒ Y) {x : 𝒟.unit 𝒟.⇒ F.₀ X}
+            → F.⊗-homo.η (Y , ⊥) ∘ (F.F₁ f ∘ x ∘ id) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐
+            𝒟.≈ F.₁ (f +₁ 𝒞.id) ∘ (F.⊗-homo.η (X , ⊥) ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐) ∘ id
+        ned {X} {Y} f {x} = begin
+              F.⊗-homo.η (Y , ⊥) ∘ (F.₁ f ∘ x ∘ id) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐             ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨refl ⟩∘⟨refl ⟩
+              F.⊗-homo.η (Y , ⊥) ∘ (F.₁ f ∘ x) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐                  ≈⟨ push-center (sym split₁ˡ) ⟩
+              F.⊗-homo.η (Y , ⊥) ∘ F.₁ f ⊗₁ id ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ F.identity ⟩∘⟨refl ⟨
+              F.⊗-homo.η (Y , ⊥) ∘ F.₁ f ⊗₁ F.₁ 𝒞.id ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐        ≈⟨ extendʳ (F.⊗-homo.commute (f , 𝒞.id)) ⟩
+              F.₁ (f +₁ 𝒞.id) ∘ F.⊗-homo.η (X , ⊥) ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐          ≈⟨ refl⟩∘⟨ identityʳ ⟨
+              F.₁ (f +₁ 𝒞.id) ∘ (F.⊗-homo.η (X , ⊥) ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐) ∘ id   ∎
+    ≃₂ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F idF)
+    ≃₂ = ntHelper record
+        { η = λ { X → record { to = idf ; cong = idf } }
+        ; commute = λ { f → refl }
+        }
+      where
+        open 𝒟.Equiv
+    open NaturalIsomorphism using (F⇐G)
+    ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ -+⊥-id))) ∘ᵥ ≃₂ ≋ ≃₁
+    ≃₂≋≃₁ {X} {f} = begin
+        F.₁ i₁ ∘ f ∘ id                                                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟨
+        F.₁ ρ⇐′ ∘ f ∘ ρ⇒ ∘ ρ⇐                                           ≈⟨ refl⟩∘⟨ extendʳ 𝒟.unitorʳ-commute-from ⟨
+        F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐                                     ≈⟨ pushˡ (introˡ F.identity) ⟩
+        F.₁ 𝒞.id ∘ F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐                          ≈⟨ F.F-resp-≈ (-+-.identity) ⟩∘⟨refl ⟨
+        F.₁ (𝒞.id +₁ 𝒞.id) ∘ F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐                ≈⟨ F.F-resp-≈ (+₁-cong₂ 𝒞.Equiv.refl (¡-unique 𝒞.id)) ⟩∘⟨refl ⟨
+        F.₁ (𝒞.id +₁ ¡) ∘ F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐                   ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorʳ) F.unitaryʳ)  ⟨
+        F.₁ (𝒞.id +₁ ¡) ∘ F.⊗-homo.η (X , ⊥) ∘ id ⊗₁ F.ε ∘ f ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₂₁) ⟩
+        F.₁ (𝒞.id +₁ ¡) ∘ F.⊗-homo.η (X , ⊥) ∘ f ⊗₁ F.ε ∘ ρ⇐            ≈⟨ extendʳ (F.⊗-homo.commute (𝒞.id , ¡)) ⟨
+        F.⊗-homo.η (X , ⊥) ∘ (F.₁ 𝒞.id ⊗₁ F.₁ ¡) ∘ f ⊗₁ F.ε ∘ ρ⇐        ≈⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        F.⊗-homo.η (X , ⊥) ∘ (id ⊗₁ F.₁ ¡) ∘ f ⊗₁ F.ε ∘ ρ⇐              ≈⟨ pull-center (sym split₂ˡ) ⟩
+        F.⊗-homo.η (X , ⊥) ∘ f ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐                    ∎
+      where
+        open Shorthands 𝒞.monoidal using () renaming (ρ⇐ to ρ⇐′)
+        open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (unitorʳ)
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+        module -+- = Functor -+-
+    module Unitorʳ = Square {𝒞} {𝒞} {𝒟} {𝒟} {F} {F} -+⊥-id ≃₁ ≃₂ ≃₂≋≃₁
+open LiftUnitorʳ using (module Unitorʳ)
+
+module LiftAssociator where
+    module ⊗ = Functor ⊗
+    module F = SymmetricMonoidalFunctor F
+    open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
+    open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐)
+    ≃₁ : NaturalTransformation (Hom[ [𝒟×𝒟]×𝒟.U ][ [𝒟×𝒟]×𝒟.unit ,-] ∘F [F×F]×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F ([x+y]+z.F {𝒞}))
+    ≃₁ = ntHelper record
+        { η = λ { ((X , Y) , Z) → record
+            { to = λ { ((f , g) , h) → F.⊗-homo.η (X + Y , Z) ∘ ((F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h) ∘ ρ⇐ }
+            ; cong = λ { {(f , g) , h} {(f′ , g′) , h′} ((x , y) , z) → refl⟩∘⟨ (refl⟩∘⟨ x ⟩⊗⟨ y ⟩∘⟨refl) ⟩⊗⟨ z ⟩∘⟨refl }
+            } }
+        ; commute = λ { {(X , Y) , Z} {(X′ , Y′) , Z′} ((x , y) , z) {(f , g) , h} → commute x y z f g h }
+        }
+      where
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+        commute
+            : {X Y Z X′ Y′ Z′ : 𝒞.Obj}
+              (x : 𝒞.U [ X , X′ ])
+              (y : 𝒞.U [ Y , Y′ ])
+              (z : 𝒞.U [ Z , Z′ ])
+              (f : 𝒟.U [ 𝒟.unit , F.₀ X ])
+              (g : 𝒟.U [ 𝒟.unit , F.₀ Y ])
+              (h : 𝒟.U [ 𝒟.unit , F.₀ Z ])
+            → F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.₁ y ∘ g ∘ id) ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐
+            ≈ F.₁ ((x +₁ y) +₁ z) ∘ (F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐) ∘ id
+        commute {X} {Y} {Z} {X′} {Y′} {Z′} x y z f g h = begin
+            F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.₁ y ∘ g ∘ id) ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl ⟩
+            F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ (F.₁ x ∘ f) ⊗₁ (F.₁ y ∘ g) ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ push-center (sym ⊗-distrib-over-∘) ⟩⊗⟨refl ⟩∘⟨refl ⟩
+            F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ F.₁ x ⊗₁ F.₁ y ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute (x , y)) ⟩⊗⟨refl ⟩∘⟨refl ⟩
+            F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.₁ (x +₁ y) ∘ F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐
+                ≈⟨ push-center (sym ⊗-distrib-over-∘) ⟩
+            F.⊗-homo.η (X′ + Y′ , Z′) ∘ F.₁ (x +₁ y) ⊗₁ F.₁ z ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐
+                ≈⟨ extendʳ (F.⊗-homo.commute (x +₁ y , z)) ⟩
+            F.₁ ((x +₁ y) +₁ z) ∘ F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ identityʳ ⟨
+            F.₁ ((x +₁ y) +₁ z) ∘ (F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐) ∘ id
+                ∎
+    ≃₂ : NaturalTransformation (Hom[ [𝒟×𝒟]×𝒟.U ][ [𝒟×𝒟]×𝒟.unit ,-] ∘F [F×F]×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (x+[y+z].F {𝒞}))
+    ≃₂ = ntHelper record
+        { η = λ { ((X , Y) , Z) → record
+            { to = λ { ((f , g) , h) → F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐)) ∘ ρ⇐ }
+            ; cong = λ { {(f , g) , h} {(f′ , g′) , h′} ((x , y) , z) → refl⟩∘⟨ x ⟩⊗⟨ (refl⟩∘⟨ y ⟩⊗⟨ z ⟩∘⟨refl) ⟩∘⟨refl }
+            } }
+        ; commute = λ { {(X , Y) , Z} {(X′ , Y′) , Z′} ((x , y) , z) {(f , g) , h} → commute x y z f g h }
+        }
+      where
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+        commute
+            : {X Y Z X′ Y′ Z′ : 𝒞.Obj}
+              (x : 𝒞.U [ X , X′ ])
+              (y : 𝒞.U [ Y , Y′ ])
+              (z : 𝒞.U [ Z , Z′ ])
+              (f : 𝒟.U [ 𝒟.unit , F.₀ X ])
+              (g : 𝒟.U [ 𝒟.unit , F.₀ Y ])
+              (h : 𝒟.U [ 𝒟.unit , F.₀ Z ])
+            → F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ (F.₁ y ∘ g ∘ id) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐) ∘ ρ⇐
+            ≈ F.₁ (x +₁ (y +₁ z)) ∘ (F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐) ∘ id
+        commute {X} {Y} {Z} {X′} {Y′} {Z′} x y z f g h = begin
+            F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ (F.₁ y ∘ g ∘ id) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl) ⟩∘⟨refl ⟩
+            F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ (F.₁ y ∘ g) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center (sym ⊗-distrib-over-∘) ⟩∘⟨refl ⟩
+            F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ F.₁ y ⊗₁ F.₁ z ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ (F.⊗-homo.commute (y , z)) ⟩∘⟨refl ⟩
+            F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f) ⊗₁ (F.₁ (y +₁ z) ∘ F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐
+                ≈⟨ push-center (sym ⊗-distrib-over-∘) ⟩
+            F.⊗-homo.η (X′ , Y′ + Z′) ∘ F.₁ x ⊗₁ F.₁ (y +₁ z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐
+                ≈⟨ extendʳ (F.⊗-homo.commute (x , y +₁ z)) ⟩
+            F.₁ (x +₁ (y +₁ z)) ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐
+                ≈⟨ refl⟩∘⟨ identityʳ ⟨
+            F.₁ (x +₁ (y +₁ z)) ∘ (F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐) ∘ id
+                ∎
+    open NaturalIsomorphism using (F⇐G)
+    ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ assoc-≃))) ∘ᵥ ≃₂ ≋ ≃₁
+    ≃₂≋≃₁ {(X , Y) , Z} {(f , g) , h} = begin
+        F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ _) ∘ ρ⇐) ∘ id                                               ≈⟨ refl⟩∘⟨ identityʳ ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym-assoc ⟩∘⟨refl ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ ((F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ ρ⇐) ∘ ρ⇐                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟨
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ λ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-to ⟨
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ λ⇐ ∘ ρ⇐                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (switch-tofromˡ α coherence-inv₁) ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g) ⊗₁ h ∘ ρ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym split₁ʳ) ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ (id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐          ≈⟨ refl⟩∘⟨ sym-assoc ⟩
+        F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐          ≈⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α′) F.associativity) ⟨
+        F.⊗-homo.η (X + Y , Z) ∘ F.⊗-homo.η (X , Y) ⊗₁ id ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐                           ≈⟨ refl⟩∘⟨ pullˡ (sym split₁ˡ) ⟩
+        F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ (f ⊗₁ g) ∘ ρ⇐) ⊗₁ h ∘ ρ⇐                               ∎
+      where
+        open Shorthands 𝒞.monoidal using () renaming (α⇐ to α⇐′)
+        open Shorthands 𝒟.monoidal using (α⇒; λ⇐)
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; assoc-commute-from; unitorˡ-commute-to) renaming (unitorˡ to ƛ; associator to α)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+        open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using () renaming (associator to α′)
+        open ⊗-Properties 𝒟.monoidal using (coherence-inv₁; coherence-inv₃)
+    module Associator = Square {[𝒞×𝒞]×𝒞} {𝒞} {[𝒟×𝒟]×𝒟} {𝒟} {[F×F]×F} {F} {[x+y]+z.F {𝒞}} {x+[y+z].F {𝒞}} (assoc-≃ {𝒞}) ≃₁ ≃₂ ≃₂≋≃₁
+open LiftAssociator using (module Associator)
+
+module LiftBraiding where
+    module ⊗ = Functor ⊗
+    module F = SymmetricMonoidalFunctor F
+    open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
+    open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐)
+    ≃₁ : NaturalTransformation (Hom[ 𝒟×𝒟.U ][ 𝒟×𝒟.unit ,-] ∘F F×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (x+y.F {𝒞}))
+    ≃₁ = ntHelper record
+        { η = λ { (X , Y) → record
+            { to = λ { (x , y) → F.⊗-homo.η (X , Y) ∘ x ⊗₁ y ∘ ρ⇐}
+            ; cong = λ { {x , y} {x′ , y′} (≈x , ≈y) → refl⟩∘⟨ ≈x ⟩⊗⟨ ≈y ⟩∘⟨refl }
+            } }
+        ; commute = λ { {X , Y} {X′ , Y′} (x , y) {f , g} →
+            (extendʳ
+                (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ)
+                ○ refl⟩∘⟨ ⊗-distrib-over-∘
+                ○ extendʳ (F.⊗-homo.commute (x , y))))
+            ○ refl⟩∘⟨ extendˡ (sym identityʳ) }
+        }
+      where
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_; assoc)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+    ≃₂ : NaturalTransformation (Hom[ 𝒟×𝒟.U ][ 𝒟×𝒟.unit ,-] ∘F F×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (y+x.F {𝒞}))
+    ≃₂ = ntHelper record
+        { η = λ { (X , Y) → record
+            { to = λ { (x , y) → F.⊗-homo.η (Y , X) ∘ y ⊗₁ x ∘ ρ⇐}
+            ; cong = λ { {x , y} {x′ , y′} (≈x , ≈y) → refl⟩∘⟨ ≈y ⟩⊗⟨ ≈x ⟩∘⟨refl }
+            } }
+        ; commute = λ { {X , Y} {X′ , Y′} (x , y) {f , g} →
+            (extendʳ
+                (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ)
+                ○ refl⟩∘⟨ ⊗-distrib-over-∘
+                ○ extendʳ (F.⊗-homo.commute (y , x))))
+            ○ refl⟩∘⟨ extendˡ (sym identityʳ) }
+        }
+      where
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_; assoc)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⇒-Reasoning 𝒟.U
+    open NaturalIsomorphism using (F⇐G)
+    open Symmetric 𝒞.symmetric using (braiding)
+    ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ F.F ⓘˡ braiding)) ∘ᵥ ≃₂ ≋ ≃₁
+    ≃₂≋≃₁ {X , Y} {f , g} =
+        refl⟩∘⟨ (identityʳ ○ sym-assoc)
+        ○ extendʳ
+            (extendʳ F.braiding-compat
+            ○ refl⟩∘⟨ (𝒟.braiding.⇒.commute (g , f)))
+        ○ refl⟩∘⟨ pullʳ (sym (switch-tofromˡ 𝒟.braiding.FX≅GX braiding-coherence-inv) ○ coherence-inv₃)
+      where
+        open σ-Properties 𝒟.braided using (braiding-coherence-inv)
+        open 𝒟.Equiv
+        open 𝒟 using (sym-assoc; identityʳ)
+        open ⊗-Reasoning 𝒟.monoidal
+        open ⊗-Properties 𝒟.monoidal using (coherence-inv₃)
+        open ⇒-Reasoning 𝒟.U
+    module Braiding = Square {𝒞×𝒞} {𝒞} {𝒟×𝒟} {𝒟} {F×F} {F} {x+y.F {𝒞}} {y+x.F {𝒞}} braiding ≃₁ ≃₂ ≃₂≋≃₁
+open LiftBraiding using (module Braiding)
+
+CospansMonoidal : Monoidal DecoratedCospans
+CospansMonoidal = record
+    { ⊗ = ⊗
+    ; unit = ⊥
+    ; unitorˡ = [ L ]-resp-≅ ⊥+A≅A
+    ; unitorʳ = [ L ]-resp-≅ A+⊥≅A
+    ; associator = [ L ]-resp-≅ (≅.sym +-assoc)
+    ; unitorˡ-commute-from = λ { {X} {Y} {f} → Unitorˡ.from f }
+    ; unitorˡ-commute-to = λ { {X} {Y} {f} → Unitorˡ.to f }
+    ; unitorʳ-commute-from = λ { {X} {Y} {f} → Unitorʳ.from f }
+    ; unitorʳ-commute-to = λ { {X} {Y} {f} → Unitorʳ.to f }
+    ; assoc-commute-from = λ { {X} {X′} {f} {Y} {Y′} {g} {Z} {Z′} {h} → Associator.from _ }
+    ; assoc-commute-to = λ { {X} {X′} {f} {Y} {Y′} {g} {Z} {Z′} {h} → Associator.to _ }
+    ; triangle = triangle
+    ; pentagon = pentagon
+    }
+  where
+    module ⊗ = Functor ⊗
+    open Category DecoratedCospans using (id; module Equiv; module HomReasoning)
+    open Equiv
+    open HomReasoning
+    open 𝒞 using (⊥; Obj; U; +-assoc)
+    λ⇒ = Unitorˡ.FX≅GX′.from
+    ρ⇒ = Unitorʳ.FX≅GX′.from
+    α⇒ = Associator.FX≅GX′.from
+    open Morphism U using (module ≅)
+    open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent)
+    triangle : {X Y : Obj} → DecoratedCospans [ DecoratedCospans [ ⊗.₁ (id {X} , λ⇒) ∘ α⇒ ] ≈ ⊗.₁ (ρ⇒ , id {Y}) ]
+    triangle = sym L-resp-⊗ ⟩∘⟨refl ○ sym L.homomorphism ○ L.F-resp-≈ tri ○ L-resp-⊗
+    pentagon
+        : {W X Y Z : Obj}
+        → DecoratedCospans
+            [ DecoratedCospans [ ⊗.₁ (id {W} , α⇒ {(X , Y) , Z}) ∘ DecoratedCospans [ α⇒ ∘ ⊗.₁ (α⇒ , id) ] ]
+            ≈ DecoratedCospans [ α⇒ ∘ α⇒ ] ]
+    pentagon = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym L.homomorphism ○ sym L.homomorphism ○ L.F-resp-≈ pent ○ L.homomorphism
+
+CospansBraided : Braided CospansMonoidal
+CospansBraided = record
+    { braiding = niHelper record
+        { η = λ { (X , Y) → Braiding.FX≅GX′.from {X , Y} }
+        ; η⁻¹ = λ { (Y , X) → Braiding.FX≅GX′.to {Y , X} }
+        ; commute = λ { {X , Y} {X′ , Y′} (f , g) → Braiding.from (record { cospan = record { f₁ = f₁ f , f₁ g ; f₂ = f₂ f , f₂ g } ; decoration = decoration f , decoration g}) }
+        ; iso = λ { (X , Y) → Braiding.FX≅GX′.iso {X , Y} }
+        }
+    ; hexagon₁ = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym L.homomorphism ○ sym L.homomorphism ○ L-resp-≈ hex₁ ○ L.homomorphism ○ refl⟩∘⟨ L.homomorphism
+    ; hexagon₂ = sym L-resp-⊗ ⟩∘⟨refl ⟩∘⟨ sym L-resp-⊗ ○ sym L.homomorphism ⟩∘⟨refl ○ sym L.homomorphism ○ L-resp-≈ hex₂ ○ L.homomorphism ○ L.homomorphism ⟩∘⟨refl
+    }
+  where
+    open Symmetric 𝒞.symmetric renaming (hexagon₁ to hex₁; hexagon₂ to hex₂)
+    open DecoratedCospan
+    module Cospans = Category DecoratedCospans
+    open Cospans.Equiv
+    open Cospans.HomReasoning
+    open Functor L renaming (F-resp-≈ to L-resp-≈)
+
+CospansSymmetric : Symmetric CospansMonoidal
+CospansSymmetric = record
+    { braided = CospansBraided
+    ; commutative = sym homomorphism ○ L-resp-≈ comm ○ identity
+    }
+  where
+    open Symmetric 𝒞.symmetric renaming (commutative to comm)
+    module Cospans = Category DecoratedCospans
+    open Cospans.Equiv
+    open Cospans.HomReasoning
+    open Functor L renaming (F-resp-≈ to L-resp-≈)
diff --git a/Category/Monoidal/Instance/DecoratedCospans/Lift.agda b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda
new file mode 100644
index 0000000..70795dd
--- /dev/null
+++ b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda
@@ -0,0 +1,114 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Monoidal.Instance.DecoratedCospans.Lift {o ℓ e o′ ℓ′ e′} where
+
+import Categories.Diagram.Pushout as PushoutDiagram
+import Categories.Diagram.Pushout.Properties as PushoutProperties
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Category.Diagram.Pushout as PushoutDiagram′
+import Functor.Instance.DecoratedCospan.Embed as CospanEmbed
+
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]; module Definitions)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Hom using (Hom[_][_,-])
+open import Categories.Functor.Properties using ([_]-resp-≅)
+open import Categories.NaturalTransformation using (NaturalTransformation; _∘ᵥ_)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; _ⓘˡ_)
+open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≋_)
+open import Function.Bundles using (_⟨$⟩_)
+open import Function.Construct.Composition using () renaming (function to _∘′_)
+open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout)
+
+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 Category.Instance.Cospans using (Cospans; Cospan)
+open import Category.Instance.DecoratedCospans using (DecoratedCospans)
+open import Category.Monoidal.Instance.Cospans.Lift {o} {ℓ} {e} using () renaming (module Square to Square′)
+open import Cospan.Decorated using (DecoratedCospan)
+
+open Lax using (SymmetricMonoidalFunctor)
+open FinitelyCocompleteCategory
+  using ()
+  renaming (symmetricMonoidalCategory to smc)
+
+module _
+  {𝒞 : FinitelyCocompleteCategory o ℓ e}
+  {𝒟 : FinitelyCocompleteCategory o ℓ e}
+  {𝒥 : SymmetricMonoidalCategory o′ ℓ′ e′}
+  {𝒦 : SymmetricMonoidalCategory o′ ℓ′ e′}
+  {H : SymmetricMonoidalFunctor (smc 𝒞) 𝒥}
+  {I : SymmetricMonoidalFunctor (smc 𝒟) 𝒦} where
+
+  module 𝒞 = FinitelyCocompleteCategory 𝒞
+  module 𝒟 = FinitelyCocompleteCategory 𝒟
+  module 𝒥 = SymmetricMonoidalCategory 𝒥
+  module 𝒦 = SymmetricMonoidalCategory 𝒦
+  module H = SymmetricMonoidalFunctor H
+  module I = SymmetricMonoidalFunctor I
+
+  open CospanEmbed 𝒟 I using (L; B₁; B∘L; R∘B; ≅-L-R)
+  open NaturalIsomorphism using (F⇐G)
+
+  module Square
+    {F G : Functor 𝒞.U 𝒟.U}
+    (F≃G : F ≃ G)
+    (⇒H≃I∘F : NaturalTransformation (Hom[ 𝒥.U ][ 𝒥.unit ,-] ∘F H.F) (Hom[ 𝒦.U ][ 𝒦.unit ,-] ∘F I.F ∘F F))
+    (⇒H≃I∘G : NaturalTransformation (Hom[ 𝒥.U ][ 𝒥.unit ,-] ∘F H.F) (Hom[ 𝒦.U ][ 𝒦.unit ,-] ∘F I.F ∘F G))
+    (≋ : (F⇐G (Hom[ 𝒦.U ][ 𝒦.unit ,-] ⓘˡ (I.F ⓘˡ F≃G))) ∘ᵥ ⇒H≃I∘G ≋ ⇒H≃I∘F)
+    where
+
+    module F = Functor F
+    module G = Functor G
+    module ⇒H≃I∘F = NaturalTransformation ⇒H≃I∘F
+    module ⇒H≃I∘G = NaturalTransformation ⇒H≃I∘G
+
+    open NaturalIsomorphism F≃G
+
+    IF≃IG : I.F ∘F F ≃ I.F ∘F G
+    IF≃IG = I.F ⓘˡ F≃G
+
+    open Morphism using (module ≅) renaming (_≅_ to _[_≅_])
+    FX≅GX′ : ∀ {Z : 𝒞.Obj} → DecoratedCospans 𝒟 I [ F.₀ Z ≅ G.₀ Z ]
+    FX≅GX′ = [ L ]-resp-≅ FX≅GX
+    module FX≅GX {Z} = _[_≅_] (FX≅GX {Z})
+    module FX≅GX′ {Z} = _[_≅_] (FX≅GX′ {Z})
+
+    module _ {X Y : 𝒞.Obj} (fg : DecoratedCospans 𝒞 H [ X , Y ]) where
+
+      open DecoratedCospan fg renaming (f₁ to f; f₂ to g; decoration to s)
+      open 𝒟 using (_∘_)
+
+      squares⇒cospan
+          : DecoratedCospans 𝒟 I
+              [ B₁ (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) (⇒H≃I∘G.η N ⟨$⟩ s)
+              ≈ B₁ (F.₁ f) (F.₁ g) (⇒H≃I∘F.η N ⟨$⟩ s)
+              ]
+      squares⇒cospan = record
+          { cospans-≈ = Square′.squares⇒cospan F≃G cospan
+          ; same-deco = refl⟩∘⟨ sym 𝒦.identityʳ ○ ≋
+          }
+        where
+          open 𝒦.HomReasoning
+          open 𝒦.Equiv
+
+      module Cospans = Category (DecoratedCospans 𝒟 I)
+
+      from : DecoratedCospans 𝒟 I
+          [ DecoratedCospans 𝒟 I [ L.₁ (⇒.η Y) ∘ B₁ (F.₁ f) (F.₁ g) (⇒H≃I∘F.η N ⟨$⟩ s) ]
+          ≈ DecoratedCospans 𝒟 I [ B₁ (G.₁ f) (G.₁ g) (⇒H≃I∘G.η N ⟨$⟩ s) ∘ L.₁ (⇒.η X) ]
+          ]
+      from = sym (switch-tofromˡ FX≅GX′ (refl⟩∘⟨ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan))
+        where
+          open Cospans.Equiv using (sym)
+          open ⇒-Reasoning (DecoratedCospans 𝒟 I) using (switch-tofromˡ)
+          open Cospans.HomReasoning using (refl⟩∘⟨_; _○_; _⟩∘⟨refl)
+
+      to : DecoratedCospans 𝒟 I
+          [ DecoratedCospans 𝒟 I [ L.₁ (⇐.η Y) ∘ B₁ (G.₁ f) (G.₁ g) (⇒H≃I∘G.η N ⟨$⟩ s) ] ≈ DecoratedCospans 𝒟 I [ B₁ (F.₁ f) (F.₁ g) (⇒H≃I∘F.η N ⟨$⟩ s) ∘ L.₁ (⇐.η X) ]
+          ]
+      to = switch-fromtoʳ FX≅GX′ (pullʳ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan)
+        where
+          open ⇒-Reasoning (DecoratedCospans 𝒟 I) using (pullʳ; switch-fromtoʳ)
+          open Cospans.HomReasoning using (refl⟩∘⟨_; _○_; _⟩∘⟨refl)
diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda
new file mode 100644
index 0000000..f8ef542
--- /dev/null
+++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda
@@ -0,0 +1,104 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+
+open Lax using (SymmetricMonoidalFunctor)
+open FinitelyCocompleteCategory
+  using ()
+  renaming (symmetricMonoidalCategory to smc)
+
+module Category.Monoidal.Instance.DecoratedCospans.Products
+    {o o′ ℓ ℓ′ e e′}
+    (𝒞 : FinitelyCocompleteCategory o ℓ e)
+    {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′}
+    (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where
+
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category)
+open import Categories.Category.Core using (Category)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Monoidal.Properties using (∘-SymmetricMonoidal)
+open import Categories.Functor.Monoidal.Construction.Product using (⁂-SymmetricMonoidalFunctor)
+open import Categories.NaturalTransformation.Core using (NaturalTransformation; _∘ᵥ_; ntHelper)
+open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian)
+open import Category.Instance.Properties.SymMonCat {o′} {ℓ′} {e′} using () renaming (SymMonCat-Cartesian to SymMonCat-Cartesian′)
+open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC)
+open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC)
+open import Data.Product.Base using (_,_)
+open import Categories.Functor.Cartesian using (CartesianF)
+open import Functor.Cartesian.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using (Underlying)
+
+module SMC = CartesianF Underlying
+module SymMonCat-CC = CartesianCategory SymMonCat-CC
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+module 𝒟 = SymmetricMonoidalCategory 𝒟
+
+module _ where
+
+  open CartesianCategory FinitelyCocompletes-CC using (products)
+  open BinaryProducts products using (_×_)
+
+  𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e
+  𝒞×𝒞 = 𝒞 × 𝒞
+
+  [𝒞×𝒞]×𝒞 : FinitelyCocompleteCategory o ℓ e
+  [𝒞×𝒞]×𝒞 = (𝒞 × 𝒞) × 𝒞
+
+module _ where
+
+  module _ where
+
+    open Cartesian SymMonCat-Cartesian′ using (products)
+    open BinaryProducts products using (_×_; _⁂_)
+
+    𝒟×𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′
+    𝒟×𝒟 = 𝒟 × 𝒟
+    module 𝒟×𝒟 = SymmetricMonoidalCategory 𝒟×𝒟
+
+    [𝒟×𝒟]×𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′
+    [𝒟×𝒟]×𝒟 = (𝒟 × 𝒟) × 𝒟
+    module [𝒟×𝒟]×𝒟 = SymmetricMonoidalCategory [𝒟×𝒟]×𝒟
+
+  module _ where
+
+    open Cartesian SymMonCat-Cartesian using (products)
+    open BinaryProducts products using (_×_; _⁂_)
+
+    smc𝒞×𝒞 : SymmetricMonoidalCategory o ℓ e
+    smc𝒞×𝒞 = smc 𝒞 × smc 𝒞
+
+    smc[𝒞×𝒞]×𝒞 : SymmetricMonoidalCategory o ℓ e
+    smc[𝒞×𝒞]×𝒞 = (smc 𝒞×𝒞) × smc 𝒞
+
+  F×F′ : SymmetricMonoidalFunctor smc𝒞×𝒞 𝒟×𝒟
+  F×F′ = ⁂-SymmetricMonoidalFunctor {o′} {ℓ′} {e′} {o′} {ℓ′} {e′} {𝒟} {𝒟} {o} {ℓ} {e} {o} {ℓ} {e} {smc 𝒞} {smc 𝒞} F F
+
+  F×F : SymmetricMonoidalFunctor (smc 𝒞×𝒞) 𝒟×𝒟
+  F×F = ∘-SymmetricMonoidal F×F′ from
+    where
+      open Morphism SymMonCat-CC.U using (_≅_)
+      ≅ : smc 𝒞×𝒞 ≅ smc𝒞×𝒞
+      ≅ = SMC.×-iso 𝒞 𝒞
+      open _≅_ ≅
+  module F×F = SymmetricMonoidalFunctor F×F
+
+  [F×F]×F′ : SymmetricMonoidalFunctor smc[𝒞×𝒞]×𝒞 [𝒟×𝒟]×𝒟
+  [F×F]×F′ = ⁂-SymmetricMonoidalFunctor {o′} {ℓ′} {e′} {o′} {ℓ′} {e′} {𝒟×𝒟} {𝒟} {o} {ℓ} {e} {o} {ℓ} {e} {smc 𝒞×𝒞} {smc 𝒞} F×F F
+
+  [F×F]×F : SymmetricMonoidalFunctor (smc [𝒞×𝒞]×𝒞) [𝒟×𝒟]×𝒟
+  [F×F]×F = ∘-SymmetricMonoidal [F×F]×F′ from
+    where
+      open Morphism SymMonCat-CC.U using (_≅_)
+      ≅ : smc [𝒞×𝒞]×𝒞 ≅ smc[𝒞×𝒞]×𝒞
+      ≅ = SMC.×-iso 𝒞×𝒞 𝒞
+      open _≅_ ≅
+  module [F×F]×F = SymmetricMonoidalFunctor [F×F]×F