Typeclass for lawful 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.LawfulMonadLiftBindFunction {m : Type u → Type v} {n : Type w → Type x} [Monad m] [Monad n] (liftBind : (γ : Type u) → (δ : Type w) → (γ → n δ) → m γ → n δ) : Prop

• liftBind_pure {γ : Type u} {δ : Type w} (f : γ → n δ) (a : γ) : liftBind γ δ f (pure a) = f a
• liftBind_bind {β γ : Type u} {δ : Type w} (f : γ → n δ) (x : m β) (g : β → m γ) : liftBind γ δ f (x >>= g) = liftBind β δ (fun (b : β) => liftBind γ δ f (g b)) x

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

@[reducible, inline]

abbrev Std.Internal.idToMonad {m : Type u → Type v} [Monad m] ⦃α : Type u⦄ (x : Id α) : m α

Equations

• Std.Internal.idToMonad x = pure x.run

def Std.Internal.LawfulMonadLiftFunction.idToMonad {m : Type u → Type v} [Monad m] [LawfulMonad m] : LawfulMonadLiftFunction Internal.idToMonad

Equations

• ⋯ = ⋯

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

instance Std.Internal.instLawfulMonadLiftFunctionOfLawfulMonadLiftBindFunctionBindOfLawfulMonad {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} [LawfulMonadLiftBindFunction fun (x x_1 : Type u) (f : x → n x_1) (x_2 : m x) => lift x_2 >>= f] [LawfulMonad n] : LawfulMonadLiftFunction lift

def Std.Internal.LawfulMonadLiftBindFunction.id {m : Type u → Type v} [Monad m] [LawfulMonad m] : LawfulMonadLiftBindFunction fun (x : Type u_1) (x_1 : Type u) (f : x → m x_1) (x_2 : Id x) => f x_2.run

Equations

• ⋯ = ⋯

instance Std.Internal.instLawfulMonadLiftBindFunctionBindMonadLiftOfLawfulMonadLiftTOfLawfulMonad {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [LawfulMonad n] : LawfulMonadLiftBindFunction fun (γ δ : Type u) (f : γ → n δ) (x : m γ) => monadLift x >>= f

instance Std.Internal.instLawfulMonadLiftBindFunctionIdRunOfLawfulMonad {n : Type u → Type w} [Monad n] [LawfulMonad n] : LawfulMonadLiftBindFunction fun (γ : Type u_1) (δ : Type u) (f : γ → n δ) (x : Id γ) => f x.run