open import Categories.Category.Core
open import Categories.Category.Distributive
open import Categories.Monad.Commutative
open import Monad.EquationalLifting

import Monad.Instance.K as MIK

-- K satisfies the equational lifting property

module Monad.Instance.K.EquationalLifting {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (MK : MIK.MonadK distributive) where
open import Category.Distributive.Helper distributive
open import Monad.Instance.K.Commutative distributive MK

KEquationalLifting : EquationalLifting cartesian KCommutativeMonad
KEquationalLifting = equationalLifting

KEquationalLiftingMonad : EquationalLiftingMonad cartesian
KEquationalLiftingMonad = record 
  { commutativeMonad = KCommutativeMonad
  ; equationalLifting = KEquationalLifting
  }