diff options
Diffstat (limited to 'Category/Monoidal')
| -rw-r--r-- | Category/Monoidal/Instance/Cospans.agda | 15 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/Cospans/Lift.agda | 15 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans.agda | 17 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans/Lift.agda | 2 |
4 files changed, 22 insertions, 27 deletions
diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda index 228ddea..a1648db 100644 --- a/Category/Monoidal/Instance/Cospans.agda +++ b/Category/Monoidal/Instance/Cospans.agda @@ -18,8 +18,9 @@ open import Categories.Category.Monoidal.Core using (Monoidal) open import Categories.Functor using (Functor) open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) -open import Category.Instance.Cospans 𝒞 using (Cospans; Cospan) -open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan using (Cospan; cospan) +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC) open import Category.Monoidal.Instance.Cospans.Lift {o} {ℓ} {e} using (module Square) open import Data.Product.Base using (_,_) open import Functor.Instance.Cospan.Stack 𝒞 using (⊗) @@ -61,7 +62,6 @@ CospansMonoidal = record ; pentagon = pentagon } where - module ⊗ = Functor ⊗ module Cospans = Category Cospans module Unitorˡ = Square ⊥+--id module Unitorʳ = Square -+⊥-id @@ -83,16 +83,15 @@ CospansMonoidal = record 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 { f₁ = f₁ f , f₁ g ; f₂ = f₂ f , f₂ g }) } - ; iso = λ { (X , Y) → Braiding.FX≅GX′.iso {X , Y} } + { η = λ (X , Y) → Braiding.FX≅GX′.from {X , Y} + ; η⁻¹ = λ (Y , X) → Braiding.FX≅GX′.to {Y , X} + ; commute = λ (cospan f₁ f₂ , cospan g₁ g₂) → Braiding.from (cospan (f₁ , g₁) (f₂ , g₂)) + ; iso = λ (X , Y) → Braiding.FX≅GX′.iso {X , Y} } ; hexagon₁ = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym homomorphism ○ sym homomorphism ○ L-resp-≈ hex₁ ○ homomorphism ○ refl⟩∘⟨ homomorphism ; hexagon₂ = sym L-resp-⊗ ⟩∘⟨refl ⟩∘⟨ sym L-resp-⊗ ○ sym homomorphism ⟩∘⟨refl ○ sym homomorphism ○ L-resp-≈ hex₂ ○ homomorphism ○ homomorphism ⟩∘⟨refl } where - open Cospan module Cospans = Category Cospans open Cospans.Equiv open Cospans.HomReasoning diff --git a/Category/Monoidal/Instance/Cospans/Lift.agda b/Category/Monoidal/Instance/Cospans/Lift.agda index fa31fcb..c7e7516 100644 --- a/Category/Monoidal/Instance/Cospans/Lift.agda +++ b/Category/Monoidal/Instance/Cospans/Lift.agda @@ -4,7 +4,7 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor module Category.Monoidal.Instance.Cospans.Lift {o ℓ e} where -open import Category.Instance.Cospans using (Cospans; Cospan; Same) +open import Category.Instance.Cospans using (Cospans) open import Categories.Category.Core using (Category) @@ -16,6 +16,7 @@ import Category.Diagram.Pushout as PushoutDiagram′ import Functor.Instance.Cospan.Embed as CospanEmbed open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; module Definitions) +open import Category.Diagram.Cospan using (Cospan; cospan) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_) @@ -26,7 +27,7 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} {𝒟 : FinitelyCocompleteC module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = FinitelyCocompleteCategory 𝒟 - open CospanEmbed 𝒟 using (L; B₁; B∘L; R∘B; ≅-L-R) + open CospanEmbed 𝒟 using (L; B∘L; R∘B; ≅-L-R) module Square {F G : Functor 𝒞.U 𝒟.U} (F≃G : F ≃ G) where @@ -51,21 +52,21 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} {𝒟 : FinitelyCocompleteC open Cospan fg renaming (f₁ to f; f₂ to g) open 𝒟 using (_∘_) - squares⇒cospan : Cospans 𝒟 [ B₁ (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) ≈ B₁ (F.₁ f) (F.₁ g) ] + squares⇒cospan : Cospans 𝒟 [ cospan (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) ≈ cospan (F.₁ f) (F.₁ g) ] squares⇒cospan = record { ≅N = ≅.sym 𝒟.U FX≅GX - ; from∘f₁≈f₁′ = sym (switch-fromtoˡ FX≅GX (⇒.commute f)) - ; from∘f₂≈f₂′ = sym (switch-fromtoˡ FX≅GX (⇒.commute g)) + ; from∘f₁≈f₁ = sym (switch-fromtoˡ FX≅GX (⇒.commute f)) + ; from∘f₂≈f₂ = sym (switch-fromtoˡ FX≅GX (⇒.commute g)) } where open 𝒟.Equiv using (sym) - from : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇒.η Y) ∘ B₁ (F.₁ f) (F.₁ g) ] ≈ Cospans 𝒟 [ B₁ (G.₁ f) (G.₁ g) ∘ L.₁ (⇒.η X) ] ] + from : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇒.η Y) ∘ cospan (F.₁ f) (F.₁ g) ] ≈ Cospans 𝒟 [ cospan (G.₁ f) (G.₁ g) ∘ 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) - to : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇐.η Y) ∘ B₁ (G.₁ f) (G.₁ g) ] ≈ Cospans 𝒟 [ B₁ (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.η X) ] ] + to : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇐.η Y) ∘ cospan (G.₁ f) (G.₁ g) ] ≈ Cospans 𝒟 [ cospan (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.η X) ] ] to = switch-fromtoʳ FX≅GX′ (pullʳ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan) where open ⇒-Reasoning (Cospans 𝒟) using (pullʳ) diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda index c570e54..3df57ee 100644 --- a/Category/Monoidal/Instance/DecoratedCospans.agda +++ b/Category/Monoidal/Instance/DecoratedCospans.agda @@ -55,7 +55,6 @@ open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+ 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 (ρ⇒; ρ⇐; λ⇒) @@ -77,7 +76,7 @@ module LiftUnitorˡ where 𝒟.≈ 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) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ (F.₁ f ∘ x) ∘ ρ⇐ ≈⟨ push-center 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ʳ ⟨ @@ -117,7 +116,6 @@ module LiftUnitorˡ where open LiftUnitorˡ using (module Unitorˡ) module LiftUnitorʳ where - module ⊗ = Functor ⊗ module F = SymmetricMonoidalFunctor F open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐) @@ -139,7 +137,7 @@ module LiftUnitorʳ where 𝒟.≈ 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 ∘ x) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ≈⟨ push-center 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ʳ ⟨ @@ -177,7 +175,6 @@ module LiftUnitorʳ where open LiftUnitorʳ using (module Unitorʳ) module LiftAssociator where - module ⊗ = Functor ⊗ module F = SymmetricMonoidalFunctor F open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐) @@ -208,11 +205,11 @@ module LiftAssociator where 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 ⟩ + ≈⟨ refl⟩∘⟨ push-center ⊗-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-∘) ⟩ + ≈⟨ push-center ⊗-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 ∘ ρ⇐ @@ -246,11 +243,11 @@ module LiftAssociator where 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 ⟩ + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center ⊗-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-∘) ⟩ + ≈⟨ push-center ⊗-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 ∘ ρ⇐) ∘ ρ⇐ @@ -288,7 +285,6 @@ module LiftAssociator where open LiftAssociator using (module Associator) module LiftBraiding where - module ⊗ = Functor ⊗ module F = SymmetricMonoidalFunctor F open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐) @@ -364,7 +360,6 @@ CospansMonoidal = record ; pentagon = pentagon } where - module ⊗ = Functor ⊗ open Category DecoratedCospans using (id; module Equiv; module HomReasoning) open Equiv open HomReasoning diff --git a/Category/Monoidal/Instance/DecoratedCospans/Lift.agda b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda index 70795dd..c75f0db 100644 --- a/Category/Monoidal/Instance/DecoratedCospans/Lift.agda +++ b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda @@ -23,7 +23,7 @@ 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.Cospans using (Cospans) 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) |