open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Monad.Construction.Kleisli
open import Categories.Monad hiding (id)
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor hiding (id)
open import Monad.Helper

import Categories.Morphism.Reasoning as MR

-- Every Elgot monad is pre-Elgot

module Monad.Elgot.PreElgot {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  open Category C
  open Cocartesian cocartesian
  open import Algebra.Elgot cocartesian
  open import Monad.PreElgot cocartesian
  open import Monad.Elgot cocartesian
  open HomReasoning
  open Equiv
  open MR C

  IsElgot⇒IsPreElgot : ∀ (T : Monad C) → IsElgot T → IsPreElgot T
  IsElgot⇒IsPreElgot T isElgot = record 
    { elgotalgebras = λ {X} → Diamond-on⇒Elgot-on (T₀ X) (record
      { _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †
      ; #-Fixpoint = λ {Y} {f} → begin 
        ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †                                                 ≈⟨ †-Fixpoint ⟩ 
        extend [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f ≈⟨ pullˡ (∘[] ○ []-cong₂ ((extend∘F₁ T [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] i₁) ○ extend-≈ inject₁) ((pullˡ kleisli.identityʳ) ○ inject₂)) ⟩ 
        [ extend (η.η _) , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f                        ≈⟨ ([]-cong₂ kleisli.identityˡ refl) ⟩∘⟨refl ⟩ 
        [ id , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f                                    ∎
      ; #-Uniformity = λ {Y} {Z} {f} {g} {h} eq → 
        let
          uni-helper : ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ g) ∘ h ≈ T₁ (id +₁ h) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f
          uni-helper = begin 
            ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ g) ∘ h          ≈⟨ pullʳ (sym eq) ⟩ 
            [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ h) ∘ f    ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ assoc) ⟩ 
            [ T₁ i₁ , η.η _ ∘ i₂ ∘ h ] ∘ f            ≈˘⟨ ([]-cong₂ refl (∘-resp-≈ʳ inject₂)) ⟩∘⟨refl ⟩
            [ T₁ i₁ , η.η _ ∘ (id +₁ h) ∘ i₂ ] ∘ f    ≈˘⟨ pullˡ (∘[] ○ []-cong₂ (sym F.homomorphism ○ F.F-resp-≈ (inject₁ ○ identityʳ)) (extendʳ (sym (η.commute _)))) ⟩ 
            T₁ (id +₁ h) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f ∎
        in †-Uniformity uni-helper
      ; #-Diamond = #-Diamond
      ; #-resp-≈ = λ {Y} {f} {g} f≈g → †-resp-≈ (∘-resp-≈ʳ f≈g)
      })
    ; extend-preserves = λ {X} {Y} {Z} f h → begin 
      ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (extend h +₁ id) ∘ f) †                  ≈⟨ †-resp-≈ (pullˡ ([]∘+₁ ○ []-cong₂ (F₁∘extend T _ _) identityʳ)) ⟩ 
      (([ extend (T₁ i₁ ∘ h) , η.η _ ∘ i₂ ] ∘ f) †)                      ≈˘⟨ †-resp-≈ (pullˡ (∘[] ○ []-cong₂ (extend∘F₁ T _ i₁ ○ extend-≈ inject₁) (pullˡ kleisli.identityʳ ○ inject₂))) ⟩ 
      (extend [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ] ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈˘⟨ †-Naturality ⟩ 
      extend h ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †                          ∎ 
    }
    where
    module monad = Monad T
    open monad using (η; F)
    module kleisli = RMonad (Monad⇒Kleisli C T)
    open kleisli using (extend; extend-≈)
    open Functor F renaming (F₀ to T₀; F₁ to T₁)
    open IsElgot isElgot
    #-Diamond : ∀ {X Y} (f : Y ⇒ T₀ X + (Y + Y)) → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ [ id , id ]) ∘ f) † ≈ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ [ i₁ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ [ id , id ]) ∘ f) † +₁ id ] ∘ f) †
    #-Diamond {X} {Y} f = begin 
      ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ ∇) ∘ f) †                                                                                            ≈⟨ †-resp-≈ (extendʳ helper) ⟩
      (T₁ (id +₁ ∇) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †                                                                                         ≈⟨ †-Diamond ⟩
      (extend ([ η.η _ ∘ i₁ , [ (T₁ i₁ ∘ (T₁ (id +₁ ∇) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †) , (η.η _ ∘ i₂) ] ]) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ †-resp-≈ (pullˡ (∘[] ○ []-cong₂ (extend∘F₁ T _ _ ○ extend-≈ inject₁ ○ ∘-resp-≈ʳ homomorphism ○ cancelˡ monad.identityˡ) (pullˡ kleisli.identityʳ ○ inject₂))) ⟩
      ([ T₁ i₁ , [ T₁ i₁ ∘ (T₁ (id +₁ ∇) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † , (η.η _ ∘ i₂) ] ] ∘ f) †                                          ≈⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ refl ([]-cong₂ (∘-resp-≈ʳ (†-resp-≈ (extendʳ (sym helper)))) refl))) ⟩ 
      ([ T₁ i₁ , [ T₁ i₁ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ ∇) ∘ f) † , η.η _ ∘ i₂ ] ] ∘ f) †                                               ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ refl ([]∘+₁ ○ []-cong₂ refl identityʳ))) ⟩ 
      ([ T₁ i₁ , [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ [ id , id ]) ∘ f) † +₁ id) ] ∘ f) †                             ≈˘⟨ †-resp-≈ (pullˡ (∘[] ○ []-cong₂ inject₁ refl)) ⟩ 
      ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ [ i₁ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ [ id , id ]) ∘ f) † +₁ id ] ∘ f) †                                  ∎
      where
      helper : [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ ∇) ≈ T₁ (id +₁ ∇) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ]
      helper = begin 
        [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (id +₁ ∇)    ≈⟨ []∘+₁ ○ []-cong₂ identityʳ assoc ⟩ 
        [ T₁ i₁ , η.η _ ∘ i₂ ∘ ∇ ]            ≈˘⟨ ∘[] ○ []-cong₂ (sym homomorphism ○ F-resp-≈ (inject₁ ○ identityʳ)) ((extendʳ (sym (η.commute _))) ○ ∘-resp-≈ʳ inject₂) ⟩ 
        T₁ (id +₁ ∇) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∎