{-# OPTIONS --safe #-}

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)

import Categories.Morphism.Reasoning as MR

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

  record IsElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
    open Monad T using (η; μ; F)
    open RMonad (Monad⇒Kleisli C T) using (extend; extend-≈)
    open Functor F renaming (F₀ to T₀; F₁ to T₁)

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

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

    private
      ∇ : ∀ {X} → X + X ⇒ X
      ∇ = [ id , id ]
    †-Diamond : ∀ {X Y} {f : Y ⇒ T₀ (X + Y + Y)} → (T₁ (id +₁ ∇) ∘ f) † ≈ (extend [ η.η _ ∘ i₁ , [ T₁ i₁ ∘ (T₁ (id +₁ ∇) ∘ f) † , η.η _ ∘ i₂ ] ] ∘ f) †
    †-Diamond {X} {Y} {f} = begin 
      (T₁ (id +₁ ∇) ∘ f) †                                                                                      ≈⟨ helper ⟩
      (T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) † †                                                                       ≈⟨ †-Fixpoint ⟩ 
      extend [ η.η _ , (T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) † † ] ∘ (T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) †                ≈˘⟨ (extend-≈ ([]-cong₂ refl helper)) ⟩∘⟨refl ⟩
      extend [ η.η _ , (T₁ (id +₁ ∇) ∘ f) † ] ∘ (T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) †                               ≈⟨ †-Naturality ⟩ 
      (extend [ T₁ i₁ ∘ [ η.η _ , (T₁ (id +₁ ∇) ∘ f) † ] , η.η _ ∘ i₂ ] ∘ T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) †      ≈⟨ †-resp-≈ (∘-resp-≈ˡ (extend-≈ ([]-cong₂ (∘[] ○ []-cong₂ (sym (η.commute _)) refl) refl))) ⟩
      (extend [ [ η.η _ ∘ i₁ , T₁ i₁ ∘ (T₁ (id +₁ ∇) ∘ f) † ] , η.η _ ∘ i₂ ] ∘ T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) † ≈⟨ †-resp-≈ (pullˡ (extend∘F₁ T _ _ ○ extend-≈ (∘[] ○ []-cong₂ (pullˡ inject₁ ○ inject₁) ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩
      (extend [ η.η _ ∘ i₁ , [ T₁ i₁ ∘ (T₁ (id +₁ ∇) ∘ f) † , η.η _ ∘ i₂ ] ] ∘ f) †                             ∎
      where
      helper : (T₁ (id +₁ ∇) ∘ f) † ≈ (T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) † †
      helper = begin 
        (T₁ (id +₁ ∇) ∘ f) †                               ≈⟨ †-resp-≈ (∘-resp-≈ˡ (F-resp-≈ ([]-cong₂ identityʳ (∘[] ○ []-cong₂ identityʳ identityʳ)))) ⟩ 
        (T₁ [ i₁ , [ i₂ , i₂ ] ] ∘ f) †                    ≈˘⟨ †-resp-≈ (pullˡ (sym homomorphism ○ F-resp-≈ (∘[] ○ []-cong₂ (cancelˡ inject₁) ([]∘+₁ ○ []-cong₂ identityˡ identityʳ)))) ⟩
        (T₁ [ id , i₂ ] ∘ T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) † ≈⟨ †-Codiagonal ⟩ 
        (T₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f) † †                ∎
  
  record ElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      T : Monad C
      isElgot : IsElgot T

    open IsElgot isElgot public