open import Level
open import Data.Product using (_,_)
open import Categories.Category.Core
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Product using () renaming (_⁂_ to _✢_)
open import Categories.Monad hiding (id)
open import Categories.Monad.Strong
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation hiding (id)
open import Categories.Object.Terminal using (Terminal)

module Monad.Strong.Helper {o ℓ e} {C : Category o ℓ e} (cartesian : Cartesian C) where
open Category C
open Cartesian cartesian
open BinaryProducts products hiding (η)
open CartesianMonoidal cartesian using (monoidal)

record ExtendsToStrongMonad (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
  field
    η : NaturalTransformation idF F
    μ : NaturalTransformation (F ∘F F) F
    τ : NaturalTransformation (-×- ∘F (idF ✢ F)) (F ∘F -×-)

  module F = Functor F
  module η = NaturalTransformation η
  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

  field
    τ-identityˡ : ∀ {A : Obj} → F₁ π₂ ∘ τ.η (Terminal.⊤ terminal , A) ≈ π₂
    τ-η-comm : ∀ {A B : Obj} → τ.η (A , B) ∘ (id ⁂ η.η B) ≈ η.η (A × B)
    τ-μ-η-comm : ∀ {A B : Obj} → μ.η (A × B) ∘ F₁ (τ.η (A , B)) ∘ τ.η (A , F₀ B) ≈ τ.η (A , B) ∘ (id ⁂ μ.η B)
    τ-strength-assoc : ∀ {A B C : Obj} → F₁ assocˡ ∘ τ.η (A × B , C) ≈ τ.η (A , B × C) ∘ (id ⁂ τ.η (B , C)) ∘ assocˡ

ExtendsToStrongMonad⇒StrongMonad : ∀ (F : Endofunctor C) → ExtendsToStrongMonad F → StrongMonad monoidal
ExtendsToStrongMonad⇒StrongMonad F extends = record 
  { M = record
    { F = F
    ; η = E.η
    ; μ = E.μ
    ; assoc = E.assoc
    ; sym-assoc = E.sym-assoc
    ; identityˡ = E.identityˡ
    ; identityʳ = E.identityʳ
    } 
  ; strength = record
    { strengthen = E.τ
    ; identityˡ = E.τ-identityˡ
    ; η-comm = E.τ-η-comm
    ; μ-η-comm = E.τ-μ-η-comm
    ; strength-assoc = E.τ-strength-assoc
    } 
  }
  where 
    module E = ExtendsToStrongMonad extends

record IsStrongMonadMorphism (M : StrongMonad monoidal) (N : StrongMonad monoidal) (α : NaturalTransformation (StrongMonad.M.F M) (StrongMonad.M.F N)) : Set (o ⊔ ℓ ⊔ e) where
  private
    module α = NaturalTransformation α
    module M = Monad (StrongMonad.M M)
    module N = Monad (StrongMonad.M N)
  open Strength (StrongMonad.strength M) using () renaming (strengthen to τ₁)
  open Strength (StrongMonad.strength N) using () renaming (strengthen to τ₂)
  field
    respects-η : ∀ {X : Obj} → α.η X ∘ M.η.η X ≈ N.η.η X
    respects-μ : ∀ {X : Obj} → α.η X ∘ M.μ.η X ≈ N.μ.η X ∘ α.η (N.F.₀ X) ∘ M.F.₁ (α.η X)
    respects-τ : ∀ {X Y : Obj} → α.η (X × Y) ∘ τ₁.η (X , Y) ≈ τ₂.η (X , Y) ∘ (id ⁂ α.η Y)