diff options
16 files changed, 1852 insertions, 9 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 diff --git a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda new file mode 100644 index 0000000..346999b --- /dev/null +++ b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -0,0 +1,169 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level) + +module Functor.Cartesian.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o ℓ e : Level} where + +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Category.Monoidal.Utilities as ⊗-Util + +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Category.Product using (_※_) +open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u) +open import Categories.Functor.Core using (Functor) +open import Categories.Functor.Cartesian using (CartesianF) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.NaturalTransformation.Core using (ntHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using (module Lax) +open import Categories.Object.Product using (IsProduct) +open import Categories.Object.Terminal using (IsTerminal) +open import Data.Product.Base using (_,_; <_,_>; proj₁; proj₂) + +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC) +open import Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using () renaming (Underlying to U) + +module CartesianCategory′ {o ℓ e : Level} (C : CartesianCategory o ℓ e) where + module CC = CartesianCategory C + open import Categories.Object.Terminal using (Terminal) + open Terminal CC.terminal public + open import Categories.Category.BinaryProducts using (BinaryProducts) + open BinaryProducts CC.products public + open CC public + +module FC = CartesianCategory′ FinitelyCocompletes-CC +module SMC = CartesianCategory′ SymMonCat-CC +module U = Functor U + +F-resp-⊤ : IsTerminal SMC.U (U.₀ FC.⊤) +F-resp-⊤ = _ + +F-resp-× : {A B : FC.Obj} → IsProduct SMC.U (U.₁ (FC.π₁ {A} {B})) (U.₁ (FC.π₂ {A} {B})) +F-resp-× {A} {B} = record + { ⟨_,_⟩ = pairing + ; project₁ = λ { {C} {F} {G} → project₁ {C} F G } + ; project₂ = λ { {C} {F} {G} → project₂ {C} F G } + ; unique = λ { {C} {H} {F} {G} ≃₁ ≃₂ → unique {C} F G H ≃₁ ≃₂ } + } + where + module _ {C : SMC.Obj} (F : Lax.SymmetricMonoidalFunctor C (U.₀ A)) (G : Lax.SymmetricMonoidalFunctor C (U.₀ B)) where + module F = Lax.SymmetricMonoidalFunctor F + module G = Lax.SymmetricMonoidalFunctor G + pairing : Lax.SymmetricMonoidalFunctor C (U.₀ (A FC.× B)) + pairing = record + { F = F.F ※ G.F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = F.ε , G.ε + ; ⊗-homo = ntHelper record + { η = < F.⊗-homo.η , G.⊗-homo.η > + ; commute = < F.⊗-homo.commute , G.⊗-homo.commute > + } + ; associativity = F.associativity , G.associativity + ; unitaryˡ = F.unitaryˡ , G.unitaryˡ + ; unitaryʳ = F.unitaryʳ , G.unitaryʳ + } + ; braiding-compat = F.braiding-compat , G.braiding-compat + } + } + module pairing = Lax.SymmetricMonoidalFunctor pairing + module A = FinitelyCocompleteCategory A + module B = FinitelyCocompleteCategory B + module C = SymmetricMonoidalCategory C + module A′ = SymmetricMonoidalCategory (U.₀ A) + module B′ = SymmetricMonoidalCategory (U.₀ B) + project₁ : Lax.SymmetricMonoidalNaturalIsomorphism ((U.₁ (FC.π₁ {A} {B})) SMC.∘ pairing) F + project₁ = record + { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {C.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = ¡-unique₂ (id ∘ F.ε ∘ ¡) F.ε + ; ⊗-homo-compat = λ { {X} {Y} → identityˡ ○ refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ) } + } + } + where + open FinitelyCocompleteCategory A + open HomReasoning + open Equiv + open ⇒-Reasoning A.U + project₂ : Lax.SymmetricMonoidalNaturalIsomorphism (U.₁ {A FC.× B} {B} FC.π₂ SMC.∘ pairing) G + project₂ = record + { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {C.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = ¡-unique₂ (id ∘ G.ε ∘ ¡) G.ε + ; ⊗-homo-compat = λ { {X} {Y} → identityˡ ○ refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ) } + } + } + where + open FinitelyCocompleteCategory B + open HomReasoning + open Equiv + open ⇒-Reasoning B.U + unique + : (H : Lax.SymmetricMonoidalFunctor C (U.F₀ (A FC.× B))) + → Lax.SymmetricMonoidalNaturalIsomorphism (U.₁ {A FC.× B} {A} FC.π₁ SMC.∘ H) F + → Lax.SymmetricMonoidalNaturalIsomorphism (U.₁ {A FC.× B} {B} FC.π₂ SMC.∘ H) G + → Lax.SymmetricMonoidalNaturalIsomorphism pairing H + unique H ≃₁ ≃₂ = record + { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {C.U} {F.F} {G.F} {H.F} ≃₁.U ≃₂.U + ; F⇒G-isMonoidal = record + { ε-compat = ε-compat₁ , ε-compat₂ + ; ⊗-homo-compat = + λ { {X} {Y} → ⊗-homo-compat₁ {X} {Y} , ⊗-homo-compat₂ {X} {Y} } + } + } + where + module H = Lax.SymmetricMonoidalFunctor H + module ≃₁ = Lax.SymmetricMonoidalNaturalIsomorphism ≃₁ + module ≃₂ = Lax.SymmetricMonoidalNaturalIsomorphism ≃₂ + ε-compat₁ : ≃₁.⇐.η C.unit A.∘ F.ε A.≈ proj₁ H.ε + ε-compat₁ = refl⟩∘⟨ sym ≃₁.ε-compat ○ cancelˡ (≃₁.iso.isoˡ C.unit) ○ ¡-unique₂ (proj₁ H.ε ∘ ¡) (proj₁ H.ε) + where + open A + open HomReasoning + open ⇒-Reasoning A.U + open Equiv + ε-compat₂ : ≃₂.⇐.η C.unit B.∘ G.ε B.≈ proj₂ H.ε + ε-compat₂ = refl⟩∘⟨ sym ≃₂.ε-compat ○ cancelˡ (≃₂.iso.isoˡ C.unit) ○ ¡-unique₂ (proj₂ H.ε ∘ ¡) (proj₂ H.ε) + where + open B + open HomReasoning + open ⇒-Reasoning B.U + open Equiv + ⊗-homo-compat₁ + : {X Y : C.Obj} + → ≃₁.⇐.η (C.⊗.₀ (X , Y)) + A.∘ F.⊗-homo.η (X , Y) + A.≈ proj₁ (H.⊗-homo.η (X , Y)) + A.∘ (≃₁.⇐.η X A.+₁ ≃₁.⇐.η Y) + ⊗-homo-compat₁ {X} {Y} = switch-fromtoʳ (≃₁.FX≅GX ⊗ᵢ ≃₁.FX≅GX) (assoc ○ sym (switch-fromtoˡ ≃₁.FX≅GX (refl⟩∘⟨ introʳ A.+-η ○ ≃₁.⊗-homo-compat))) + where + open A + open HomReasoning + open Equiv + open ⇒-Reasoning A.U + open ⊗-Util A′.monoidal + ⊗-homo-compat₂ + : {X Y : C.Obj} + → ≃₂.⇐.η (C.⊗.₀ (X , Y)) + B.∘ G.⊗-homo.η (X , Y) + B.≈ proj₂ (H.⊗-homo.η (X , Y)) + B.∘ (≃₂.⇐.η X B.+₁ ≃₂.⇐.η Y) + ⊗-homo-compat₂ = switch-fromtoʳ (≃₂.FX≅GX ⊗ᵢ ≃₂.FX≅GX) (assoc ○ sym (switch-fromtoˡ ≃₂.FX≅GX (refl⟩∘⟨ introʳ B.+-η ○ ≃₂.⊗-homo-compat))) + where + open B + open HomReasoning + open Equiv + open ⇒-Reasoning B.U + open ⊗-Util B′.monoidal + +Underlying : CartesianF FinitelyCocompletes-CC SymMonCat-CC +Underlying = record + { F = U + ; isCartesian = record + { F-resp-⊤ = F-resp-⊤ + ; F-resp-× = F-resp-× + } + } diff --git a/Functor/Exact/Instance/Swap.agda b/Functor/Exact/Instance/Swap.agda new file mode 100644 index 0000000..99a27c5 --- /dev/null +++ b/Functor/Exact/Instance/Swap.agda @@ -0,0 +1,79 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +module Functor.Exact.Instance.Swap {o ℓ e : Level} (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where + +open import Categories.Category using (_[_,_]) +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Product using (Product) renaming (Swap to Swap′) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Diagram.Coequalizer using (IsCoequalizer) +open import Categories.Object.Initial using (IsInitial) +open import Categories.Object.Coproduct using (IsCoproduct) +open import Data.Product.Base using (_,_; proj₁; proj₂; swap) + +open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-Cartesian) +open import Functor.Exact using (RightExactFunctor) + +module FCC = Cartesian FinitelyCocompletes-Cartesian +open BinaryProducts (FCC.products) using (_×_) -- ; π₁; π₂; _⁂_; assocˡ) + + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = FinitelyCocompleteCategory 𝒟 + +swap-resp-⊥ : {A : 𝒞.Obj} {B : 𝒟.Obj} → IsInitial (Product 𝒞.U 𝒟.U) (A , B) → IsInitial (Product 𝒟.U 𝒞.U) (B , A) +swap-resp-⊥ {A} {B} isInitial = record + { ! = swap ! + ; !-unique = λ { (f , g) → swap (!-unique (g , f)) } + } + where + open IsInitial isInitial + +swap-resp-+ + : {A₁ B₁ A+B₁ : 𝒞.Obj} + → {A₂ B₂ A+B₂ : 𝒟.Obj} + → {i₁₁ : 𝒞.U [ A₁ , A+B₁ ]} + → {i₂₁ : 𝒞.U [ B₁ , A+B₁ ]} + → {i₁₂ : 𝒟.U [ A₂ , A+B₂ ]} + → {i₂₂ : 𝒟.U [ B₂ , A+B₂ ]} + → IsCoproduct (Product 𝒞.U 𝒟.U) (i₁₁ , i₁₂) (i₂₁ , i₂₂) + → IsCoproduct (Product 𝒟.U 𝒞.U) (i₁₂ , i₁₁) (i₂₂ , i₂₁) +swap-resp-+ {A₁} {B₁} {A+B₁} {A₂} {B₂} {A+B₂} {i₁₁} {i₂₁} {i₁₂} {i₂₂} isCoproduct = record + { [_,_] = λ { X Y → swap ([ swap X , swap Y ]) } + ; inject₁ = swap inject₁ + ; inject₂ = swap inject₂ + ; unique = λ { ≈₁ ≈₂ → swap (unique (swap ≈₁) (swap ≈₂)) } + } + where + open IsCoproduct isCoproduct + +swap-resp-coeq + : {A₁ B₁ C₁ : 𝒞.Obj} + {A₂ B₂ C₂ : 𝒟.Obj} + {f₁ g₁ : 𝒞.U [ A₁ , B₁ ]} + {h₁ : 𝒞.U [ B₁ , C₁ ]} + {f₂ g₂ : 𝒟.U [ A₂ , B₂ ]} + {h₂ : 𝒟.U [ B₂ , C₂ ]} + → IsCoequalizer (Product 𝒞.U 𝒟.U) (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) + → IsCoequalizer (Product 𝒟.U 𝒞.U) (f₂ , f₁) (g₂ , g₁) (h₂ , h₁) +swap-resp-coeq isCoequalizer = record + { equality = swap equality + ; coequalize = λ { x → swap (coequalize (swap x)) } + ; universal = swap universal + ; unique = λ { x → swap (unique (swap x)) } + } + where + open IsCoequalizer isCoequalizer + +Swap : RightExactFunctor (𝒞 × 𝒟) (𝒟 × 𝒞) +Swap = record + { F = Swap′ + ; isRightExact = record + { F-resp-⊥ = swap-resp-⊥ + ; F-resp-+ = swap-resp-+ + ; F-resp-coeq = swap-resp-coeq + } + } diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda index b7664dc..03cca1f 100644 --- a/Functor/Instance/Cospan/Stack.agda +++ b/Functor/Instance/Cospan/Stack.agda @@ -13,7 +13,7 @@ open import Categories.Category.Core using (Category) open import Categories.Functor.Bifunctor using (Bifunctor) open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same; id-Cospan; compose) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using () renaming (_×_ to _×′_) -open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout) open import Level using (Level; _⊔_; suc) diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda new file mode 100644 index 0000000..e87f20c --- /dev/null +++ b/Functor/Instance/Decorate.agda @@ -0,0 +1,168 @@ +{-# OPTIONS --without-K --safe #-} + +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 Data.Product.Base using (_,_) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module Functor.Instance.Decorate + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Functor.Core using (Functor) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Function.Base using () renaming (id to idf) +open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same) +open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) +open import Functor.Instance.Cospan.Stack using (⊗) +open import Functor.Instance.DecoratedCospan.Stack using () renaming (⊗ to ⊗′) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 +module F = SymmetricMonoidalFunctor F +module Cospans = Category Cospans +module DecoratedCospans = Category DecoratedCospans +module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian + +-- For every cospan there exists a free decorated cospan +-- i.e. the original cospan with the empty decoration + +private + variable + A A′ B B′ C C′ D : 𝒞.Obj + f : Cospans [ A , B ] + g : Cospans [ C , D ] + +decorate : Cospans [ A , B ] → DecoratedCospans [ A , B ] +decorate f = record + { cospan = f + ; decoration = F₁ ¡ ∘ ε + } + where + open 𝒞 using (¡) + open 𝒟 using (_∘_) + open F using (ε; F₁) + +identity : DecoratedCospans [ decorate (Cospans.id {A}) ≈ DecoratedCospans.id ] +identity = record + { cospans-≈ = Cospans.Equiv.refl + ; same-deco = elimˡ F.identity + } + where + open ⇒-Reasoning 𝒟.U + +homomorphism : DecoratedCospans [ decorate (Cospans [ g ∘ f ]) ≈ DecoratedCospans [ decorate g ∘ decorate f ] ] +homomorphism {B} {C} {g} {A} {f} = record + { cospans-≈ = Cospans.Equiv.refl + ; same-deco = same-deco + } + where + + open Cospan f using (N; f₂) + open Cospan g using () renaming (N to M; f₁ to g₁) + + open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + + open DiagramPushout 𝒞.U using (Pushout) + open Pushout (pushout f₂ g₁) using (i₁; i₂) + open mc𝒞 using (unitorˡ) + open unitorˡ using () renaming (to to λ⇐′) + + same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ F.ε ≈ F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ + same-deco = begin + F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈⟨ elimˡ F.identity ⟩ + F₁ ¡ ∘ ε ≈⟨ F.F-resp-≈ (¡-unique _) ⟩∘⟨refl ⟩ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ≈⟨ refl⟩∘⟨ introʳ λ-.isoʳ ⟩ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ F.homomorphism ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ push-center (sym F.homomorphism) ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , ¡)) ⟨ + F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ + F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ∎ + +F-resp-≈ : Cospans [ f ≈ g ] → DecoratedCospans [ decorate f ≈ decorate g ] +F-resp-≈ f≈g = record + { cospans-≈ = f≈g + ; same-deco = pullˡ (sym F.homomorphism) ○ sym (F.F-resp-≈ (¡-unique _)) ⟩∘⟨refl + } + where + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + open 𝒟.HomReasoning + open 𝒞 using (¡-unique) + +Decorate : Functor Cospans DecoratedCospans +Decorate = record + { F₀ = idf + ; F₁ = decorate + ; identity = identity + ; homomorphism = homomorphism + ; F-resp-≈ = F-resp-≈ + } + +module ⊗ = Functor (⊗ 𝒞) +module ⊗′ = Functor (⊗′ 𝒞 F) +open 𝒞 using (_+₁_) + +Decorate-resp-⊗ : DecoratedCospans [ decorate (⊗.₁ (f , g)) ≈ ⊗′.₁ (decorate f , decorate g) ] +Decorate-resp-⊗ {f = f} {g = g} = record + { cospans-≈ = Cospans.Equiv.refl + ; same-deco = same-deco + } + where + + open Cospan f using (N) + open Cospan g using () renaming (N to M) + + open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + open mc𝒞 using (unitorˡ) + open unitorˡ using () renaming (to to λ⇐′) + + same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ + same-deco = begin + F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈⟨ elimˡ F.identity ⟩ + F₁ ¡ ∘ ε ≈⟨ F.F-resp-≈ (¡-unique _) ⟩∘⟨refl ⟩ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ≈⟨ refl⟩∘⟨ introʳ λ-.isoʳ ⟩ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ F.homomorphism ⟩ + F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨ + F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩ + F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ extendʳ (φ-commute (¡ , ¡)) ⟨ + φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ + φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ∎ + diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda new file mode 100644 index 0000000..4595a8f --- /dev/null +++ b/Functor/Instance/DecoratedCospan/Embed.agda @@ -0,0 +1,275 @@ +{-# OPTIONS --without-K --safe #-} + +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 Functor.Instance.DecoratedCospan.Embed + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Category.Diagram.Pushout as Pushout′ +import Functor.Instance.Cospan.Embed 𝒞 as Embed + +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) + +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism as Morphism + +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Functor using (Functor; _∘F_) +open import Data.Product.Base using (_,_) +open import Function.Base using () renaming (id to idf) +open import Functor.Instance.DecoratedCospan.Stack using (⊗) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 +module F = SymmetricMonoidalFunctor F +module Cospans = Category Cospans +module DecoratedCospans = Category DecoratedCospans +module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian + +open import Functor.Instance.Decorate 𝒞 F using (Decorate; Decorate-resp-⊗) + +private + variable + A B C D E H : 𝒞.Obj + f : 𝒞.U [ A , B ] + g : 𝒞.U [ C , D ] + h : 𝒞.U [ E , H ] + +L : Functor 𝒞.U DecoratedCospans +L = Decorate ∘F Embed.L + +R : Functor 𝒞.op DecoratedCospans +R = Decorate ∘F Embed.R + +B₁ : 𝒞.U [ A , C ] → 𝒞.U [ B , C ] → 𝒟.U [ 𝒟.unit , F.F₀ C ] → DecoratedCospans [ A , B ] +B₁ f g s = record + { cospan = Embed.B₁ f g + ; decoration = s + } + +module _ where + + module L = Functor L + module R = Functor R + + module Codiagonal where + + open mc𝒞 using (unitorˡ; unitorʳ; +-monoidal) public + open unitorˡ using () renaming (to to λ⇐′) public + open unitorʳ using () renaming (to to ρ⇐′) public + open 𝒞 using (U; _+_; []-cong₂; []∘+₁; ∘-distribˡ-[]; inject₁; inject₂; ¡) + renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open HomReasoning + open ⇒-Reasoning 𝒞.U + + μ : {X : Obj} → X + X ⇒ X + μ = [ id , id ]′ + + μ∘+ : {X Y Z : Obj} {f : X ⇒ Z} {g : Y ⇒ Z} → [ f , g ]′ ≈ μ ∘ f +₁ g + μ∘+ = []-cong₂ (sym identityˡ) (sym identityˡ) ○ sym []∘+₁ + + μ∘¡ˡ : {X : Obj} → μ ∘ ¡ +₁ id ∘ λ⇐′ ≈ id {X} + μ∘¡ˡ = begin + μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩ + [ ¡ , id ]′ ∘ λ⇐′ ≈⟨ inject₂ ⟩ + id ∎ + + μ∘¡ʳ : {X : Obj} → μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈ id {X} + μ∘¡ʳ = begin + μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩ + [ id , ¡ ]′ ∘ ρ⇐′ ≈⟨ inject₁ ⟩ + id ∎ + + + μ-natural : {X Y : Obj} {f : X ⇒ Y} → f ∘ μ ≈ μ ∘ f +₁ f + μ-natural = ∘-distribˡ-[] ○ []-cong₂ (identityʳ ○ sym identityˡ) (identityʳ ○ sym identityˡ) ○ sym []∘+₁ + + B∘L : {A B M C : 𝒞.Obj} + → {f : 𝒞.U [ A , B ]} + → {g : 𝒞.U [ B , M ]} + → {h : 𝒞.U [ C , M ]} + → {s : 𝒟.U [ 𝒟.unit , F.₀ M ]} + → DecoratedCospans [ DecoratedCospans [ B₁ g h s ∘ L.₁ f ] ≈ B₁ (𝒞.U [ g ∘ f ]) h s ] + B∘L {A} {B} {M} {C} {f} {g} {h} {s} = record + { cospans-≈ = Embed.B∘L + ; same-deco = same-deco + } + where + + module _ where + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open 𝒞 using (U) + open Category U + open mc𝒞 using (unitorˡ; unitorˡ-commute-to; +-monoidal) public + open unitorˡ using () renaming (to to λ⇐′) public + open ⊗-Reasoning +-monoidal + open ⇒-Reasoning 𝒞.U + open Equiv + + open Pushout′ 𝒞.U using (pushout-id-g) + open PushoutProperties 𝒞.U using (up-to-iso) + open DiagramPushout 𝒞.U using (Pushout) + P P′ : Pushout 𝒞.id g + P = pushout 𝒞.id g + P′ = pushout-id-g + module P = Pushout P + module P′ = Pushout P′ + open Morphism 𝒞.U using (_≅_) + open _≅_ using (from) + open P using (i₁ ; i₂; universal∘i₂≈h₂) public + + open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ˡ) + + ≅ : P.Q ⇒ M + ≅ = up-to-iso P P′ .from + + ≅∘[]∘¡+id : ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈ id + ≅∘[]∘¡+id = begin + ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈⟨ assoc²αε ⟩ + ≅ ∘ [ i₁ , i₂ ]′ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩ + ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ refl⟩∘⟨ pull-center (sym split₁ʳ) ⟩ + ≅ ∘ μ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′ ≈⟨ extendʳ μ-natural ⟩ + μ ∘ ≅ +₁ ≅ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩ + μ ∘ (≅ ∘ i₁ ∘ ¡) +₁ (≅ ∘ i₂) ∘ λ⇐′ ≈⟨ refl⟩∘⟨ sym (¡-unique (≅ ∘ i₁ ∘ ¡)) ⟩⊗⟨ universal∘i₂≈h₂ ⟩∘⟨refl ⟩ + μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ μ∘¡ˡ ⟩ + id ∎ + + open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + + same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s + same-deco = begin + F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ id ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym F.identity ⟩∘⟨refl ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ F₁ 𝒞.id ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , 𝒞.id)) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟨ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ λ-.isoʳ) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘¡+id ○ F.identity) ⟩ + s ∎ + + R∘B : {A N B C : 𝒞.Obj} + → {f : 𝒞.U [ A , N ]} + → {g : 𝒞.U [ B , N ]} + → {h : 𝒞.U [ C , B ]} + → {s : 𝒟.U [ 𝒟.unit , F.₀ N ]} + → DecoratedCospans [ DecoratedCospans [ R.₁ h ∘ B₁ f g s ] ≈ B₁ f (𝒞.U [ g ∘ h ]) s ] + R∘B {A} {N} {B} {C} {f} {g} {h} {s} = record + { cospans-≈ = Embed.R∘B + ; same-deco = same-deco + } + where + + module _ where + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open 𝒞 using (U) + open Category U + open mc𝒞 using (unitorʳ; unitorˡ; unitorˡ-commute-to; +-monoidal) public + open unitorˡ using () renaming (to to λ⇐′) public + open unitorʳ using () renaming (to to ρ⇐′) public + open ⊗-Reasoning +-monoidal + open ⇒-Reasoning 𝒞.U + open Equiv + + open Pushout′ 𝒞.U using (pushout-f-id) + open PushoutProperties 𝒞.U using (up-to-iso) + open DiagramPushout 𝒞.U using (Pushout) + P P′ : Pushout g 𝒞.id + P = pushout g 𝒞.id + P′ = pushout-f-id + module P = Pushout P + module P′ = Pushout P′ + open Morphism 𝒞.U using (_≅_) + open _≅_ using (from) + open P using (i₁ ; i₂; universal∘i₁≈h₁) public + + open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ʳ) + + ≅ : P.Q ⇒ N + ≅ = up-to-iso P P′ .from + + ≅∘[]∘id+¡ : ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈ id + ≅∘[]∘id+¡ = begin + ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈⟨ assoc²αε ⟩ + ≅ ∘ [ i₁ , i₂ ]′ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩ + ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ pull-center merge₂ʳ ⟩ + ≅ ∘ μ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ extendʳ μ-natural ⟩ + μ ∘ ≅ +₁ ≅ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩ + μ ∘ (≅ ∘ i₁) +₁ (≅ ∘ i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ universal∘i₁≈h₁ ⟩⊗⟨ sym (¡-unique (≅ ∘ i₂ ∘ ¡)) ⟩∘⟨refl ⟩ + μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ μ∘¡ʳ ⟩ + id ∎ + + open 𝒟 using (U; monoidal; _⊗₁_; unitorʳ-commute-from) renaming (module unitorˡ to λ-; module unitorʳ to ρ) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + + same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s + same-deco = begin + F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ F₁ 𝒞.id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (𝒞.id , ¡)) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorʳ) F.unitaryʳ) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ F₁ ρ⇐′ ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorʳ-commute-from ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ∘ ρ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ ρ.isoʳ) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘id+¡ ○ F.identity) ⟩ + s ∎ + + open Morphism 𝒞.U using (_≅_) + open _≅_ + + ≅-L-R : (X≅Y : A ≅ B) → DecoratedCospans [ L.₁ (to X≅Y) ≈ R.₁ (from X≅Y) ] + ≅-L-R X≅Y = Decorate.F-resp-≈ (Embed.≅-L-R X≅Y) + where + module Decorate = Functor Decorate + + module ⊗ = Functor (⊗ 𝒞 F) + open 𝒞 using (_+₁_) + + L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ] + L-resp-⊗ = Decorate.F-resp-≈ Embed.L-resp-⊗ ○ Decorate-resp-⊗ + where + module Decorate = Functor Decorate + open DecoratedCospans.HomReasoning diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda new file mode 100644 index 0000000..80b7b2f --- /dev/null +++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -0,0 +1,229 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --no-require-unique-meta-solutions #-} + +open import Level using (Level) +module Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o ℓ e : Level} where + +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Object.Coproduct as Coproduct +import Categories.Object.Initial as Initial + +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) +open import Categories.Functor.Monoidal using (IsMonoidalFunctor) +open import Categories.Functor.Monoidal.Braided using (module Lax) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory; MonoidalCategory) +open import Categories.Category.Product using (_⁂_) +open import Categories.Morphism using (_≅_) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper) renaming (refl to ≃-refl) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using (module Lax) +open import Data.Product.Base using (_,_) + +open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Functor.Exact using (RightExactFunctor; idREF; ∘-RightExactFunctor) + +open FinitelyCocompleteCategory using () renaming (symmetricMonoidalCategory to smc) +open SymmetricMonoidalCategory using (unit) renaming (braidedMonoidalCategory to bmc) +open BraidedMonoidalCategory using () renaming (monoidalCategory to mc) + +private + variable + A B C : FinitelyCocompleteCategory o ℓ e + +F₀ : FinitelyCocompleteCategory o ℓ e → SymmetricMonoidalCategory o ℓ e +F₀ C = smc C +{-# INJECTIVE_FOR_INFERENCE F₀ #-} + +F₁ : RightExactFunctor A B → Lax.SymmetricMonoidalFunctor (F₀ A) (F₀ B) +F₁ {A} {B} F = record + { F = F.F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε-iso.from + ; ⊗-homo = ⊗-homo + ; associativity = assoc + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + ; braiding-compat = braiding-compat + } + } + where + module F = RightExactFunctor F + module A = SymmetricMonoidalCategory (F₀ A) + module B = SymmetricMonoidalCategory (F₀ B) + module A′ = FinitelyCocompleteCategory A + module B′ = FinitelyCocompleteCategory B + ε-iso : B.U [ B.unit ≅ F.₀ A.unit ] + ε-iso = Initial.up-to-iso B.U B′.initial (record { ⊥ = F.₀ A′.⊥ ; ⊥-is-initial = F.F-resp-⊥ A′.⊥-is-initial }) + module ε-iso = _≅_ ε-iso + +-iso : ∀ {X Y} → B.U [ F.₀ X B′.+ F.₀ Y ≅ F.₀ (X A′.+ Y) ] + +-iso = Coproduct.up-to-iso B.U B′.coproduct (Coproduct.IsCoproduct⇒Coproduct B.U (F.F-resp-+ (Coproduct.Coproduct⇒IsCoproduct A.U A′.coproduct))) + module +-iso {X Y} = _≅_ (+-iso {X} {Y}) + module B-proofs where + open ⇒-Reasoning B.U + open B.HomReasoning + open B.Equiv + open B using (_∘_; _≈_) + open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂) + open A′ using (_+_; i₁; i₂) + ⊗-homo : NaturalTransformation (B.⊗ ∘F (F.F ⁂ F.F)) (F.F ∘F A.⊗) + ⊗-homo = ntHelper record + { η = λ { (X , Y) → +-iso.from {X} {Y} } + ; commute = λ { {X , Y} {X′ , Y′} (f , g) → + B′.coproduct.∘-distribˡ-[] + ○ B′.coproduct.[]-cong₂ + (pullˡ B′.coproduct.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₁)) + (pullˡ B′.coproduct.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₂)) + ○ sym B′.coproduct.∘-distribˡ-[] } + } + assoc + : {X Y Z : A.Obj} + → F.₁ A′.+-assocˡ + ∘ +-iso.from {X + Y} {Z} + ∘ (+-iso.from {X} {Y} +₁ B.id {F.₀ Z}) + ≈ +-iso.from {X} {Y + Z} + ∘ (B.id {F.₀ X} +₁ +-iso.from {Y} {Z}) + ∘ B′.+-assocˡ + assoc {X} {Y} {Z} = begin + F.₁ A′.+-assocˡ ∘ +-iso.from ∘ (+-iso.from +₁ B.id) ≈⟨ refl⟩∘⟨ B′.[]∘+₁ ⟩ + F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩ + F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩ + B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ (i₂ A′.∘ i₂) ∘ B.id ] ≈⟨ []-cong₂ ([]-congˡ F.homomorphism) (B.identityʳ ○ F.homomorphism) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congʳ ([]-congˡ B′.coproduct.inject₁) ⟨ + B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁ , _ ] ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ ([]-cong₂ (sym B′.coproduct.inject₁) (pushˡ (sym B′.coproduct.inject₂))) ⟩ + B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟨ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congˡ B′.coproduct.inject₂ ⟨ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ] ≈⟨ []-congˡ (pushˡ (sym B′.coproduct.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨ + B′.[ F.₁ i₁ , B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ []-cong₂ B.identityʳ (B′.coproduct.∘-distribˡ-[]) ⟩∘⟨refl ⟨ + B′.[ F.₁ i₁ B′.∘ B′.id , F.₁ i₂ ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ pushˡ (sym B′.[]∘+₁) ⟩ + +-iso.from ∘ (B.id +₁ +-iso.from) ∘ B′.+-assocˡ ∎ + unitaryˡ + : {X : A.Obj} + → F.₁ A′.[ A′.initial.! , A.id {X} ] + ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] + ∘ B′.[ B′.i₁ ∘ B′.initial.! , B′.i₂ ∘ B.id ] + ≈ B′.[ B′.initial.! , B.id ] + unitaryˡ {X} = begin + F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩ + _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.initial.! , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.coproduct.inject₂) ⟩ + F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ B′.initial.! , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ _ ∘ B′.initial.! , F.₁ A′.[ A′.initial.! , A.id ] ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + B′.[ B′.initial.! , F.₁ A.id ∘ B.id ] ≈⟨ []-congˡ (elimˡ F.identity) ⟩ + B′.[ B′.initial.! , B.id ] ∎ + unitaryʳ + : {X : A.Obj} + → F.₁ A′.[ A′.id {X} , A′.initial.! ] + ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] + ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.initial.! ] + ≈ B′.[ B.id , B′.initial.! ] + unitaryʳ {X} = begin + F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ] ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩ + _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.initial.! ] ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.coproduct.inject₁) (sym (B′.¡-unique _)) ⟩ + F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ ∘ B.id , B′.initial.! ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.[ A.id , A′.initial.! ] ∘ F.₁ i₁ ∘ B.id , _ ∘ B′.initial.! ] ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) (sym (B′.¡-unique _)) ⟩ + B′.[ F.₁ A.id ∘ B.id , B′.initial.! ] ≈⟨ []-congʳ (elimˡ F.identity) ⟩ + B′.[ B.id , B′.initial.! ] ∎ + braiding-compat + : {X Y : A.Obj} + → F.₁ A′.[ i₂ {X} {Y} , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] + ≈ B′.[ F.F₁ i₁ , F.F₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ] + braiding-compat = begin + F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ] ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.coproduct.inject₁) ([ F.F ]-resp-∘ A′.coproduct.inject₂) ⟩ + B′.[ F.₁ i₂ , F.₁ i₁ ] ≈⟨ []-cong₂ B′.coproduct.inject₂ B′.coproduct.inject₁ ⟨ + B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨ + B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ] ∎ + open B-proofs + +identity : Lax.SymmetricMonoidalNaturalIsomorphism (F₁ (Functor.Exact.idREF {o} {ℓ} {e} {A})) (idF-SymmetricMonoidal (F₀ A)) +identity {A} = record + { U = ≃-refl + ; F⇒G-isMonoidal = record + { ε-compat = ¡-unique₂ (id ∘ ¡) id + ; ⊗-homo-compat = refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ) + } + } + where + open FinitelyCocompleteCategory A + open HomReasoning + open Equiv + +homomorphism + : {F : RightExactFunctor A B} + {G : RightExactFunctor B C} + → Lax.SymmetricMonoidalNaturalIsomorphism + (F₁ {A} {C} (∘-RightExactFunctor G F)) + (∘-SymmetricMonoidal (F₁ {B} {C} G) (F₁ {A} {B} F)) +homomorphism {A} {B} {C} {F} {G} = record + { U = ≃-refl + ; F⇒G-isMonoidal = record + { ε-compat = ¡-unique₂ (id ∘ ¡) (G.₁ B.¡ ∘ ¡) + ; ⊗-homo-compat = + identityˡ + ○ sym + ([]-cong₂ + ([ G.F ]-resp-∘ B.coproducts.inject₁) + ([ G.F ]-resp-∘ B.coproducts.inject₂)) + ○ sym ∘-distribˡ-[] + ○ pushʳ (introʳ C.⊗.identity) + } + } + where + module A = FinitelyCocompleteCategory A + module B = FinitelyCocompleteCategory B + open FinitelyCocompleteCategory C + module C = SymmetricMonoidalCategory (F₀ C) + open HomReasoning + open Equiv + open ⇒-Reasoning U + module F = RightExactFunctor F + module G = RightExactFunctor G + +module _ {F G : RightExactFunctor A B} where + + module F = RightExactFunctor F + module G = RightExactFunctor G + + F-resp-≈ + : NaturalIsomorphism F.F G.F + → Lax.SymmetricMonoidalNaturalIsomorphism (F₁ {A} {B} F) (F₁ {A} {B} G) + F-resp-≈ F≃G = record + { U = F≃G + ; F⇒G-isMonoidal = record + { ε-compat = sym (¡-unique (⇒.η A.⊥ ∘ ¡)) + ; ⊗-homo-compat = + ∘-distribˡ-[] + ○ []-cong₂ (⇒.commute A.i₁) (⇒.commute A.i₂) + ○ sym []∘+₁ + } + } + where + module A = FinitelyCocompleteCategory A + open NaturalIsomorphism F≃G + open FinitelyCocompleteCategory B + open HomReasoning + open Equiv + +Underlying : Functor FinitelyCocompletes SymMonCat +Underlying = record + { F₀ = F₀ + ; F₁ = F₁ + ; identity = λ { {X} → identity {X} } + ; homomorphism = λ { {X} {Y} {Z} {F} {G} → homomorphism {X} {Y} {Z} {F} {G} } + ; F-resp-≈ = λ { {X} {Y} {F} {G} → F-resp-≈ {X} {Y} {F} {G} } + } |