diff options
Diffstat (limited to 'Category/Monoidal/Instance')
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans.agda | 30 | ||||
| -rw-r--r-- | Category/Monoidal/Instance/DecoratedCospans/Products.agda | 2 |
2 files changed, 16 insertions, 16 deletions
diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda index 3df57ee..b0625ab 100644 --- a/Category/Monoidal/Instance/DecoratedCospans.agda +++ b/Category/Monoidal/Instance/DecoratedCospans.agda @@ -257,21 +257,21 @@ module LiftAssociator where 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 ∘ ρ⇐ ∎ + 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 (α⇒; λ⇐) diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda index f8ef542..647f887 100644 --- a/Category/Monoidal/Instance/DecoratedCospans/Products.agda +++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda @@ -25,7 +25,7 @@ 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.Symmetric.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) |