Prove associativity for decorated cospan composition

1 files changed, 132 insertions, 0 deletions

diff --git a/Category/Monoidal/Coherence.agda b/Category/Monoidal/Coherence.agda
new file mode 100644
index 0000000..7603860
--- /dev/null
+++ b/Category/Monoidal/Coherence.agda
@@ -0,0 +1,132 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Monoidal.Core using (Monoidal)
+
+module Category.Monoidal.Coherence {o ℓ e} {𝒞 : Category o ℓ e} (monoidal : Monoidal 𝒞) where
+
+import Categories.Morphism as Morphism
+import Categories.Morphism.IsoEquiv as IsoEquiv
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+
+open import Categories.Functor.Properties using ([_]-resp-≅)
+
+open Monoidal monoidal
+open Category 𝒞
+
+open ⇒-Reasoning 𝒞
+open ⊗-Reasoning monoidal
+open Morphism 𝒞 using (_≅_)
+open IsoEquiv 𝒞 using (to-unique)
+
+open Equiv
+
+𝟏 : Obj
+𝟏 = unit
+
+module α≅ = associator
+module λ≅ = unitorˡ
+module ρ≅ = unitorʳ
+
+private
+  variable
+    A B C D : Obj
+
+α⇒ : (A ⊗₀ B) ⊗₀ C ⇒ A ⊗₀ B ⊗₀ C
+α⇒ = α≅.from
+
+α⇐ : A ⊗₀ B ⊗₀ C ⇒ (A ⊗₀ B) ⊗₀ C
+α⇐ = α≅.to
+
+λ⇒ : 𝟏 ⊗₀ A ⇒ A
+λ⇒ = λ≅.from
+
+λ⇐ : A ⇒ 𝟏 ⊗₀ A
+λ⇐ = λ≅.to
+
+ρ⇒ : A ⊗₀ 𝟏 ⇒ A
+ρ⇒ = ρ≅.from
+
+ρ⇐ : A ⇒ A ⊗₀ 𝟏
+ρ⇐ = ρ≅.to
+
+α⊗id : ((A ⊗₀ B) ⊗₀ C) ⊗₀ D ≅ (A ⊗₀ B ⊗₀ C) ⊗₀ D
+α⊗id {A} {B} {C} {D} = [ -⊗ D ]-resp-≅ (associator {A} {B} {C})
+
+module α⊗id {A} {B} {C} {D} = _≅_ (α⊗id {A} {B} {C} {D})
+
+perimeter
+    : α⇒ {𝟏} {A} {B} ∘ (ρ⇒ {𝟏} ⊗₁ id {A}) ⊗₁ id {B}
+    ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ B} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {B} ∘ α⇒ {𝟏} {𝟏 ⊗₀ A} {B} ∘ α⇒ {𝟏} {𝟏} {A} ⊗₁ id {B}
+perimeter = begin
+    α⇒ ∘ (ρ⇒ ⊗₁ id) ⊗₁ id               ≈⟨ assoc-commute-from ⟩
+    ρ⇒ ⊗₁ id ⊗₁ id ∘ α⇒                 ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩
+    ρ⇒ ⊗₁ id ∘ α⇒                       ≈⟨ pullˡ triangle ⟨
+    id ⊗₁ λ⇒ ∘ α⇒ ∘ α⇒                  ≈⟨ refl⟩∘⟨ pentagon ⟨
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id ∎
+
+perimeter-triangle
+    : α⇒ {𝟏} {A} {C} ∘ (id {𝟏} ⊗₁ λ⇒ {A}) ⊗₁ id {C}
+    ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ C} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {C} ∘ α⇒ {𝟏} {𝟏 ⊗₀ A} {C}
+perimeter-triangle = begin
+    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id                            ≈⟨ refl⟩∘⟨ identityʳ ⟨
+    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ id                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ α⊗id.isoʳ ⟨
+    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐ ⊗₁ id      ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨
+    α⇒ ∘ (id ⊗₁ λ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐ ⊗₁ id            ≈⟨ refl⟩∘⟨ triangle ⟩⊗⟨refl ⟩∘⟨refl ⟩
+    α⇒ ∘ (ρ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id                 ≈⟨ extendʳ perimeter ⟩
+    id ⊗₁ λ⇒ ∘ (id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ assoc ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id ∘ α⇐ ⊗₁ id   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ α⊗id.isoʳ ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ id                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒                         ∎
+
+perimeter-triangle-square
+    : ∀ {A C : Obj}
+    → id {𝟏} ⊗₁ λ⇒ {A} ⊗₁ id {C}
+    ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ C} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {C}
+perimeter-triangle-square = begin
+    id ⊗₁ λ⇒ ⊗₁ id                  ≈⟨ identityʳ ⟨
+    id ⊗₁ λ⇒ ⊗₁ id ∘ id             ≈⟨ refl⟩∘⟨ associator.isoʳ ⟨
+    id ⊗₁ λ⇒ ⊗₁ id ∘ α⇒ ∘ α⇐        ≈⟨ extendʳ assoc-commute-from ⟨
+    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ α⇐      ≈⟨ extendʳ perimeter-triangle ⟩
+    id ⊗₁ λ⇒ ∘ (id ⊗₁ α⇒ ∘ α⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇐   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ associator.isoʳ ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ id        ≈⟨ refl⟩∘⟨ identityʳ ⟩
+    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒             ∎
+
+λₕi≈λₕᵢ∘α₁ₕᵢ : λ⇒ {A} ⊗₁ id {C} ≈ λ⇒ {A ⊗₀ C} ∘ α⇒ {𝟏} {A} {C}
+λₕi≈λₕᵢ∘α₁ₕᵢ = begin
+    λ⇒ ⊗₁ id                          ≈⟨ insertʳ unitorˡ.isoʳ ⟩
+    (λ⇒ ⊗₁ id ∘ λ⇒) ∘ λ⇐              ≈⟨ unitorˡ-commute-from ⟩∘⟨refl ⟨
+    (λ⇒ ∘ id ⊗₁ λ⇒ ⊗₁ id) ∘ λ⇐        ≈⟨ (refl⟩∘⟨ perimeter-triangle-square) ⟩∘⟨refl ⟩
+    (λ⇒ ∘ id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒) ∘ λ⇐   ≈⟨ (refl⟩∘⟨ merge₂ˡ) ⟩∘⟨refl ⟩
+    (λ⇒ ∘ id ⊗₁ (λ⇒ ∘ α⇒)) ∘ λ⇐       ≈⟨ unitorˡ-commute-from ⟩∘⟨refl ⟩
+    ((λ⇒ ∘ α⇒) ∘ λ⇒) ∘ λ⇐             ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
+    λ⇒ ∘ α⇒                           ∎
+
+1λ₁≈λ₁₁ : id {𝟏} ⊗₁ λ⇒ {𝟏} ≈ λ⇒ {𝟏 ⊗₀ 𝟏}
+1λ₁≈λ₁₁ = begin
+    id ⊗₁ λ⇒            ≈⟨ insertˡ unitorˡ.isoˡ ⟩
+    λ⇐ ∘ λ⇒ ∘ id ⊗₁ λ⇒  ≈⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩
+    λ⇐ ∘ λ⇒ ∘ λ⇒        ≈⟨ cancelˡ unitorˡ.isoˡ ⟩
+    λ⇒                  ∎
+
+λ₁𝟏≈ρ₁𝟏 : λ⇒ {𝟏} ⊗₁ id {𝟏} ≈ ρ⇒ {𝟏} ⊗₁ id {𝟏}
+λ₁𝟏≈ρ₁𝟏 = begin
+    λ⇒ ⊗₁ id      ≈⟨ λₕi≈λₕᵢ∘α₁ₕᵢ ⟩
+    λ⇒ ∘ α⇒       ≈⟨ 1λ₁≈λ₁₁ ⟩∘⟨refl ⟨
+    id ⊗₁ λ⇒ ∘ α⇒ ≈⟨ triangle ⟩
+    ρ⇒ ⊗₁ id      ∎
+
+λ₁≅ρ₁⇒ : λ⇒ {𝟏} ≈ ρ⇒ {𝟏}
+λ₁≅ρ₁⇒ = begin
+    λ⇒                    ≈⟨ insertʳ unitorʳ.isoʳ ⟩
+    (λ⇒ ∘ ρ⇒) ∘ ρ⇐        ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟨
+    (ρ⇒ ∘ λ⇒ ⊗₁ id) ∘ ρ⇐  ≈⟨ (refl⟩∘⟨ λ₁𝟏≈ρ₁𝟏) ⟩∘⟨refl ⟩
+    (ρ⇒ ∘ ρ⇒ ⊗₁ id) ∘ ρ⇐  ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟩
+    (ρ⇒ ∘ ρ⇒) ∘ ρ⇐        ≈⟨ cancelʳ unitorʳ.isoʳ ⟩
+    ρ⇒                    ∎
+
+λ₁≅ρ₁⇐ : λ⇐ {𝟏} ≈ ρ⇐ {𝟏}
+λ₁≅ρ₁⇐ = to-unique λ≅.iso ρ≅.iso λ₁≅ρ₁⇒