diff options
Diffstat (limited to 'Functor')
| -rw-r--r-- | Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 169 | ||||
| -rw-r--r-- | Functor/Exact/Instance/Swap.agda | 79 | ||||
| -rw-r--r-- | Functor/Instance/Cospan/Stack.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Decorate.agda | 168 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Embed.agda | 275 | ||||
| -rw-r--r-- | Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 229 |
6 files changed, 921 insertions, 1 deletions
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} } + } |