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 Elgot-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
open strongK using (strengthen)

-- some helper definitions to make our life easier
private
  η = λ Z → FreeObject.η (freealgebras Z)
  _♯ = λ {A X Y} f → IsStableFreeElgotAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
  _# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f

K is an equational lifting monad

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 # ⟩ ≈⟨ helper₁ ⟩
      ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈⟨ helper₂ ⟩ -- lemma20
      ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) # ∎
      where
        helper₁ : τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩
        helper₁ = begin 
          τ (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 ⟩ ∎
        helper₂ : ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈ ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) #
        helper₂ = sym (#-Uniformity (algebras _) (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 ⟩ ∎