aboutsummaryrefslogtreecommitdiff
path: root/Category/Monoidal
diff options
context:
space:
mode:
Diffstat (limited to 'Category/Monoidal')
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans.agda415
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans/Lift.agda114
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans/Products.agda104
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-06-16 17:16:41 +0000