diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/Cartesian/Instance/FinitelyCocompletes.agda (renamed from Category/Instance/Properties/FinitelyCocompletes.agda) | 44 | ||||
| -rw-r--r-- | Category/Cartesian/Instance/SymMonCat.agda | 16 | ||||
| -rw-r--r-- | Category/Cocomplete/Finitely/Bundle.agda | 1 | ||||
| -rw-r--r-- | Category/Cocomplete/Finitely/SymmetricMonoidal.agda | 4 | ||||
| -rw-r--r-- | Category/Instance/FinitelyCocompletes.agda | 1 | ||||
| -rw-r--r-- | Category/Instance/Properties/SymMonCat.agda | 166 | ||||
| -rw-r--r-- | Category/Instance/SymMonCat.agda | 74 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans.agda | 415 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans/Lift.agda | 114 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans/Products.agda | 104 |
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 |