diff options
Diffstat (limited to 'Functor/Instance/Decorate.agda')
| -rw-r--r-- | Functor/Instance/Decorate.agda | 168 |
1 files changed, 168 insertions, 0 deletions
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₁ ¡ ∘ ε) ∘ ρ⇐ ∎ + |