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

import Categories.Morphism.Reasoning as MR

-- Convenient conversion between Kleisli triples and monads.
module Monad.Helper {o ℓ e} {C : Category o ℓ e} where
  open Category C
  open MR C
  open HomReasoning
  open Equiv
  Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
  Kleisli⇒Monad⇒Kleisli K f = begin 
    extend id ∘ extend (unit ∘ f) ≈⟨ sym kleisli.assoc ⟩ 
    extend (extend id ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ kleisli.identityʳ) ⟩
    extend (id ∘ f)               ≈⟨ extend-≈ (identityˡ) ⟩
    extend f                       ∎
    where 
      module kleisli = RMonad K 
      open kleisli using (unit; extend; extend-≈)

  Monad⇒Kleisli⇒Monad : ∀ (M : Monad C) {X Y} (f : X ⇒ Monad.F.₀ M Y) → Monad.F.₁ (Kleisli⇒Monad C (Monad⇒Kleisli C M)) f ≈ Monad.F.₁ M f
  Monad⇒Kleisli⇒Monad M f = begin 
    μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩ 
    μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ monad.identityˡ ⟩ 
    F.₁ f ∎
    where
      module monad = Monad M
      open monad using (F; η; μ)

  F₁⇒extend : ∀ (M : Monad C) {X Y} (f : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) (RMonad.unit (Monad⇒Kleisli C M) ∘ f) ≈ Monad.F.₁ M f
  F₁⇒extend M f = begin 
    μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩ 
    μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩ 
    F.₁ f ∎
    where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ)

  extend⇒F₁ : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend K f ≈ Monad.μ.η (Kleisli⇒Monad C K) _ ∘ Monad.F.₁ (Kleisli⇒Monad C K) f
  extend⇒F₁ K f = begin 
    extend f                      ≈˘⟨ extend-≈ (cancelˡ k-identityʳ) ⟩ 
    extend (extend id ∘ unit ∘ f) ≈⟨ k-assoc ⟩ 
    extend id ∘ extend (unit ∘ f) ∎
    where open RMonad K renaming (assoc to k-assoc; identityʳ to k-identityʳ)

  extend∘F₁ : ∀ (M : Monad C) {X Y Z} (f : Y ⇒ Monad.F.₀ M Z) (g : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) f ∘ Monad.F.₁ M g ≈ RMonad.extend (Monad⇒Kleisli C M) (f ∘ g)
  extend∘F₁ M f g = begin 
    extend f ∘ F.₁ g ≈⟨ (refl⟩∘⟨ sym (F₁⇒extend M g)) ⟩ 
    extend f ∘ extend (unit ∘ g) ≈⟨ k-sym-assoc ⟩ 
    extend (extend f ∘ unit ∘ g) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ 
    extend (f ∘ g) ∎
    where 
      open Monad M using (F)
      open RMonad (Monad⇒Kleisli C M) using (extend; unit; extend-≈) renaming (sym-assoc to k-sym-assoc; identityʳ to k-identityʳ)

  extend∘F₁' : ∀ (K : KleisliTriple C) {X Y Z} (f : Y ⇒ RMonad.F₀ K Z) (g : X ⇒ Y) → RMonad.extend K f ∘ Monad.F.₁ (Kleisli⇒Monad C K) g ≈ RMonad.extend K (f ∘ g)
  extend∘F₁' K f g = begin 
    extend f ∘ F.₁ g ≈⟨ refl ⟩ 
    extend f ∘ extend (unit ∘ g) ≈⟨ sym k-assoc ⟩ 
    extend (extend f ∘ unit ∘ g) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ 
    extend (f ∘ g) ∎
    where
    open Monad (Kleisli⇒Monad C K) using (F; μ)
    open RMonad K using (extend; unit; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)

  F₁∘extend : ∀ (M : Monad C) {X Y Z} (f : Y ⇒ Z) (g : X ⇒ Monad.F.₀ M Y) → Monad.F.₁ M f ∘ RMonad.extend (Monad⇒Kleisli C M) g ≈ RMonad.extend (Monad⇒Kleisli C M) (Monad.F.₁ M f ∘ g)
  F₁∘extend M f g = begin 
    F.₁ f ∘ extend g            ≈⟨ refl ⟩ 
    F.₁ f ∘ μ.η _ ∘ F.₁ g       ≈⟨ extendʳ (sym (μ.commute f)) ⟩ 
    μ.η _ ∘ F.₁ (F.₁ f) ∘ F.₁ g ≈⟨ refl⟩∘⟨ sym F.homomorphism ⟩ 
    extend (F.₁ f ∘ g)          ∎
    where
    open Monad M using (F; μ)
    open RMonad (Monad⇒Kleisli C M) using (extend)

  F₁∘extend' : ∀ (K : KleisliTriple C) {X Y Z} (f : Y ⇒ Z) (g : X ⇒ RMonad.F₀ K Y) → Monad.F.₁ (Kleisli⇒Monad C K) f ∘ RMonad.extend K g ≈ RMonad.extend K (Monad.F.₁ (Kleisli⇒Monad C K) f ∘ g)
  F₁∘extend' K f g = begin 
    F.₁ f ∘ extend g               ≈⟨ refl ⟩ 
    extend (unit ∘ f) ∘ extend g   ≈⟨ sym k-assoc ⟩ 
    extend (extend (unit ∘ f) ∘ g) ≈⟨ refl ⟩ 
    extend (F.₁ f ∘ g)             ∎
    where
    open Monad (Kleisli⇒Monad C K) using (F; μ)
    open RMonad K using (extend; unit) renaming (assoc to k-assoc)

  -- record ExtendsToMonad (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
  --   field
  --     η : NaturalTransformation Id F
  --     μ : NaturalTransformation (F ∘F F) F

  --   module F = Functor F
  --   module η = NaturalTransformation η
  --   module μ = NaturalTransformation μ

  --   open F

  --   field
  --     assoc : ∀ {X : Obj} → μ.η X ∘ F₁ (μ.η X) ≈ μ.η X ∘ μ.η (F₀ X)
  --     sym-assoc : ∀ {X : Obj} → μ.η X ∘ μ.η (F₀ X) ≈ μ.η X ∘ F₁ (μ.η X)
  --     identityˡ : ∀ {X : Obj} → μ.η X ∘ F₁ (η.η X) ≈ id
  --     identityʳ : ∀ {X : Obj} → μ.η X ∘ η.η (F₀ X) ≈ id

  -- ExtendsToMonad⇒Monad : ∀ (F : Endofunctor C) → ExtendsToMonad F → Monad C
  -- ExtendsToMonad⇒Monad F extendsToMonad = record
  --   { F = F
  --   ; η = M.η
  --   ; μ = M.μ
  --   ; assoc = M.assoc
  --   ; sym-assoc = M.sym-assoc
  --   ; identityˡ = M.identityˡ
  --   ; identityʳ = M.identityʳ
  --   }
  --   where 
  --     module M = ExtendsToMonad extendsToMonad