K is an Equational Lifting Monad

module Monad.Instance.K.EquationalLifting {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.ElgotAlgebras cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)

open HomReasoning
open Equiv
open M C
open MR C
open kleisliK using (extend)
open monadK using (μ)
open FreeObject using (*-uniq)
open strongK using (strengthen)

The equational lifting law follows by the universal property of free objects, i.e. we show that τ (K.₀ X , X) ∘ Δ is a elgot algbera morphism that satisfies the universal property.

equationalLifting : ∀ {X} → τ (K.₀ X , X) ∘ Δ {K.₀ X} ≈ K.₁ ⟨ η X , idC ⟩
equationalLifting {X} = *-uniq (freealgebras _) (η _ ∘ ⟨ η X , idC ⟩) (record { h = τ (K.₀ X , X) ∘ Δ ; preserves = preserves' }) commute
  where
  preserves' : ∀ {Z} {f : Z ⇒ K.₀ X + Z} → (τ (K.₀ X , X) ∘ Δ) ∘ f # ≈ ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) #
  preserves' {Z} {f} = begin 
    (τ (K.₀ X , X) ∘ Δ) ∘ f #                                   ≈⟨ pullʳ Δ∘ ⟩ 
    τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩                               ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) (sym identityʳ)) ○ sym ⁂∘⟨⟩) ⟩ 
    τ (K.₀ X , X) ∘ (idC ⁂ f #) ∘ ⟨ f # , idC ⟩                 ≈⟨ pullˡ (τ-comm f) ⟩ 
    ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈⟨ sym (#-Uniformity (algebras _) by-uni) ⟩
    ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) #                          ∎
    where
    by-uni : (idC +₁ ⟨ f # , idC ⟩) ∘ (τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f ≈ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f)) ∘ ⟨ f # , idC ⟩
    by-uni = begin 
      (idC +₁ ⟨ f # , idC ⟩) ∘ (τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f    ≈⟨ pullˡ +₁∘+₁ ⟩ 
      (idC ∘ τ (K.₀ X , X) ∘ Δ +₁ ⟨ f # , idC ⟩ ∘ idC) ∘ f       ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
      (τ (K.₀ X , X) ∘ Δ +₁ idC ∘ ⟨ f # , idC ⟩) ∘ f             ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
      ((τ _ +₁ idC) ∘ (Δ +₁ ⟨ f # , idC ⟩)) ∘ f                  ≈⟨ assoc ⟩ 
      (τ _ +₁ idC) ∘ (Δ +₁ ⟨ f # , idC ⟩) ∘ f                    ≈⟨ refl⟩∘⟨ distrib ⟩ 
      (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩                 ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩ 
      (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ f # , f ∘ idC ⟩     ≈˘⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ 
      ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f)) ∘ ⟨ f # , idC ⟩ ∎
      where
      distrib : (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩
      distrib = Iso⇒Mono C (IsIso.iso isIsoˡ) ((Δ +₁ ⟨ f # , idC ⟩) ∘ f) (distributeˡ⁻¹ ∘ ⟨ f # , f ⟩) (begin 
        distributeˡ ∘ (Δ +₁ ⟨ f # , idC ⟩) ∘ f              ≈⟨ pullˡ []∘+₁ ⟩ 
        [ (idC ⁂ i₁) ∘ Δ , (idC ⁂ i₂) ∘ ⟨ f # , idC ⟩ ] ∘ f ≈⟨ ([]-cong₂ ⁂∘Δ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
        [ ⟨ idC , i₁ ⟩ , ⟨ idC ∘ f # , i₂ ∘ idC ⟩ ] ∘ f     ≈⟨ ([]-unique 
                                                              (⟨⟩∘ ○ (⟨⟩-cong₂ inject₁ identityˡ)) 
                                                              (⟨⟩∘ ○ (⟨⟩-cong₂ (inject₂ ○ sym identityˡ) id-comm-sym))) ⟩∘⟨refl ⟩ 
        ⟨ [ idC , f # ] , idC ⟩ ∘ f                         ≈⟨ ⟨⟩∘ ⟩ 
        ⟨ [ idC , f # ] ∘ f , idC ∘ f ⟩                     ≈˘⟨ ⟨⟩-cong₂ (#-Fixpoint (algebras _)) (sym identityˡ) ⟩ 
        ⟨ f # , f ⟩                                         ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ 
        distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩           ∎)
  commute : (τ (K.₀ X , X) ∘ Δ) ∘ η _ ≈ η _ ∘ ⟨ η X , idC ⟩
  commute = begin 
    (τ (K.₀ X , X) ∘ Δ) ∘ η _                   ≈⟨ pullʳ Δ∘ ⟩ 
    τ (K.₀ X , X) ∘ ⟨ η X , η X ⟩               ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (sym identityʳ) ○ sym ⁂∘⟨⟩) ⟩ 
    τ (K.₀ X , X) ∘ (idC ⁂ η X) ∘ ⟨ η X , idC ⟩ ≈⟨ pullˡ (τ-η _) ⟩ 
    η _ ∘ ⟨ η X , idC ⟩                         ∎