{-# OPTIONS --safe #-}

open import Categories.Category.Core using (Category)
open import Categories.Category.Distributive using (Distributive)
open import Categories.Monad.EquationalLifting using (EquationalLifting)
open import Categories.Category.Construction.Kleisli using (Kleisli)
open import Categories.Category.Restriction using (Restriction)
open import Categories.Category.Restriction.Construction.Kleisli using (Kleisli-Restriction)

import Monad.Instance.K as MIK

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

  open import Monad.Instance.K.EquationalLifting distributive MK

  KRestriction : Restriction (Kleisli monadK)
  KRestriction = Kleisli-Restriction cartesian KEquationalLiftingMonad