{-# OPTIONS --allow-unsolved-metas #-}
open import Categories.Category.Core
open import Categories.Monad hiding (id)
open import Categories.Monad.Strong
open import Categories.Monad.Commutative
open import Categories.Functor.Core
open import Categories.Category.Restriction
open import Categories.Category.Cartesian
open import Categories.Category.Cartesian.Bundle
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.BinaryProducts
open import Categories.Category.Construction.Kleisli
open import Categories.Object.Terminal
open import Categories.NaturalTransformation hiding (id)
open import Monad.EquationalLifting
open import Data.Product using (_,_)
import Categories.Morphism.Reasoning as MR
-- The Kleisli category of equational lifting monads is a restriction category
module Monad.EquationalLifting.Restriction {o ℓ e} (CC : CartesianCategory o ℓ e) where
open CartesianCategory CC
open HomReasoning
open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)
open CartesianMonoidal cartesian using (monoidal)
open Terminal terminal using (!; ⊤)
open MR U
open Equiv
kleisli-restriction : ∀ (EM : EquationalLiftingMonad cartesian) → Restriction (Kleisli (StrongMonad.M (CommutativeMonad.strongMonad (EquationalLiftingMonad.commutativeMonad EM))))
kleisli-restriction EM = record
{ _↓ = _↓
; pidʳ = pidʳ'
; ↓-comm = ↓-comm'
; ↓-denestʳ = {! !}
; ↓-skew-comm = ↓-skew-comm'
; ↓-cong = ↓-cong'
}
where
open EquationalLiftingMonad EM hiding (identityˡ)
open Monad M using (F; μ; η)
open Functor F using () renaming (F₀ to M₀; F₁ to M₁)
module rightStrength = RightStrength rightStrength
_↓ : ∀ {A B} → A ⇒ M₀ B → A ⇒ M₀ A
f ↓ = M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩
-- TODO probably not needed
_↓' : ∀ {A B} → A ⇒ M₀ B → A ⇒ M₀ A
f ↓' = M₁ π₂ ∘ τ ∘ ⟨ f , id ⟩
↓'≈↓ : ∀ {A B} {f : A ⇒ M₀ B} → f ↓' ≈ f ↓
↓'≈↓ {A} {B} {f} = _
↓-cong' : ∀ {A B : Obj} {f g : A ⇒ M₀ B} → f ≈ g → (f ↓) ≈ (g ↓)
↓-cong' {A} {B} {f} {g} f≈g = refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl f≈g
↓-skew-comm' : ∀ {A B C} {g : A ⇒ M₀ B} {f : C ⇒ M₀ A} → (μ.η A ∘ M₁ (g ↓)) ∘ f ≈ (μ.η A ∘ M₁ f) ∘ ((μ.η B ∘ M₁ g) ∘ f) ↓
↓-skew-comm' {A} {B} {C} {g} {f} = begin
(μ.η A ∘ M₁ (M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩)) ∘ f ≈⟨ {! !} ⟩
μ.η A ∘ M₁ (M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩) ∘ f ≈⟨ {! !} ⟩
μ.η A ∘ M₁ (M₁ π₁) ∘ M₁ σ ∘ M₁ ⟨ id , g ⟩ ∘ f ≈⟨ {! !} ⟩
μ.η A ∘ M₁ (M₁ π₁) ∘ M₁ σ ∘ M₁ ⟨ id , g ⟩ ∘ (μ.η _ ∘ M₁ f) ∘ M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ (M₁ π₁) ∘ M₁ σ ∘ M₁ ⟨ id , g ⟩ ∘ μ.η _ ∘ M₁ f ∘ M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ (M₁ π₁) ∘ M₁ σ ∘ μ.η _ ∘ M₁ (M₁ ⟨ id , g ⟩) ∘ M₁ f ∘ M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
μ.η A ∘ M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ M₁ (f ⁂ g) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ M₁ (f ⁂ M₁ id) ∘ M₁ (id ⁂ g) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ π₁ ∘ μ.η _ ∘ M₁ (M₁ (f ⁂ id)) ∘ M₁ σ ∘ M₁ (id ⁂ g) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ π₁ ∘ M₁ (f ⁂ id) ∘ μ.η _ ∘ M₁ σ ∘ M₁ (id ⁂ g) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ f ∘ M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ M₁ (id ⁂ g) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ f ∘ M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ (id ⁂ M₁ g) ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ f ∘ M₁ π₁ ∘ (μ.η _ ∘ M₁ σ ∘ σ) ∘ (id ⁂ M₁ g) ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ f ∘ M₁ π₁ ∘ σ ∘ (id ⁂ μ.η B) ∘ (id ⁂ M₁ g) ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ f ∘ M₁ π₁ ∘ σ ∘ (id ⁂ μ.η B ∘ M₁ g) ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
μ.η A ∘ M₁ f ∘ M₁ π₁ ∘ σ ∘ ⟨ id , μ.η B ∘ M₁ g ∘ f ⟩ ≈⟨ {! !} ⟩
(μ.η A ∘ M₁ f) ∘ M₁ π₁ ∘ σ ∘ ⟨ id , (μ.η B ∘ M₁ g) ∘ f ⟩ ∎
Mswap-invariant : ∀ {A B C} {f : A ⇒ M₀ (B × C)} → (M₁ swap ∘ f) ↓ ≈ f ↓
Mswap-invariant {A} {B} {C} {f} = begin
M₁ π₁ ∘ σ ∘ ⟨ id , M₁ swap ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
M₁ π₁ ∘ σ ∘ (id ⁂ M₁ swap) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ (extendʳ (σ.commute (id , swap))) ⟩
M₁ π₁ ∘ M₁ (id ⁂ swap) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ (project₁ ○ identityˡ)) ⟩
M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩ ∎
pidʳ' : {A B : Obj} {f : A ⇒ M₀ B} → (μ.η B ∘ M₁ f) ∘ (f ↓) ≈ f
pidʳ' {A} {B} {f} = _
-- commented out for faster typechecking
-- begin
-- (μ.η B ∘ M₁ f) ∘ M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ (pullʳ (sym M.F.homomorphism)) ⟩
-- (μ.η B ∘ M₁ (f ∘ π₁)) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ (refl⟩∘⟨ (M.F.F-resp-≈ (sym project₁))) ⟩∘⟨refl ⟩
-- (μ.η B ∘ M₁ (π₁ ∘ (f ⁂ id))) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ (refl⟩∘⟨ M.F.homomorphism) ⟩∘⟨refl ⟩
-- (μ.η B ∘ M₁ π₁ ∘ M₁ (f ⁂ id)) ∘ σ ∘ ⟨ id , f ⟩ ≈⟨ pullʳ (pullˡ (pullʳ (sym (σ.commute (f , id))))) ⟩
-- μ.η B ∘ (M₁ π₁ ∘ σ ∘ (f ⁂ M₁ id)) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ pull-last (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ M.F.identity)) ⟩
-- μ.η B ∘ M₁ π₁ ∘ σ ∘ ⟨ f , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ Δ∘ ⟩
-- μ.η B ∘ M₁ π₁ ∘ σ ∘ Δ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ equationalLifting ⟩
-- μ.η B ∘ M₁ π₁ ∘ M.F.₁ ⟨ η.η B , id ⟩ ∘ f ≈⟨ refl⟩∘⟨ (pullˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ project₁)) ⟩
-- μ.η B ∘ M₁ (η.η B) ∘ f ≈⟨ cancelˡ M.identityˡ ⟩
-- f ∎
σ-τ : ∀ {A B} → σ {A} {B} ≈ M₁ swap ∘ τ ∘ swap
σ-τ = sym (begin
M₁ swap ∘ τ ∘ swap ≈⟨ refl ⟩
M₁ swap ∘ (M₁ swap ∘ σ ∘ swap) ∘ swap ≈⟨ pullˡ (cancelˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ swap∘swap ○ M.F.identity)) ⟩
(σ ∘ swap) ∘ swap ≈⟨ cancelʳ swap∘swap ⟩
σ ∎)
↓-comm' : ∀ {A B C} {f : A ⇒ M₀ B} {g : A ⇒ M₀ C} → (μ.η A ∘ M₁ (f ↓)) ∘ g ↓ ≈ (μ.η A ∘ M₁ (g ↓)) ∘ f ↓
↓-comm' {A} {B} {C} {f} {g} = _
-- begin
-- (μ.η A ∘ M₁ (f ↓)) ∘ g ↓ ≈⟨ key ⟩
-- (μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩) ↓ ≈⟨ refl ⟩
-- (μ.η _ ∘ M₁ σ ∘ (M₁ swap ∘ σ ∘ swap) ∘ ⟨ f , g ⟩) ↓ ≈⟨ ↓-cong' (refl⟩∘⟨ refl⟩∘⟨ pullʳ (pullʳ swap∘⟨⟩)) ⟩
-- (μ.η _ ∘ M₁ σ ∘ M₁ swap ∘ σ ∘ ⟨ g , f ⟩) ↓ ≈⟨ ↓-cong' (refl⟩∘⟨ ((M.F.F-resp-≈ σ-τ) ⟩∘⟨refl)) ⟩
-- (μ.η _ ∘ M₁ (M₁ swap ∘ τ ∘ swap) ∘ M₁ swap ∘ σ ∘ ⟨ g , f ⟩) ↓ ≈⟨ ↓-cong' (refl⟩∘⟨ (M.F.homomorphism ○ refl⟩∘⟨ M.F.homomorphism) ⟩∘⟨refl) ⟩
-- (μ.η _ ∘ (M₁ (M₁ swap) ∘ M₁ τ ∘ M₁ swap) ∘ M₁ swap ∘ σ ∘ ⟨ g , f ⟩) ↓ ≈⟨ ↓-cong' (refl⟩∘⟨ (pullʳ (pullʳ (cancelˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ swap∘swap ○ M.F.identity))))) ⟩
-- (μ.η _ ∘ M₁ (M₁ swap) ∘ M₁ τ ∘ σ ∘ ⟨ g , f ⟩) ↓ ≈⟨ ↓-cong' (pullˡ (μ.commute swap)) ⟩
-- ((M₁ swap ∘ μ.η _) ∘ M₁ τ ∘ σ ∘ ⟨ g , f ⟩) ↓ ≈⟨ ↓-cong' assoc ⟩
-- (M₁ swap ∘ μ.η _ ∘ M₁ τ ∘ σ ∘ ⟨ g , f ⟩) ↓ ≈⟨ ↓-cong' (refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ commutes) ○ assoc²βε)) ⟩
-- (M₁ swap ∘ μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ g , f ⟩) ↓ ≈⟨ Mswap-invariant ⟩
-- (μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ g , f ⟩) ↓
-- p₁ : ∀ {A B} → M₁ π₁ ∘ τ ≈ π₁ {M₀ A} {B}
-- p₁ {A} {B} = begin
-- M₁ π₁ ∘ τ ≈˘⟨ pullˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ (project₁ ○ identityˡ)) ⟩
-- M₁ π₁ ∘ M₁ (id ⁂ !) ∘ τ ≈⟨ refl⟩∘⟨ (sym (τ.commute (id , !))) ⟩
-- M₁ π₁ ∘ τ ∘ (M₁ id ⁂ !) ≈⟨ pullˡ rightStrength.identityˡ ⟩
-- π₁ ∘ (M₁ id ⁂ !) ≈⟨ project₁ ○ elimˡ M.F.identity ⟩
-- π₁ ∎
-- key : ∀ {A B C} {f : A ⇒ M₀ B} {g : A ⇒ M₀ C} → (μ.η _ ∘ M₁ (f ↓)) ∘ g ↓ ≈ (μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩) ↓
-- key {A} {B} {C} {f} {g} = begin
-- (μ.η A ∘ M₁ (M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩)) ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ≈⟨ (refl⟩∘⟨ (M.F.homomorphism ○ refl⟩∘⟨ M.F.homomorphism)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ assoc²βε ⟩
-- μ.η A ∘ M₁ (M₁ π₁) ∘ M₁ σ ∘ M₁ ⟨ id , f ⟩ ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ≈⟨ extendʳ (μ.commute π₁) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ M₁ ⟨ id , f ⟩ ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ ⁂∘Δ) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ M₁ (id ⁂ f) ∘ M₁ Δ ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ helper₁ ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ M₁ (id ⁂ f) ∘ σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ (sym (σ.commute (id , f)))) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ (id ⁂ M₁ f) ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ f ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (extendʳ (sym M.F.homomorphism ○ M.F.F-resp-≈ project₁ ○ M.F.homomorphism)) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ π₁ ∘ M₁ (f ⁂ id) ∘ σ ∘ ⟨ id , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ (extendʳ (sym (σ.commute (f , id))))) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ (f ⁂ M₁ id) ∘ ⟨ id , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ M.F.identity))) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ helper ⟩
-- M₁ π₁ ∘ M₁ (id ⁂ π₁) ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (cancelˡ M.identityʳ) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ η.η _ ∘ M₁ (id ⁂ π₁) ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl ((sym-assoc ○ pullˡ (assoc ○ sym commutes)) ○ assoc²βε) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ η.η _ ∘ M₁ (id ⁂ π₁) ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (η.commute (M₁ (id ⁂ π₁))) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ M₁ (M₁ (id ⁂ π₁)) ∘ η.η _ ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ (extendʳ (μ.commute (id ⁂ π₁))) ⟩
-- M₁ π₁ ∘ M₁ (id ⁂ π₁) ∘ μ.η _ ∘ η.η _ ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ pullˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ (project₁ ○ identityˡ)) ⟩
-- M₁ π₁ ∘ μ.η _ ∘ η.η _ ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ (cancelˡ M.identityʳ) ⟩
-- M₁ π₁ ∘ σ {A} {B × C} ∘ ⟨ id , μ.η _ ∘ M₁ σ ∘ τ ∘ ⟨ f , g ⟩ ⟩ ∎
-- where
-- helper : μ.η _ ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈ M₁ (id ⁂ π₁) ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩
-- helper = begin
-- μ.η (A × B) ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl ((M.F.F-resp-≈ p₁) ⟩∘⟨refl) ⟩
-- μ.η (A × B) ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ (M₁ π₁ ∘ τ) ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (pullˡ (sym M.F.homomorphism)) ⟩
-- μ.η (A × B) ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ (M₁ π₁) ∘ M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
-- μ.η (A × B) ∘ M₁ σ ∘ σ ∘ (id ⁂ M₁ (M₁ π₁)) ∘ ⟨ id , M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , M₁ π₁)) ⟩
-- μ.η (A × B) ∘ M₁ σ ∘ M₁ (id ⁂ M₁ π₁) ∘ σ ∘ ⟨ id , M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ (extendʳ (sym M.F.homomorphism ○ M.F.F-resp-≈ (σ.commute (id , π₁)) ○ M.F.homomorphism)) ⟩
-- μ.η (A × B) ∘ M₁ (M₁ (id ⁂ π₁)) ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ extendʳ (μ.commute (id ⁂ π₁)) ⟩
-- M₁ (id ⁂ π₁) ∘ μ.η _ ∘ M₁ σ ∘ σ ∘ ⟨ id , M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ μ-η-comm) ○ assoc ○ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
-- M₁ (id ⁂ π₁) ∘ σ ∘ ⟨ id , μ.η _ ∘ M₁ τ ∘ σ ∘ ⟨ f , g ⟩ ⟩ ∎
-- associate : Δ ∘ π₁ ≈ (id ⁂ π₁) ∘ assocˡ ∘ (Δ ⁂ id)
-- associate = ⟨⟩-unique′ a₁ a₂
-- where
-- a₁ = begin
-- π₁ ∘ Δ ∘ π₁ ≈˘⟨ pullʳ project₁ ⟩
-- (π₁ ∘ π₁) ∘ (Δ ⁂ id) ≈˘⟨ pullˡ project₁ ⟩
-- π₁ ∘ assocˡ ∘ (Δ ⁂ id) ≈˘⟨ identityˡ ⟩∘⟨refl ⟩
-- (id ∘ π₁) ∘ assocˡ ∘ (Δ ⁂ id) ≈˘⟨ pullˡ project₁ ⟩
-- π₁ ∘ (id ⁂ π₁) ∘ assocˡ ∘ (Δ ⁂ id) ∎
-- a₂ = sym (begin
-- π₂ ∘ (id ⁂ π₁) ∘ assocˡ ∘ (Δ ⁂ id) ≈⟨ pullˡ project₂ ⟩
-- (π₁ ∘ π₂) ∘ assocˡ ∘ (Δ ⁂ id) ≈⟨ pullˡ (pullʳ project₂) ⟩
-- (π₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (Δ ⁂ id) ≈⟨ project₁ ⟩∘⟨refl ⟩
-- (π₂ ∘ π₁) ∘ (Δ ⁂ id) ≈⟨ pullʳ project₁ ⟩
-- π₂ ∘ Δ ∘ π₁ ∎)
-- helper₁ : M₁ Δ ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ≈ σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ⟩
-- helper₁ = begin
-- M₁ Δ ∘ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ≈⟨ pullˡ ( sym M.F.homomorphism ○ M.F.F-resp-≈ associate) ⟩
-- M₁ ((id ⁂ π₁) ∘ assocˡ ∘ (Δ ⁂ id)) ∘ σ ∘ ⟨ id , g ⟩ ≈⟨ ((M.F.homomorphism ○ refl⟩∘⟨ M.F.homomorphism) ⟩∘⟨refl) ○ assoc²βε ⟩
-- M₁ (id ⁂ π₁) ∘ M₁ assocˡ ∘ M₁ (Δ ⁂ id) ∘ σ ∘ ⟨ id , g ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (sym (σ.commute (Δ , id))) ○ pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ M.F.identity))) ⟩
-- M₁ (id ⁂ π₁) ∘ M₁ assocˡ ∘ σ ∘ ⟨ Δ , g ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocʳ∘⟨⟩ ⟩
-- M₁ (id ⁂ π₁) ∘ M₁ assocˡ ∘ σ ∘ assocʳ ∘ ⟨ id , ⟨ id , g ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘Δ ⟩
-- M₁ (id ⁂ π₁) ∘ M₁ assocˡ ∘ σ ∘ assocʳ ∘ (id ⁂ ⟨ id , g ⟩) ∘ Δ ≈⟨ refl⟩∘⟨ (pullˡ strength-assoc) ⟩
-- M₁ (id ⁂ π₁) ∘ (σ ∘ (id ⁂ σ) ∘ assocˡ) ∘ assocʳ ∘ (id ⁂ ⟨ id , g ⟩) ∘ Δ ≈⟨ refl⟩∘⟨ (pullˡ (pullʳ (cancelʳ assocˡ∘assocʳ)) ○ assoc) ⟩
-- M₁ (id ⁂ π₁) ∘ σ ∘ (id ⁂ σ) ∘ (id ⁂ ⟨ id , g ⟩) ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
-- M₁ (id ⁂ π₁) ∘ σ ∘ (id ⁂ σ ∘ ⟨ id , g ⟩) ∘ Δ ≈⟨ extendʳ (sym (σ.commute (id , π₁))) ⟩
-- σ ∘ (id ⁂ M₁ π₁) ∘ (id ⁂ σ ∘ ⟨ id , g ⟩) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
-- σ ∘ (id ⁂ M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩) ∘ Δ ≈⟨ refl⟩∘⟨ ⁂∘Δ ⟩
-- σ ∘ ⟨ id , M₁ π₁ ∘ σ ∘ ⟨ id , g ⟩ ⟩ ∎