aboutsummaryrefslogtreecommitdiff
path: root/Category/Monoidal/Instance
diff options
context:
space:
mode:
Diffstat (limited to 'Category/Monoidal/Instance')
-rw-r--r--Category/Monoidal/Instance/Cospans.agda15
-rw-r--r--Category/Monoidal/Instance/Cospans/Lift.agda15
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans.agda410
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans/Lift.agda114
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans/Products.agda104
-rw-r--r--Category/Monoidal/Instance/Nat.agda71
6 files changed, 714 insertions, 15 deletions
diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda
index 228ddea..a1648db 100644
--- a/Category/Monoidal/Instance/Cospans.agda
+++ b/Category/Monoidal/Instance/Cospans.agda
@@ -18,8 +18,9 @@ open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Functor using (Functor)
open import Categories.Functor.Properties using ([_]-resp-β‰…)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
-open import Category.Instance.Cospans π’ž using (Cospans; Cospan)
-open import Category.Instance.Properties.FinitelyCocompletes {o} {β„“} {e} using (FinitelyCocompletes-CC)
+open import Category.Instance.Cospans π’ž using (Cospans)
+open import Category.Diagram.Cospan using (Cospan; cospan)
+open import Category.Cartesian.Instance.FinitelyCocompletes {o} {β„“} {e} using (FinitelyCocompletes-CC)
open import Category.Monoidal.Instance.Cospans.Lift {o} {β„“} {e} using (module Square)
open import Data.Product.Base using (_,_)
open import Functor.Instance.Cospan.Stack π’ž using (βŠ—)
@@ -61,7 +62,6 @@ CospansMonoidal = record
; pentagon = pentagon
}
where
- module βŠ— = Functor βŠ—
module Cospans = Category Cospans
module UnitorΛ‘ = Square βŠ₯+--id
module UnitorΚ³ = Square -+βŠ₯-id
@@ -83,16 +83,15 @@ CospansMonoidal = record
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 { f₁ = f₁ f , f₁ g ; fβ‚‚ = fβ‚‚ f , fβ‚‚ g }) }
- ; iso = λ { (X , Y) → Braiding.FX≅GX′.iso {X , Y} }
+ { η = λ (X , Y) → Braiding.FX≅GX′.from {X , Y}
+ ; η⁻¹ = Ξ» (Y , X) β†’ Braiding.FXβ‰…GXβ€².to {Y , X}
+ ; commute = Ξ» (cospan f₁ fβ‚‚ , cospan g₁ gβ‚‚) β†’ Braiding.from (cospan (f₁ , g₁) (fβ‚‚ , gβ‚‚))
+ ; iso = λ (X , Y) → Braiding.FX≅GX′.iso {X , Y}
}
; hexagon₁ = sym L-resp-βŠ— ⟩∘⟨ refl ⟩∘⟨ sym L-resp-βŠ— β—‹ refl⟩∘⟨ sym homomorphism β—‹ sym homomorphism β—‹ L-resp-β‰ˆ hex₁ β—‹ homomorphism β—‹ refl⟩∘⟨ homomorphism
; hexagonβ‚‚ = sym L-resp-βŠ— ⟩∘⟨refl ⟩∘⟨ sym L-resp-βŠ— β—‹ sym homomorphism ⟩∘⟨refl β—‹ sym homomorphism β—‹ L-resp-β‰ˆ hexβ‚‚ β—‹ homomorphism β—‹ homomorphism ⟩∘⟨refl
}
where
- open Cospan
module Cospans = Category Cospans
open Cospans.Equiv
open Cospans.HomReasoning
diff --git a/Category/Monoidal/Instance/Cospans/Lift.agda b/Category/Monoidal/Instance/Cospans/Lift.agda
index fa31fcb..c7e7516 100644
--- a/Category/Monoidal/Instance/Cospans/Lift.agda
+++ b/Category/Monoidal/Instance/Cospans/Lift.agda
@@ -4,7 +4,7 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor
module Category.Monoidal.Instance.Cospans.Lift {o β„“ e} where
-open import Category.Instance.Cospans using (Cospans; Cospan; Same)
+open import Category.Instance.Cospans using (Cospans)
open import Categories.Category.Core using (Category)
@@ -16,6 +16,7 @@ import Category.Diagram.Pushout as PushoutDiagramβ€²
import Functor.Instance.Cospan.Embed as CospanEmbed
open import Categories.Category using (_[_,_]; _[_β‰ˆ_]; _[_∘_]; module Definitions)
+open import Category.Diagram.Cospan using (Cospan; cospan)
open import Categories.Functor.Core using (Functor)
open import Categories.Functor.Properties using ([_]-resp-β‰…)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_)
@@ -26,7 +27,7 @@ module _ {π’ž : FinitelyCocompleteCategory o β„“ e} {π’Ÿ : FinitelyCocompleteC
module π’ž = FinitelyCocompleteCategory π’ž
module π’Ÿ = FinitelyCocompleteCategory π’Ÿ
- open CospanEmbed π’Ÿ using (L; B₁; B∘L; R∘B; β‰…-L-R)
+ open CospanEmbed π’Ÿ using (L; B∘L; R∘B; β‰…-L-R)
module Square {F G : Functor π’ž.U π’Ÿ.U} (F≃G : F ≃ G) where
@@ -51,21 +52,21 @@ module _ {π’ž : FinitelyCocompleteCategory o β„“ e} {π’Ÿ : FinitelyCocompleteC
open Cospan fg renaming (f₁ to f; fβ‚‚ to g)
open π’Ÿ using (_∘_)
- squaresβ‡’cospan : Cospans π’Ÿ [ B₁ (G.₁ f ∘ FXβ‰…GX.from) (G.₁ g ∘ FXβ‰…GX.from) β‰ˆ B₁ (F.₁ f) (F.₁ g) ]
+ squaresβ‡’cospan : Cospans π’Ÿ [ cospan (G.₁ f ∘ FXβ‰…GX.from) (G.₁ g ∘ FXβ‰…GX.from) β‰ˆ cospan (F.₁ f) (F.₁ g) ]
squares⇒cospan = record
{ β‰…N = β‰….sym π’Ÿ.U FXβ‰…GX
- ; from∘fβ‚β‰ˆf₁′ = sym (switch-fromtoΛ‘ FXβ‰…GX (β‡’.commute f))
- ; from∘fβ‚‚β‰ˆfβ‚‚β€² = sym (switch-fromtoΛ‘ FXβ‰…GX (β‡’.commute g))
+ ; from∘fβ‚β‰ˆf₁ = sym (switch-fromtoΛ‘ FXβ‰…GX (β‡’.commute f))
+ ; from∘fβ‚‚β‰ˆfβ‚‚ = sym (switch-fromtoΛ‘ FXβ‰…GX (β‡’.commute g))
}
where
open π’Ÿ.Equiv using (sym)
- from : Cospans π’Ÿ [ Cospans π’Ÿ [ L.₁ (β‡’.Ξ· Y) ∘ B₁ (F.₁ f) (F.₁ g) ] β‰ˆ Cospans π’Ÿ [ B₁ (G.₁ f) (G.₁ g) ∘ L.₁ (β‡’.Ξ· X) ] ]
+ from : Cospans π’Ÿ [ Cospans π’Ÿ [ L.₁ (β‡’.Ξ· Y) ∘ cospan (F.₁ f) (F.₁ g) ] β‰ˆ Cospans π’Ÿ [ cospan (G.₁ f) (G.₁ g) ∘ 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)
- to : Cospans π’Ÿ [ Cospans π’Ÿ [ L.₁ (⇐.Ξ· Y) ∘ B₁ (G.₁ f) (G.₁ g) ] β‰ˆ Cospans π’Ÿ [ B₁ (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.Ξ· X) ] ]
+ to : Cospans π’Ÿ [ Cospans π’Ÿ [ L.₁ (⇐.Ξ· Y) ∘ cospan (G.₁ f) (G.₁ g) ] β‰ˆ Cospans π’Ÿ [ cospan (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.Ξ· X) ] ]
to = switch-fromtoΚ³ FXβ‰…GXβ€² (pullΚ³ B∘L β—‹ β‰…-L-R FXβ‰…GX ⟩∘⟨refl β—‹ R∘B β—‹ squaresβ‡’cospan)
where
open β‡’-Reasoning (Cospans π’Ÿ) using (pullΚ³)
diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda
new file mode 100644
index 0000000..3df57ee
--- /dev/null
+++ b/Category/Monoidal/Instance/DecoratedCospans.agda
@@ -0,0 +1,410 @@
+{-# 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 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 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 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 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 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 βŠ—-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 βŠ—-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 βŠ—-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 βŠ—-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 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
+ 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..c75f0db
--- /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)
+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
diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda
new file mode 100644
index 0000000..24b30a6
--- /dev/null
+++ b/Category/Monoidal/Instance/Nat.agda
@@ -0,0 +1,71 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Monoidal.Instance.Nat where
+
+open import Level using (0β„“)
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
+open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian)
+
+import Categories.Category.Cartesian.SymmetricMonoidal as CartesianSymmetricMonoidal
+
+Natop-Cartesian : Cartesian Natop
+Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian
+
+Natop-Cocartesian : Cocartesian Natop
+Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian
+
+module Monoidal where
+
+ open MonoidalCategory
+ open CartesianMonoidal using () renaming (monoidal to Γ—-monoidal)
+ open CocartesianMonoidal using (+-monoidal)
+
+ Nat,+,0 : MonoidalCategory 0β„“ 0β„“ 0β„“
+ Nat,+,0 .U = Nat
+ Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian
+
+ Nat,Γ—,1 : MonoidalCategory 0β„“ 0β„“ 0β„“
+ Nat,Γ—,1 .U = Nat
+ Nat,Γ—,1 .monoidal = Γ—-monoidal Nat-Cartesian
+
+ Natop,+,0 : MonoidalCategory 0β„“ 0β„“ 0β„“
+ Natop,+,0 .U = Natop
+ Natop,+,0 .monoidal = Γ—-monoidal Natop-Cartesian
+
+ Natop,Γ—,1 : MonoidalCategory 0β„“ 0β„“ 0β„“
+ Natop,Γ—,1 .U = Natop
+ Natop,Γ—,1 .monoidal = +-monoidal Natop Natop-Cocartesian
+
+module Symmetric where
+
+ open SymmetricMonoidalCategory
+ open CartesianMonoidal using () renaming (monoidal to Γ—-monoidal)
+ open CocartesianMonoidal using (+-monoidal)
+ open CartesianSymmetricMonoidal using () renaming (symmetric to Γ—-symmetric)
+ open CocartesianSymmetricMonoidal using (+-symmetric)
+
+ Nat,+,0 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“
+ Nat,+,0 .U = Nat
+ Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian
+ Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian
+
+ Nat,Γ—,1 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“
+ Nat,Γ—,1 .U = Nat
+ Nat,Γ—,1 .monoidal = Γ—-monoidal Nat-Cartesian
+ Nat,Γ—,1 .symmetric = Γ—-symmetric Nat Nat-Cartesian
+
+ Natop,+,0 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“
+ Natop,+,0 .U = Natop
+ Natop,+,0 .monoidal = Γ—-monoidal Natop-Cartesian
+ Natop,+,0 .symmetric = Γ—-symmetric Natop Natop-Cartesian
+
+ Natop,Γ—,1 : SymmetricMonoidalCategory 0β„“ 0β„“ 0β„“
+ Natop,Γ—,1 .U = Natop
+ Natop,Γ—,1 .monoidal = +-monoidal Natop Natop-Cocartesian
+ Natop,Γ—,1 .symmetric = +-symmetric Natop Natop-Cocartesian
+
+open Symmetric public
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 03:36:14 +0000