{-# OPTIONS --without-K --safe #-}

open import Categories.Category
open import Categories.Category.Monoidal.Core using (Monoidal)

-- Reassociation lemmas for monoidal categories.

module Categories.Category.Monoidal.Reassociation
  {o β„“ e} {π’ž : Category o β„“ e} (M : Monoidal π’ž) where

open Category π’ž
open Monoidal M

open import Categories.Category.Construction.Core π’ž as Core using (Core)
open import Categories.Category.Monoidal.Properties M
open import Categories.Category.Monoidal.Utilities M
open import Categories.Category.Monoidal.Reasoning M
import Categories.Morphism.Reasoning as MR

open Core.Shorthands
open Shorthands
open MR π’ž

private
  variable
    A B C D X Y Z : Obj

------------------------------------------------------------------------
-- Unitors against the associator.

Ξ»β‡’-assoc : (Ξ»β‡’ {A} βŠ—β‚ id {B}) ∘ α⇐ β‰ˆ Ξ»β‡’
Ξ»β‡’-assoc = ⟺ (switch-fromtoΚ³ associator coherence₁)

λ⇐-assoc : Ξ±β‡’ ∘ (λ⇐ {A} βŠ—β‚ id {B}) β‰ˆ λ⇐
λ⇐-assoc = begin
  Ξ±β‡’ ∘ (λ⇐ βŠ—β‚ id)   β‰ˆΛ˜βŸ¨ refl⟩∘⟨ coherence-inv₁ ⟩
  Ξ±β‡’ ∘ (α⇐ ∘ λ⇐)    β‰ˆβŸ¨ cancelΛ‘ associator.isoΚ³ ⟩
  λ⇐                ∎

ρ⇒-assoc : ρ⇒ ∘ α⇐ {X} {Y} {unit} β‰ˆ id βŠ—β‚ ρ⇒
ρ⇒-assoc = ⟺ (switch-fromtoΚ³ associator coherenceβ‚‚)

ρ⇐-assoc : id {A} βŠ—β‚ ρ⇐ {B} β‰ˆ Ξ±β‡’ ∘ ρ⇐
ρ⇐-assoc = begin
  id βŠ—β‚ ρ⇐                 β‰ˆΛ˜βŸ¨ cancelΛ‘ associator.isoΚ³ ⟩
  Ξ±β‡’ ∘ (α⇐ ∘ (id βŠ—β‚ ρ⇐))   β‰ˆβŸ¨ refl⟩∘⟨ coherence-invβ‚‚ ⟩
  Ξ±β‡’ ∘ ρ⇐                  ∎

-- Commute the left unitor past a right counit through the associator: the
-- |coherence₁| triangle, then the right unitor's square.
Ξ»β‡’-ρ⇐-comm : Ξ»β‡’ ∘ Ξ±β‡’ ∘ ρ⇐ β‰ˆ ρ⇐ {X} ∘ Ξ»β‡’
Ξ»β‡’-ρ⇐-comm = pullΛ‘ coherence₁ β—‹ ⟺ unitorΚ³-commute-to

------------------------------------------------------------------------
-- Whiskered maps against the associator.  Each is `assoc-commute-from/to`
-- with one leg's `id βŠ—β‚ id` folded away.

Ξ±β‡’-idβŠ—-commute : {k : X β‡’ Y} β†’
  Ξ±β‡’ {A} {B} {Y} ∘ (id βŠ—β‚ k) β‰ˆ (id βŠ—β‚ (id βŠ—β‚ k)) ∘ Ξ±β‡’
Ξ±β‡’-idβŠ—-commute {k = k} = begin
  Ξ±β‡’ ∘ (id βŠ—β‚ k)            β‰ˆΛ˜βŸ¨ refl⟩∘⟨ (βŠ—.identity βŸ©βŠ—βŸ¨refl) ⟩
  Ξ±β‡’ ∘ ((id βŠ—β‚ id) βŠ—β‚ k)    β‰ˆβŸ¨ assoc-commute-from ⟩
  (id βŠ—β‚ (id βŠ—β‚ k)) ∘ Ξ±β‡’    ∎

α⇐-idβŠ—-commute : {k : X β‡’ Y} β†’
  (id {A βŠ—β‚€ B} βŠ—β‚ k) ∘ α⇐ β‰ˆ α⇐ ∘ (id βŠ—β‚ (id βŠ—β‚ k))
α⇐-idβŠ—-commute {k = k} = begin
  (id βŠ—β‚ k) ∘ α⇐            β‰ˆΛ˜βŸ¨ (βŠ—.identity βŸ©βŠ—βŸ¨refl) ⟩∘⟨refl ⟩
  ((id βŠ—β‚ id) βŠ—β‚ k) ∘ α⇐    β‰ˆΛ˜βŸ¨ assoc-commute-to ⟩
  α⇐ ∘ (id βŠ—β‚ (id βŠ—β‚ k))    ∎

α⇐-βŠ—id-commute : {k : X β‡’ Y} β†’
  α⇐ {Y} {A} {B} ∘ (k βŠ—β‚ id) β‰ˆ ((k βŠ—β‚ id) βŠ—β‚ id) ∘ α⇐
α⇐-βŠ—id-commute {k = k} = begin
  α⇐ ∘ (k βŠ—β‚ id)          β‰ˆΛ˜βŸ¨ refl⟩∘⟨ (reflβŸ©βŠ—βŸ¨ βŠ—.identity) ⟩
  α⇐ ∘ (k βŠ—β‚ (id βŠ—β‚ id))  β‰ˆβŸ¨ assoc-commute-to ⟩
  ((k βŠ—β‚ id) βŠ—β‚ id) ∘ α⇐  ∎

Ξ±β‡’-βŠ—id-commute : {k : X β‡’ Y} β†’
  Ξ±β‡’ {Y} {A} {B} ∘ ((k βŠ—β‚ id) βŠ—β‚ id) β‰ˆ (k βŠ—β‚ id) ∘ Ξ±β‡’
Ξ±β‡’-βŠ—id-commute {k = k} = begin
  Ξ±β‡’ ∘ ((k βŠ—β‚ id) βŠ—β‚ id)  β‰ˆβŸ¨ assoc-commute-from ⟩
  (k βŠ—β‚ (id βŠ—β‚ id)) ∘ Ξ±β‡’  β‰ˆβŸ¨ (reflβŸ©βŠ—βŸ¨ βŠ—.identity) ⟩∘⟨refl ⟩
  (k βŠ—β‚ id) ∘ Ξ±β‡’          ∎

-- Maps whiskered into *different* factors commute past each other: both sides are
-- `f βŠ—β‚ g`, serialized the two ways round.
whisker-comm : {f : A β‡’ B} {g : X β‡’ Y} β†’
  (f βŠ—β‚ id {Y}) ∘ (id {A} βŠ—β‚ g) β‰ˆ (id βŠ—β‚ g) ∘ (f βŠ—β‚ id {X})
whisker-comm = ⟺ serialize₁₂ β—‹ serialize₂₁

-- Rebracketing commutes with a map tensored on either side.
rebracket-tightenΛ‘ : {f : B β‡’ C} {h : A βŠ—β‚€ (X βŠ—β‚€ Y) β‡’ B βŠ—β‚€ (X βŠ—β‚€ Y)} β†’
  α⇐ ∘ ((f βŠ—β‚ id) ∘ h) ∘ Ξ±β‡’ β‰ˆ ((f βŠ—β‚ id) βŠ—β‚ id) ∘ (α⇐ ∘ h ∘ Ξ±β‡’)
rebracket-tightenΛ‘ {f = f} {h = h} = begin
  α⇐ ∘ ((f βŠ—β‚ id) ∘ h) ∘ Ξ±β‡’   β‰ˆβŸ¨ refl⟩∘⟨ assoc ⟩
  α⇐ ∘ (f βŠ—β‚ id) ∘ h ∘ Ξ±β‡’     β‰ˆβŸ¨ extendΚ³ α⇐-βŠ—id-commute ⟩
  ((f βŠ—β‚ id) βŠ—β‚ id) ∘ α⇐ ∘ h ∘ Ξ±β‡’ ∎

rebracket-tightenΚ³ : {h : B βŠ—β‚€ (X βŠ—β‚€ Y) β‡’ C βŠ—β‚€ (X βŠ—β‚€ Y)} {g : A β‡’ B} β†’
  α⇐ ∘ (h ∘ (g βŠ—β‚ id)) ∘ Ξ±β‡’ β‰ˆ (α⇐ ∘ h ∘ Ξ±β‡’) ∘ ((g βŠ—β‚ id) βŠ—β‚ id)
rebracket-tightenΚ³ {h = h} {g = g} = begin
  α⇐ ∘ (h ∘ (g βŠ—β‚ id)) ∘ Ξ±β‡’        β‰ˆβŸ¨ refl⟩∘⟨ assoc ⟩
  α⇐ ∘ h ∘ (g βŠ—β‚ id) ∘ Ξ±β‡’          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ ⟺ Ξ±β‡’-βŠ—id-commute ⟩
  α⇐ ∘ h ∘ Ξ±β‡’ ∘ ((g βŠ—β‚ id) βŠ—β‚ id)  β‰ˆβŸ¨ assoc²Ρβ ⟩
  (α⇐ ∘ h ∘ Ξ±β‡’) ∘ ((g βŠ—β‚ id) βŠ—β‚ id) ∎

------------------------------------------------------------------------
-- Pentagon corollaries.

pentagon-assoc : Ξ±β‡’ {A βŠ—β‚€ B} {C} {D} ∘ (α⇐ βŠ—β‚ id) ∘ α⇐ β‰ˆ α⇐ ∘ (id βŠ—β‚ Ξ±β‡’)
pentagon-assoc = conjugate-from (idα΅’ βŠ—α΅’ (associator ⁻¹)) (associator ⁻¹) pentagon-inv

assoc-to-coherence :
  (id {A} βŠ—β‚ α⇐ {B} {C} {D}) ∘ Ξ±β‡’ β‰ˆ Ξ±β‡’ ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐
assoc-to-coherence = begin
  (id βŠ—β‚ α⇐) ∘ Ξ±β‡’         β‰ˆβŸ¨ conjugate-from associator (idα΅’ βŠ—α΅’ associator) (⟺ pentagon) ⟩
  (Ξ±β‡’ ∘ (Ξ±β‡’ βŠ—β‚ id)) ∘ α⇐  β‰ˆβŸ¨ assoc ⟩
  Ξ±β‡’ ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐    ∎

assoc-from-coherence :
  Ξ±β‡’ {A βŠ—β‚€ B} {C} {D} ∘ (α⇐ βŠ—β‚ id) β‰ˆ α⇐ ∘ (id βŠ—β‚ Ξ±β‡’) ∘ Ξ±β‡’
assoc-from-coherence =
  switch-tofromΚ³ associator (assoc β—‹ pentagon-assoc) β—‹ assoc

-- Two associators followed by `α⇐ βŠ—β‚ id` drop a level.
pentagon-collapse :
  (Ξ±β‡’ {A} {B} {C βŠ—β‚€ D} ∘ Ξ±β‡’) ∘ (α⇐ βŠ—β‚ id) β‰ˆ (id βŠ—β‚ Ξ±β‡’) ∘ Ξ±β‡’
pentagon-collapse = pullΚ³ assoc-from-coherence β—‹ cancelΛ‘ associator.isoΚ³

pentagon-collapse-inv :
  (Ξ±β‡’ {A} {B} {C} βŠ—β‚ id {D}) ∘ α⇐ ∘ α⇐ β‰ˆ α⇐ ∘ (id βŠ—β‚ α⇐)
pentagon-collapse-inv = begin
  (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐ ∘ α⇐
    β‰ˆΛ˜βŸ¨ refl⟩∘⟨ pentagon-inv ⟩
  (Ξ±β‡’ βŠ—β‚ id) ∘ ((α⇐ βŠ—β‚ id) ∘ α⇐) ∘ (id βŠ—β‚ α⇐)
    β‰ˆβŸ¨ refl⟩∘⟨ assoc ⟩
  (Ξ±β‡’ βŠ—β‚ id) ∘ (α⇐ βŠ—β‚ id) ∘ α⇐ ∘ (id βŠ—β‚ α⇐)
    β‰ˆβŸ¨ cancelΛ‘ (βŠ—-cancel associator.isoΚ³ identityΒ²) ⟩
  α⇐ ∘ (id βŠ—β‚ α⇐)  ∎

-- Associator-conjugation slide.  Conjugating an `id βŠ—β‚ f` block by `α⇐ ∘ _ ∘ Ξ±β‡’`
-- on the left, whiskered by `id` and wrapped in a further pair of associators,
-- equals the same `f` conjugated by `Ξ±β‡’ ∘ _ ∘ α⇐` on the right, under one `Ξ±β‡’`.
-- `f` is opaque β€” this is pure pentagon/associator gymnastics.
Ξ±-conj-slide : {f : A βŠ—β‚€ X β‡’ B βŠ—β‚€ X} β†’
  Ξ±β‡’ ∘ Ξ±β‡’ ∘ ((α⇐ ∘ (id {Y} βŠ—β‚ f) ∘ Ξ±β‡’) βŠ—β‚ id {Z}) ∘ α⇐
  β‰ˆ (id βŠ—β‚ (Ξ±β‡’ ∘ (f βŠ—β‚ id) ∘ α⇐)) ∘ Ξ±β‡’
Ξ±-conj-slide {f = f} = begin
  Ξ±β‡’ ∘ Ξ±β‡’ ∘ ((α⇐ ∘ (id βŠ—β‚ f) ∘ Ξ±β‡’) βŠ—β‚ id) ∘ α⇐                    β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ split₁³ ⟩∘⟨refl ⟩
  Ξ±β‡’ ∘ Ξ±β‡’ ∘ ((α⇐ βŠ—β‚ id) ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ±β‡’ βŠ—β‚ id)) ∘ α⇐    β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ assocΒ²Ξ²Ξ΅ ⟩
  Ξ±β‡’ ∘ Ξ±β‡’ ∘ (α⇐ βŠ—β‚ id) ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐      β‰ˆβŸ¨ assoc²Ρα ⟩
  ((Ξ±β‡’ ∘ Ξ±β‡’) ∘ (α⇐ βŠ—β‚ id)) ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐  β‰ˆβŸ¨ pentagon-collapse ⟩∘⟨refl ⟩
  ((id βŠ—β‚ Ξ±β‡’) ∘ Ξ±β‡’) ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐         β‰ˆβŸ¨ assoc ⟩
  (id βŠ—β‚ Ξ±β‡’) ∘ Ξ±β‡’ ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐           β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ assoc-commute-from ⟩
  (id βŠ—β‚ Ξ±β‡’) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ Ξ±β‡’ ∘ (Ξ±β‡’ βŠ—β‚ id) ∘ α⇐           β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ assoc-to-coherence ⟩
  (id βŠ—β‚ Ξ±β‡’) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (id βŠ—β‚ α⇐) ∘ Ξ±β‡’                β‰ˆΛ˜βŸ¨ assocΒ²Ξ²Ξ΅ ⟩
  ((id βŠ—β‚ Ξ±β‡’) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (id βŠ—β‚ α⇐)) ∘ Ξ±β‡’              β‰ˆβŸ¨ mergeβ‚‚Β³ ⟩∘⟨refl ⟩
  (id βŠ—β‚ (Ξ±β‡’ ∘ (f βŠ—β‚ id) ∘ α⇐)) ∘ Ξ±β‡’                              ∎