Lawful version of MonadLift

This file defines the LawfulMonadLift(T) class, which adds laws to the MonadLift(T) class.

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

theorem monadLift_map {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) : monadLift (f <$> ma) = f <$> monadLift ma

theorem monadLift_seq {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) : monadLift (mf <*> ma) = monadLift mf <*> monadLift ma

theorem monadLift_seqLeft {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) : monadLift (x <* y) = monadLift x <* monadLift y

theorem monadLift_seqRight {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) : monadLift (x *> y) = monadLift x *> monadLift y

We duplicate the theorems for monadLift to liftM since rw matches on syntax only.

@[simp]

theorem liftM_pure {m : Type u_1 → Type u_3} {n : Type u_1 → Type u_2} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α : Type u_1} (a : α) : liftM (pure a) = pure a

@[simp]

theorem liftM_bind {m : Type u_1 → Type u_3} {n : Type u_1 → Type u_2} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} (ma : m α) (f : α → m β) : liftM (ma >>= f) = do let a ← liftM ma liftM (f a)

@[simp]

theorem liftM_map {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) : liftM (f <$> ma) = f <$> liftM ma

@[simp]

theorem liftM_seq {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) : liftM (mf <*> ma) = liftM mf <*> liftM ma

@[simp]

theorem liftM_seqLeft {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) : liftM (x <* y) = liftM x <* liftM y

@[simp]

theorem liftM_seqRight {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) : liftM (x *> y) = liftM x *> liftM y

instance instLawfulMonadLiftTOfLawfulMonadLift (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [Monad m] [Monad n] [Monad o] [MonadLift n o] [MonadLiftT m n] [LawfulMonadLift n o] [LawfulMonadLiftT m n] : LawfulMonadLiftT m o

instance instLawfulMonadLiftT (m : Type u_1 → Type u_2) [Monad m] : LawfulMonadLiftT m m

instance StateT.instLawfulMonadLift {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {σ : Type u_1} : LawfulMonadLift m (StateT σ m)

instance ReaderT.instLawfulMonadLift {m : Type u_1 → Type u_2} [Monad m] {ρ : Type u_1} : LawfulMonadLift m (ReaderT ρ m)

@[simp]

theorem OptionT.lift_pure {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {α : Type u_1} (a : α) : OptionT.lift (pure a) = pure a

@[simp]

theorem OptionT.lift_bind {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {α β : Type u_1} (ma : m α) (f : α → m β) : OptionT.lift (ma >>= f) = do let a ← OptionT.lift ma OptionT.lift (f a)

instance OptionT.instLawfulMonadLift {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] : LawfulMonadLift m (OptionT m)

@[simp]

theorem ExceptT.lift_bind {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {α β ε : Type u_1} (ma : m α) (f : α → m β) : ExceptT.lift (ma >>= f) = do let a ← ExceptT.lift ma ExceptT.lift (f a)

instance ExceptT.instLawfulMonadLift {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {ε : Type u_1} : LawfulMonadLift m (ExceptT ε m)

instance ExceptT.instLawfulMonadLiftExcept {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {ε : Type u_1} : LawfulMonadLift (Except ε) (ExceptT ε m)

instance StateRefT'.instLawfulMonadLift {m : Type → Type} {ω σ : Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m)

instance StateCpsT.instLawfulMonadLiftOfLawfulMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonadLift m (StateCpsT σ m)

instance ExceptCpsT.instLawfulMonadLiftOfLawfulMonad {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT ε m)

instance Id.instMonadLiftOfPure_batteries {m : Type u_1 → Type u_2} [Pure m] : MonadLift Id m

The pure operation of a monad m can be seen as a lifting operation from Id to m.

Equations

• Id.instMonadLiftOfPure_batteries = { monadLift := fun {α : Type ?u.21} => pure }

instance Id.instLawfulMonadLiftOfLawfulMonad {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] : LawfulMonadLift Id m

The lifting from Id to a lawful monad m induced by pure is lawful.