Category of decorated cospans is symmetric monoidal

10 files changed, 931 insertions, 8 deletions

diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda
index dedfa16..5425233 100644
--- a/Category/Instance/Properties/FinitelyCocompletes.agda
+++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda
@@ -1,23 +1,27 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level)
-module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where
+open import Level using (Level; suc; _⊔_)
 
+module Category.Cartesian.Instance.FinitelyCocompletes {o ℓ e : Level} where
+
+import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning as ⇒-Reasoning
 
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
-open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_)
 open import Categories.Diagram.Coequalizer using (IsCoequalizer)
+open import Categories.Functor.Bifunctor using (flip-bifunctor)
 open import Categories.Functor.Core using (Functor)
-open import Categories.Functor using (_∘F_) renaming (id to idF)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso)
 open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct)
 open import Categories.Object.Initial using (IsInitial)
+open import Data.Product.Base using (_,_) renaming (_×_ to _×′_)
+
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
 open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_)
-open import Data.Product.Base using (_,_) renaming (_×_ to _×′_)
 open import Functor.Exact using (IsRightExact; RightExactFunctor)
-open import Level using (_⊔_; suc)
+open import Functor.Exact.Instance.Swap using (Swap)
 
 FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
 FinitelyCocompletes-CC = record
@@ -202,9 +206,37 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
           ; F-resp-coeq = +-resp-coeq 𝒞
           }
       }
+  module x+y = RightExactFunctor -+-
+
+  ↔-+- : 𝒞 × 𝒞 ⇒ 𝒞
+  ↔-+- = -+- ∘ Swap 𝒞 𝒞
+  module y+x = RightExactFunctor ↔-+-
 
   [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
   [x+y]+z = -+- ∘ (-+- ×₁ id)
+  module [x+y]+z = RightExactFunctor [x+y]+z
 
   x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
   x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ
+  module x+[y+z] = RightExactFunctor x+[y+z]
+
+  assoc-≃ : [x+y]+z.F ≃ x+[y+z].F
+  assoc-≃ = pointwise-iso (λ { ((X , Y) , Z) → ≅.sym (𝒞.+-assoc {X} {Y} {Z})}) commute
+    where
+      open 𝒞
+      module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞)
+      open Morphism U using (_≅_; module ≅)
+      module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z}))
+      open import Categories.Category.BinaryProducts using (BinaryProducts)
+      open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct)
+      op-binaryProducts : BinaryProducts op
+      op-binaryProducts = record { product = Coproduct⇒coProduct coproduct }
+      open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⁂ to +₁∘assocˡ)
+      open Equiv
+      commute
+          : {((X , Y) , Z) : 𝒞×𝒞×𝒞.Obj}
+            {((X′ , Y′) , Z′) : 𝒞×𝒞×𝒞.Obj}
+          → (F : ((X , Y) , Z) 𝒞×𝒞×𝒞.⇒ ((X′ , Y′) , Z′))
+          → (+-assoc.from 𝒞.∘ [x+y]+z.₁ F)
+          ≈ (x+[y+z].₁ F 𝒞.∘ +-assoc.from)
+      commute {(X , Y) , Z} {(X′ , Y′) , Z′} ((F , G) , H) = sym +₁∘assocˡ
diff --git a/Category/Cartesian/Instance/SymMonCat.agda b/Category/Cartesian/Instance/SymMonCat.agda
new file mode 100644
index 0000000..7d91d52
--- /dev/null
+++ b/Category/Cartesian/Instance/SymMonCat.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+
+module Category.Cartesian.Instance.SymMonCat {o ℓ e : Level} where
+
+open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat)
+open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+
+SymMonCat-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+SymMonCat-CC = record
+    { U = SymMonCat
+    ; cartesian = SymMonCat-Cartesian
+    }
+
diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
index 74f434f..8af8633 100644
--- a/Category/Cocomplete/Finitely/Bundle.agda
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -28,6 +28,7 @@ record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
       ; monoidal = monoidal
       ; symmetric = symmetric
       }
+  {-# INJECTIVE_FOR_INFERENCE symmetricMonoidalCategory #-}
 
   cocartesianCategory : CocartesianCategory o ℓ e
   cocartesianCategory = record
diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
index 26813eb..2b66d19 100644
--- a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
+++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
@@ -4,11 +4,11 @@ open import Categories.Category.Core using (Category)
 
 module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where
 
-open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Category.Cocomplete.Finitely 𝒞 using (FinitelyCocomplete)
 open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
 
 
-module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete 𝒞) where
+module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete) where
 
   open FinitelyCocomplete finCo using (cocartesian)
   open CocartesianMonoidal cocartesian using (+-monoidal) public
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda
index 0847165..2766df2 100644
--- a/Category/Instance/FinitelyCocompletes.agda
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -62,6 +62,7 @@ _×_ 𝒞 𝒟 = record
   where
     module 𝒞 = FinitelyCocompleteCategory 𝒞
     module 𝒟 = FinitelyCocompleteCategory 𝒟
+{-# INJECTIVE_FOR_INFERENCE _×_ #-}
 
 module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
 
diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda
new file mode 100644
index 0000000..fa15295
--- /dev/null
+++ b/Category/Instance/Properties/SymMonCat.agda
@@ -0,0 +1,166 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Level using (Level; suc; _⊔_)
+module Category.Instance.Properties.SymMonCat {o ℓ e : Level} where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI
+import Categories.Functor.Monoidal.Symmetric {o} {o} {ℓ} {ℓ} {e} {e} as SMF
+
+open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat)
+
+open import Categories.Category using (Category; _[_≈_]; _[_∘_])
+open import Categories.Object.Product.Core SymMonCat using (Product)
+open import Categories.Object.Terminal SymMonCat using (Terminal)
+open import Categories.Category.Instance.One using (One)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Cartesian SymMonCat using (Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
+open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts)
+open import Categories.Functor.Monoidal.Construction.Product
+  using ()
+  renaming
+    ( πˡ-SymmetricMonoidalFunctor to πˡ-SMF
+    ; πʳ-SymmetricMonoidalFunctor to πʳ-SMF
+    ; ※-SymmetricMonoidalFunctor to ※-SMF
+    )
+open import Categories.Category.Monoidal.Construction.Product using (Product-SymmetricMonoidalCategory)
+open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+
+open SMF.Lax using (SymmetricMonoidalFunctor)
+open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
+
+module Cone
+  {A B X : SymmetricMonoidalCategory o ℓ e}
+  {F : SymmetricMonoidalFunctor X A}
+  {G : SymmetricMonoidalFunctor X B} where
+
+  module A = SymmetricMonoidalCategory A
+  module B = SymmetricMonoidalCategory B
+  module X = SymmetricMonoidalCategory X
+  module F = SymmetricMonoidalFunctor X A F
+  module G = SymmetricMonoidalFunctor X B G
+
+  A×B : SymmetricMonoidalCategory o ℓ e
+  A×B = (Product-SymmetricMonoidalCategory A B)
+
+  πˡ : SymmetricMonoidalFunctor A×B A
+  πˡ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+
+  πʳ : SymmetricMonoidalFunctor A×B B
+  πʳ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+
+  module _ where
+    open Category A.U
+    open Equiv
+    open ⇒-Reasoning A.U
+    open ⊗-Reasoning A.monoidal
+    project₁ : SymMonCat [ SymMonCat [ πˡ ∘ ※-SMF F G ] ≈ F ]
+    project₁ = record
+        { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F}
+        ; F⇒G-isMonoidal = record
+            { ε-compat = identityˡ ○ identityʳ
+            ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym A.⊗.identity }
+            }
+        }
+    module _ (H : SymmetricMonoidalFunctor X A×B) (eq₁ : SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]) where
+      private
+        module H = SymmetricMonoidalFunctor X A×B H
+      open SymmetricMonoidalNaturalIsomorphism eq₁
+      ε-compat₁ : ⇐.η X.unit A.∘ F.ε A.≈ H.ε .proj₁
+      ε-compat₁ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ
+      ⊗-homo-compat₁
+          : ∀ {C D}
+          → ⇐.η (X.⊗.₀ (C , D)) ∘ F.⊗-homo.η (C , D)
+          ≈ H.⊗-homo.η (C , D) .proj₁ ∘ A.⊗.₁ (⇐.η C , ⇐.η D)
+      ⊗-homo-compat₁ {C} {D} =
+          insertʳ
+              (sym ⊗-distrib-over-∘
+              ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D
+              ○ A.⊗.identity)
+          ○ (pullʳ (sym ⊗-homo-compat)
+            ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D)))
+            ○ identityʳ) ⟩∘⟨refl
+
+  module _ where
+    open Category B.U
+    open Equiv
+    open ⇒-Reasoning B.U
+    open ⊗-Reasoning B.monoidal
+    project₂ : SymMonCat [ SymMonCat [ πʳ ∘ ※-SMF F G ] ≈ G ]
+    project₂ = record
+        { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F}
+        ; F⇒G-isMonoidal = record
+            { ε-compat = identityˡ ○ identityʳ
+            ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym B.⊗.identity }
+            }
+        }
+    module _ (H : SymmetricMonoidalFunctor X A×B) (eq₂ : SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]) where
+      private
+        module H = SymmetricMonoidalFunctor X A×B H
+      open SymmetricMonoidalNaturalIsomorphism eq₂
+      ε-compat₂ : ⇐.η X.unit ∘ G.ε ≈ H.ε .proj₂
+      ε-compat₂ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ
+      ⊗-homo-compat₂
+          : ∀ {C D}
+          → ⇐.η (X.⊗.₀ (C , D)) ∘ G.⊗-homo.η (C , D)
+          ≈ H.⊗-homo.η (C , D) .proj₂ ∘ B.⊗.₁ (⇐.η C , ⇐.η D)
+      ⊗-homo-compat₂ {C} {D} =
+          insertʳ
+              (sym ⊗-distrib-over-∘
+              ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D
+              ○ B.⊗.identity)
+          ○ (pullʳ (sym ⊗-homo-compat)
+            ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D)))
+            ○ identityʳ) ⟩∘⟨refl
+
+  unique
+      : (H : SymmetricMonoidalFunctor X A×B)
+      → SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]
+      → SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]
+      → SymMonCat [ ※-SMF F G ≈ H ]
+  unique H eq₁ eq₂ = record
+      { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} {H.F} eq₁.U eq₂.U
+      ; F⇒G-isMonoidal = record
+          { ε-compat = ε-compat₁ H eq₁ , ε-compat₂ H eq₂
+          ; ⊗-homo-compat = ⊗-homo-compat₁ H eq₁ , ⊗-homo-compat₂ H eq₂
+          }
+      }
+    where
+      module H = SymmetricMonoidalFunctor X A×B H
+      module eq₁ = SymmetricMonoidalNaturalIsomorphism eq₁
+      module eq₂ = SymmetricMonoidalNaturalIsomorphism eq₂
+
+prod-SymMonCat : ∀ {A B} → Product A B
+prod-SymMonCat {A} {B} = record
+    { A×B = Product-SymmetricMonoidalCategory A B
+    ; π₁ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+    ; π₂ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B}
+    ; ⟨_,_⟩ = ※-SMF
+    ; project₁ = λ { {X} {f} {g} → Cone.project₁ {A} {B} {X} {f} {g} }
+    ; project₂ = λ { {X} {f} {g} → Cone.project₂ {A} {B} {X} {f} {g} }
+    ; unique = λ { {X} {h} {f} {g} eq₁ eq₂ → Cone.unique {A} {B} {X} {f} {g} h eq₁ eq₂ }
+    }
+
+SymMonCat-BinaryProducts : BinaryProducts
+SymMonCat-BinaryProducts = record { product = prod-SymMonCat }
+
+SymMonCat-Terminal : Terminal
+SymMonCat-Terminal = record
+    { ⊤ = record
+        { U = One
+        ; monoidal = _
+        ; symmetric = _
+        }
+    ; ⊤-is-terminal = _
+    }
+
+SymMonCat-Cartesian : Cartesian
+SymMonCat-Cartesian = record
+    { terminal = SymMonCat-Terminal
+    ; products = SymMonCat-BinaryProducts
+    }
diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda
new file mode 100644
index 0000000..e4b136c
--- /dev/null
+++ b/Category/Instance/SymMonCat.agda
@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Level using (Level; suc; _⊔_)
+module Category.Instance.SymMonCat {o ℓ e : Level} where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Functor.Monoidal.Symmetric as SMF
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Morphism as Morphism
+import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI
+import Categories.Category.Monoidal.Utilities as MonoidalUtil
+import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
+open import Relation.Binary.Core using (Rel)
+
+open import Categories.Category using (Category; _[_,_]; _[_∘_])
+open import Categories.Category.Helper using (categoryHelper)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
+
+open SMF.Lax using (SymmetricMonoidalFunctor)
+open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
+
+assoc
+    : {A B C D : SymmetricMonoidalCategory o ℓ e}
+      {F : SymmetricMonoidalFunctor A B}
+      {G : SymmetricMonoidalFunctor B C}
+      {H : SymmetricMonoidalFunctor C D}
+    → SymmetricMonoidalNaturalIsomorphism
+        (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F)
+        (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F))
+assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H}
+
+identityˡ
+    : {A B : SymmetricMonoidalCategory o ℓ e}
+      {F : SymmetricMonoidalFunctor A B}
+    → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F
+identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
+
+identityʳ
+    : {A B : SymmetricMonoidalCategory o ℓ e}
+      {F : SymmetricMonoidalFunctor A B}
+    → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F
+identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
+
+Compose
+    : {A B C : SymmetricMonoidalCategory o ℓ e}
+    → SymmetricMonoidalFunctor B C
+    → SymmetricMonoidalFunctor A B
+    → SymmetricMonoidalFunctor A C
+Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G
+
+∘-resp-≈
+    : {A B C : SymmetricMonoidalCategory o ℓ e}
+      {f h : SymmetricMonoidalFunctor B C}
+      {g i : SymmetricMonoidalFunctor A B}
+    → SymmetricMonoidalNaturalIsomorphism f h
+    → SymmetricMonoidalNaturalIsomorphism g i
+    → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i)
+∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′
+
+SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+SymMonCat = categoryHelper record
+    { Obj = SymmetricMonoidalCategory o ℓ e
+    ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e}
+    ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} }
+    ; id = λ { {X} → idF-SymmetricMonoidal X }
+    ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G }
+    ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} }
+    ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} }
+    ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} }
+    ; equiv = isEquivalence
+    ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i }
+    }
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