open import Level
open import Categories.Category.Core
open import Categories.Category.Extensive.Bundle
open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.Extensive
open import ElgotAlgebra

import Categories.Morphism.Reasoning as MR

module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
  open HomReasoning
  open Cocartesian (Extensive.cocartesian extensive)
  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
  open BinaryProducts products hiding (η)
  open MR C
  open Equiv
  
  open import Categories.Monad
  open import Categories.Functor

  record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
    open Monad T
    open Functor F renaming (F₀ to T₀; F₁ to T₁)

    -- every TX needs to be equipped with an elgot algebra structure
    field
      elgotalgebras : ∀ {X} → Elgot-Algebra-on ED (T₀ X)

    module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})

    -- with the following associativity
    field
      assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
  
  record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      T : Monad C
      isPreElgot : IsPreElgot T

    open IsPreElgot isPreElgot public

  record IsElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
    open Monad T
    open Functor F renaming (F₀ to T₀; F₁ to T₁)

    -- iteration operator
    field
      _† : ∀ {X Y} → X ⇒ T₀ (Y + X) → X ⇒ T₀ Y

    -- laws
    field
      Fixpoint : ∀ {X Y} {f : X ⇒ T₀ (Y + X)} → f † ≈ (μ.η _ ∘ T₁ [ η.η _ , f † ]) ∘ f
      Naturality : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Y ⇒ T₀ Z} → (μ.η _ ∘ T₁ g) ∘ f † ≈ ((μ.η _ ∘ T₁ [ (T₁ i₁) ∘ g , η.η _ ∘ i₂ ]) ∘ f)†
      Codiagonal : ∀ {X Y} {f : X ⇒ T₀ ((Y + X) + X)} → (T₁ [ idC , i₂ ] ∘ f )† ≈ f † †
      Uniformity : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Z ⇒ T₀ (Y + Z)} {h : Z ⇒ X} → f ∘ h ≈ (T₁ (idC +₁ h)) ∘ g → f † ∘ h ≈ g †

  record ElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      T : Monad C
      isElgot : IsElgot T

    open IsElgot isElgot public

  -- elgot monads are pre-elgot
  Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
  Elgot⇒PreElgot EM = record 
    { T = T 
    ; isPreElgot = record 
      { elgotalgebras = λ {X} → record
        { _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †
        ; #-Fixpoint = λ {Y} {f} → begin 
          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ Fixpoint ⟩ 
          (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) ≈⟨ pullˡ ∘[] ⟩
          [ (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ T₁ i₁ 
          , (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ η.η _ ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (pullʳ (sym homomorphism)) (pullˡ (pullʳ (η.sym-commute [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]))) ⟩∘⟨refl ⟩
          [ μ.η _ ∘ T₁ ([ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘  i₁) 
          , (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩
          [ μ.η _ ∘ (T₁ (η.η _))
          , μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩
          [ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ∎
        ; #-Uniformity = {!   !}
        ; #-Folding = {!   !}
        ; #-resp-≈ = {!   !}
        } 
      ; assoc = {!   !} 
      } 
    }
    where
      open ElgotMonad EM
      module T = Monad T
      open T
      open Functor F renaming (F₀ to T₀; F₁ to T₁)