Equational Lifting Monads

An equational lifting monad is a commutative monad satisfying one additional equational law

module Monad.EquationalLifting {o ℓ e} {C : Category o ℓ e} (cartesian : Cartesian C) where
  open Category C
  open Cartesian cartesian using (products)
  open BinaryProducts products
  open CartesianMonoidal cartesian using (monoidal)
  open Symmetric (symmetric C cartesian) using (braided)

  IsEquationalLiftingMonad : ∀ (CM : CommutativeMonad braided) → Set (o ⊔ e)
  IsEquationalLiftingMonad CM = ∀ {X} → τ.η _ ∘ Δ {M.F.₀ X} ≈ M.F.₁ ⟨ M.η.η X , id ⟩
    where
      open CommutativeMonad CM
      module τ = strengthen