aboutsummaryrefslogtreecommitdiff
path: root/Category/Monoidal
diff options
context:
space:
mode:
Diffstat (limited to 'Category/Monoidal')
-rw-r--r--Category/Monoidal/Coherence.agda132
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 λ₁≅ρ₁⇒
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-18 10:01:13 +0000