Typeclass for lawfule monad lifting functions

This module provides a typeclass LawfulMonadLiftFunction f that asserts that a function f mapping values from one monad to another monad commutes with pure and bind. This equivalent to the requirement that the MonadLift(T) instance induced by f admits a LawfulMonadLift(T) instance.

class Std.Internal.LawfulMonadLiftFunction {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] (lift : ⦃α : Type u⦄ → m α → n α) : Prop

• lift_pure {α : Type u} (a : α) : lift (pure a) = pure a
• lift_bind {α β : Type u} (ma : m α) (f : α → m β) : lift (ma >>= f) = do let x ← lift ma lift (f x)

instance Std.Internal.instLawfulMonadLiftFunctionId {m : Type u → Type v} [Monad m] : LawfulMonadLiftFunction fun ⦃α : Type u⦄ => id

instance Std.Internal.instLawfulMonadLiftFunctionMonadLiftOfLawfulMonadLiftT {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : LawfulMonadLiftFunction fun ⦃α : Type u⦄ => monadLift

theorem Std.Internal.LawfulMonadLiftFunction.lift_map {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftFunction lift] (f : α → β) (ma : m α) : lift (f <$> ma) = f <$> lift ma

theorem Std.Internal.LawfulMonadLiftFunction.lift_seq {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftFunction lift] (mf : m (α → β)) (ma : m α) : lift (mf <*> ma) = lift mf <*> lift ma

theorem Std.Internal.LawfulMonadLiftFunction.lift_seqLeft {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftFunction lift] (x : m α) (y : m β) : lift (x <* y) = lift x <* lift y

theorem Std.Internal.LawfulMonadLiftFunction.lift_seqRight {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftFunction lift] (x : m α) (y : m β) : lift (x *> y) = lift x *> lift y

def Std.Internal.instMonadLiftOfFunction {m : Type u → Type v} {n : Type u → Type w} {lift : ⦃α : Type u⦄ → m α → n α} : MonadLift m n

Equations

• Std.Internal.instMonadLiftOfFunction = { monadLift := fun {α : Type ?u.22} => lift }

instance Std.Internal.instLawfulMonadLiftOfLawfulMonadLiftFunction {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} [LawfulMonadLiftFunction lift] : LawfulMonadLift m n