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.Monad.Strong
open import Categories.Category.Core
open import Categories.Category.Distributive
open import Data.Product using (_,_)

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

-- The (Functor-)Category of Strong Pre-Elgot Monads.

module Category.Construction.StrongPreElgotMonads {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
open import Category.Distributive.Helper distributive
open import Algebra.Elgot cocartesian
open import Monad.StrongPreElgot distributive
open Category C
open HomReasoning
open Equiv
open M C
open MR C

module _ (P S : StrongPreElgotMonad) where
  private
    open StrongPreElgotMonad P using () renaming (SM to SMP; elgotalgebras to P-elgots)
    open StrongPreElgotMonad S using () renaming (SM to SMS; elgotalgebras to S-elgots)
    open StrongMonad SMP using () renaming (M to TP; strengthen to strengthenP)
    open StrongMonad SMS using () renaming (M to TS; strengthen to strengthenS)
    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 StrongPreElgotMonad-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)
      α-strength : ∀ {X Y}
        → α.η (X × Y) ∘ strengthenP.η (X , Y) ≈ strengthenS.η (X , Y) ∘ (id ⁂ α.η Y)
      α-preserves : ∀ {X A} (f : X ⇒ TP.F.₀ A + X) → α.η A ∘ f #P ≈ ((α.η A +₁ id) ∘ f) #S

StrongPreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
StrongPreElgotMonads = record
  { Obj = StrongPreElgotMonad 
  ; _⇒_ = StrongPreElgotMonad-Morphism
  ; _≈_ = λ f g → (StrongPreElgotMonad-Morphism.α f) ≃ (StrongPreElgotMonad-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 : StrongPreElgotMonad} → StrongPreElgotMonad-Morphism A A
    id' {A} = record
      { α = ntHelper (record { η = λ _ → id ; commute = λ _ → id-comm-sym }) 
      ; α-η = identityˡ 
      ; α-μ = sym (begin
          M.μ.η _ ∘ M.F.₁ id ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
          M.μ.η _ ∘ M.F.₁ id       ≈⟨ elimʳ M.F.identity ⟩
          M.μ.η _                   ≈⟨ sym identityˡ ⟩
          id ∘ M.μ.η _             ∎)
      ; α-strength = λ {X} {Y} → sym (begin 
        strengthen.η (X , Y) ∘ (id ⁂ id)       ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym M.F.identity)) ⟩ 
        strengthen.η (X , Y) ∘ (id ⁂ M.F.₁ id) ≈⟨ strengthen.commute (id , id) ⟩ 
        M.F.₁ (id ⁂ id) ∘ strengthen.η (X , Y) ≈⟨ (M.F.F-resp-≈ (⟨⟩-unique id-comm id-comm) ○ M.F.identity) ⟩∘⟨refl ⟩ 
        id ∘ strengthen.η (X , Y)               ∎) 
      ; α-preserves = λ f → begin
          id ∘ f #            ≈⟨ identityˡ ⟩
          f #                  ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
          ((id +₁ id) ∘ f) # ∎
      }
      where
        open StrongPreElgotMonad A using (SM; elgotalgebras)
        open StrongMonad SM using (M; strengthen)
        _# = λ {X} {A} f → elgotalgebras._# {X} {A} f
    _∘'_ : ∀ {X Y Z : StrongPreElgotMonad} → StrongPreElgotMonad-Morphism Y Z → StrongPreElgotMonad-Morphism X Y → StrongPreElgotMonad-Morphism X Z
    _∘'_ {X} {Y} {Z} f g = record
      { α = αf ∘ᵥ αg
      ; α-η = λ {A} → begin
        (αf.η A ∘ αg.η A) ∘ MX.η.η A ≈⟨ pullʳ (α-η g) ⟩
        αf.η A ∘ MY.η.η A            ≈⟨ α-η f ⟩
        MZ.η.η A                     ∎
      ; α-μ = λ {A} → begin
        (αf.η A ∘ αg.η A) ∘ MX.μ.η A                                                       ≈⟨ pullʳ (α-μ g) ⟩
        αf.η A ∘ MY.μ.η A ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A)                              ≈⟨ pullˡ (α-μ f) ⟩
        (MZ.μ.η A ∘ MZ.F.₁ (αf.η A) ∘ αf.η (MY.F.₀ A)) ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
        MZ.μ.η A ∘ MZ.F.₁ (αf.η A) ∘ (MZ.F.₁ (αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism MZ.F))) ⟩
        MZ.μ.η A ∘ (MZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A)          ≈⟨ refl⟩∘⟨ assoc ⟩
        MZ.μ.η A ∘ MZ.F.₁ ((αf.η A ∘ αg.η A)) ∘  αf.η (MX.F.₀ A) ∘ αg.η (MX.F.₀ A)         ∎
      ; α-strength = λ {A} {B} → begin 
        (αf.η (A × B) ∘ αg.η (A × B)) ∘ strengthenX.η (A , B)     ≈⟨ pullʳ (α-strength g) ⟩
        αf.η (A × B) ∘ strengthenY.η (A , B) ∘ (id ⁂ αg.η B)     ≈⟨ pullˡ (α-strength f) ⟩
        (strengthenZ.η (A , B) ∘ (id ⁂ αf.η B)) ∘ (id ⁂ αg.η B) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
        strengthenZ.η (A , B) ∘ (id ⁂ (αf.η B ∘ αg.η B))         ∎
      ; α-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-≈ (StrongPreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
        (((αf.η B ∘ αg.η B +₁ id) ∘ h) #Z)          ∎
      }
      where
        open StrongPreElgotMonad X using () renaming (SM to SMX)
        open StrongPreElgotMonad Y using () renaming (SM to SMY)
        open StrongPreElgotMonad Z using () renaming (SM to SMZ)
        open StrongMonad SMX using () renaming (M to MX; strengthen to strengthenX)
        open StrongMonad SMY using () renaming (M to MY; strengthen to strengthenY)
        open StrongMonad SMZ using () renaming (M to MZ; strengthen to strengthenZ)
        _#X = λ {A} {B} f → StrongPreElgotMonad.elgotalgebras._# X {A} {B} f
        _#Y = λ {A} {B} f → StrongPreElgotMonad.elgotalgebras._# Y {A} {B} f
        _#Z = λ {A} {B} f → StrongPreElgotMonad.elgotalgebras._# Z {A} {B} f

        open StrongPreElgotMonad-Morphism using (α-η; α-μ; α-strength; α-preserves)

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