diff options
Diffstat (limited to 'Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda')
| -rw-r--r-- | Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 229 |
1 files changed, 229 insertions, 0 deletions
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} } + } |