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

  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
      †-resp-≈ : ∀ {X Y} {f g : X ⇒ T₀ (Y + X)} → f ≈ g → f † ≈ g †

    -- 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₂ 
                                                                                                    (pushʳ (homomorphism)) 
                                                                                                    (pushˡ (pushʳ (η.commute _)))
                                                                                                  ⟩∘⟨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 = λ {X} {Y} {f} {g} {h} H → sym (Uniformity (begin 
            ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ g) ∘ h                           ≈˘⟨ pushʳ H ⟩
            [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ h) ∘ f                    ≈⟨ pullˡ []∘+₁ ⟩
            [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ h ] ∘ f                     ≈⟨ []-cong₂ (trans identityʳ (F-resp-≈ (sym identityʳ))) assoc ⟩∘⟨refl ⟩
            [ T₁ (i₁ ∘ idC) , η.η _ ∘ i₂ ∘ h ] ∘ f                     ≈˘⟨ []-cong₂ (F-resp-≈ +₁∘i₁) (pullʳ +₁∘i₂) ⟩∘⟨refl ⟩
            [ T₁ ((idC +₁ h) ∘ i₁) , (η.η _ ∘ (idC +₁ h)) ∘ i₂ ] ∘ f   ≈⟨ []-cong₂ homomorphism ( pushˡ (η.commute _)) ⟩∘⟨refl ⟩
            [ T₁ (idC +₁ h) ∘ T₁ i₁ , T₁ (idC +₁ h) ∘ η.η _ ∘ i₂ ] ∘ f ≈˘⟨ pullˡ ∘[] ⟩
            T₁ (idC +₁ h) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f ∎))
        ; #-Folding = λ {X} {Y} {f} {h} → begin 
          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ ((([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †) +₁ h))† ≈⟨ †-resp-≈ []∘+₁ ⟩ 
          [ T₁ i₁ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † , (η.η _ ∘ i₂) ∘ h ] † ≈⟨ {!   !} ⟩
          {!   !} ≈⟨ {!   !} ⟩
          [ [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ i₁ ] ∘ f , (η.η _ ∘ i₂) ∘ h ] † ≈˘⟨ †-resp-≈ ([]-cong₂ (pullˡ []∘+₁) (pullˡ inject₂)) ⟩
          [ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ i₁) ∘ f , [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ i₂ ∘ h ] † ≈˘⟨ †-resp-≈ ∘[] ⟩
          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])† ∎
        ; #-resp-≈ = λ fg → †-resp-≈ (∘-resp-≈ʳ fg)
        }
      ; assoc = λ {X} {Y} {Z} f h → begin 
        -- TODO tidy up by moving doing sym outside, apply Naturality and then do `†-resp-≈ pullˡ` once.
        ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (μ.η Y ∘ T₁ h +₁ idC) ∘ f)†                                                             ≈⟨ †-resp-≈ (pullˡ []∘+₁) ⟩ 
        (([ T₁ i₁ ∘ μ.η _ ∘ T₁ h , (η.η _ ∘ i₂) ∘ idC ] ∘ f)†)                                                            ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ assoc (sym identityʳ))) ⟩
        ([ (T₁ i₁ ∘ μ.η _) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)†                                                                    ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-congʳ (pullˡ (μ.commute _)))) ⟩
        ([ μ.η _ ∘ T₁ (T₁ i₁) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)†                                                                 ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ homomorphism) (cancelˡ T.identityʳ))) ⟩
        ([ μ.η _ ∘ T₁ (T₁ i₁ ∘ h) , μ.η _ ∘ η.η _ ∘ η.η _ ∘ i₂ ] ∘ f)†                                                    ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (∘-resp-≈ʳ (pullʳ inject₂)))) ⟩
        ([ μ.η _ ∘ T₁ ([ T₁ i₁ ∘ h , η.η _ ∘ i₂ ] ∘ i₁) , μ.η _ ∘ (η.η _ ∘ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ i₂ ] ∘ f)†       ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (pullʳ (sym homomorphism)) (pullʳ (pullˡ (η.sym-commute _))))) ⟩
        ([ (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ T₁ i₁ , (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (pullˡ ∘[]) ⟩
        ((μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f)†                                           ≈˘⟨ Naturality ⟩
        (μ.η Y ∘ T₁ h) ∘ ([ T₁ i₁ ,  η.η _ ∘ i₂ ] ∘ f)†                                                                   ∎ 
      } 
    }
    where
      open ElgotMonad EM
      module T = Monad T
      open T using (F; η; μ)
      open Functor F renaming (F₀ to T₀; F₁ to T₁)