LawfulMonadLift and LawfulMonadLiftT

This module provides classes asserting that MonadLift and MonadLiftT are lawful, which means that monadLift is compatible with pure and bind.

class LawfulMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) [Monad m] [Monad n] [inst : MonadLift m n] : Prop

The MonadLift typeclass only contains the lifting operation. LawfulMonadLift further asserts that lifting commutes with pure and bind:

monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f

• monadLift_pure {α : Type u} (a : α) : MonadLift.monadLift (pure a) = pure a

  Lifting preserves pure

• monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) : MonadLift.monadLift (ma >>= f) = do let x ← MonadLift.monadLift ma MonadLift.monadLift (f x)

  Lifting preserves bind

class LawfulMonadLiftT (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n] [inst : MonadLiftT m n] : Prop

The MonadLiftT typeclass only contains the transitive lifting operation. LawfulMonadLiftT further asserts that lifting commutes with pure and bind:

monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f

• monadLift_pure {α : Type u} (a : α) : monadLift (pure a) = pure a

  Lifting preserves pure

• monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) : monadLift (ma >>= f) = do let x ← monadLift ma monadLift (f x)

  Lifting preserves bind