{-# OPTIONS --safe #-}
open import Level
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Equivalence
open import Categories.Monad hiding (id)
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor hiding (id)
open import Categories.Monad.Construction.Kleisli
open import Categories.Category.Core
open import Categories.Category.Cocartesian
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR


module Category.Construction.PreElgotMonads {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
open import Monad.PreElgot cocartesian
open import Algebra.Elgot cocartesian
open Cocartesian cocartesian renaming (+-unique to []-unique)
open Category C
open HomReasoning
open Equiv
open M C
open MR C

module _ (P S : PreElgotMonad) where
  private
    open PreElgotMonad P using () renaming (T to TP; elgotalgebras to P-elgots)
    open PreElgotMonad S using () renaming (T to TS; elgotalgebras to S-elgots)
    module TP = Monad TP
    module TS = Monad TS
    open RMonad (Monad⇒Kleisli C TP) using () renaming (extend to extendP)
    open RMonad (Monad⇒Kleisli C TS) using () renaming (extend to extendS)
    _#P = λ {X} {A} f → P-elgots._# {X} {A} f
    _#S = λ {X} {A} f → S-elgots._# {X} {A} f
  record PreElgotMonad-Morphism : Set (o ⊔ ℓ ⊔ e) where
    field
      α : NaturalTransformation TP.F TS.F
    module α = NaturalTransformation α
    field
      α-η : ∀ {X}
        → α.η X ∘ TP.η.η X ≈ TS.η.η X
      α-μ : ∀ {X}
        → α.η X ∘ TP.μ.η X ≈ TS.μ.η X ∘ TS.F.₁ (α.η X) ∘ α.η (TP.F.₀ X)
      preserves : ∀ {X A} (f : X ⇒ TP.F.₀ A + X) → α.η A ∘ f #P ≈ ((α.η A +₁ id) ∘ f) #S

PreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
PreElgotMonads = record
  { Obj = PreElgotMonad
  ; _⇒_ = PreElgotMonad-Morphism
  ; _≈_ = λ f g → (PreElgotMonad-Morphism.α f) ≃ (PreElgotMonad-Morphism.α g)
  ; id = id'
  ; _∘_ = _∘'_
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv = record { refl = refl ; sym = λ f → sym f ; trans = λ f g → trans f g }
  ; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
  }
  where
    open Elgot-Algebra-on using (#-resp-≈)
    id' : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism A A
    id' {A} = record
      { α = ntHelper (record
        { η = λ _ → id
        ; commute = λ _ → id-comm-sym
        })
      ; α-η = identityˡ
      ; α-μ = sym (begin
        T.μ.η _ ∘ T.F.₁ id ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
        T.μ.η _ ∘ T.F.₁ id       ≈⟨ elimʳ T.F.identity ⟩
        T.μ.η _                   ≈⟨ sym identityˡ ⟩
        id ∘ T.μ.η _             ∎)
      ; preserves = λ f → begin
        id ∘ f #            ≈⟨ identityˡ ⟩
        f #                  ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
        ((id +₁ id) ∘ f) # ∎
      }
      where
        open PreElgotMonad A using (T; elgotalgebras)
        module T = Monad T
        _# = λ {X} {A} f → elgotalgebras._# {X} {A} f
    _∘'_ : ∀ {X Y Z : PreElgotMonad} → PreElgotMonad-Morphism Y Z → PreElgotMonad-Morphism X Y → PreElgotMonad-Morphism X Z
    _∘'_ {X} {Y} {Z} f g = record
      { α = αf ∘ᵥ αg
      ; α-η = λ {A} → begin
        (αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ pullʳ (α-η g) ⟩
        αf.η A ∘ TY.η.η A            ≈⟨ α-η f ⟩
        TZ.η.η A                     ∎
      ; α-μ = λ {A} → begin
        (αf.η A ∘ αg.η A) ∘ TX.μ.η A                                                       ≈⟨ pullʳ (α-μ g) ⟩
        αf.η A ∘ TY.μ.η A ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A)                              ≈⟨ pullˡ (α-μ f) ⟩
        (TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ αf.η (TY.F.₀ A)) ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
        TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ (TZ.F.₁ (αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism TZ.F))) ⟩
        TZ.μ.η A ∘ (TZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A)          ≈⟨ refl⟩∘⟨ assoc ⟩
        TZ.μ.η A ∘ TZ.F.₁ ((αf.η A ∘ αg.η A)) ∘  αf.η (TX.F.₀ A) ∘ αg.η (TX.F.₀ A)         ∎
      ; preserves = λ {A} {B} h → begin
        (αf.η B ∘ αg.η B) ∘ (h #X)                   ≈⟨ pullʳ (preserves g h) ⟩
        αf.η B ∘ ((αg.η B +₁ id) ∘ h) #Y            ≈⟨ preserves f ((αg.η B +₁ id) ∘ h) ⟩
        (((αf.η B +₁ id) ∘ (αg.η B +₁ id) ∘ h) #Z) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
        (((αf.η B ∘ αg.η B +₁ id) ∘ h) #Z)          ∎
      }
      where
        module TX = Monad (PreElgotMonad.T X)
        module TY = Monad (PreElgotMonad.T Y)
        module TZ = Monad (PreElgotMonad.T Z)
        _#X = λ {A} {B} f → PreElgotMonad.elgotalgebras._# X {A} {B} f
        _#Y = λ {A} {B} f → PreElgotMonad.elgotalgebras._# Y {A} {B} f
        _#Z = λ {A} {B} f → PreElgotMonad.elgotalgebras._# Z {A} {B} f

        open PreElgotMonad-Morphism using (α-η; α-μ; preserves)

        open PreElgotMonad-Morphism f using () renaming (α to αf)
        open PreElgotMonad-Morphism g using () renaming (α to αg)