# Monadic instances for ULift and PLift#

In this file we define Monad and IsLawfulMonad instances on PLift and ULift.

def PLift.map {α : Sort u} {β : Sort v} (f : αβ) (a : ) :

Functorial action.

Equations
• = { down := f a.down }
Instances For
@[simp]
theorem PLift.map_up {α : Sort u} {β : Sort v} (f : αβ) (a : α) :
PLift.map f { down := a } = { down := f a }
def PLift.pure {α : Sort u} :
α

Embedding of pure values.

Equations
• PLift.pure = PLift.up
Instances For
def PLift.seq {α : Sort u} {β : Sort v} (f : PLift (αβ)) (x : Unit) :

Applicative sequencing.

Equations
• f.seq x = { down := f.down (x ()).down }
Instances For
@[simp]
theorem PLift.seq_up {α : Sort u} {β : Sort v} (f : αβ) (x : α) :
({ down := f }.seq fun (x_1 : Unit) => { down := x }) = { down := f x }
def PLift.bind {α : Sort u} {β : Sort v} (a : ) (f : α) :

Equations
• a.bind f = f a.down
Instances For
@[simp]
theorem PLift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α) :
{ down := a }.bind f = f a
Equations
Equations
@[simp]
theorem PLift.rec.constant {α : Sort u} {β : Type v} (b : β) :
(PLift.rec fun (x : α) => b) = fun (x : ) => b
def ULift.map {α : Type u} {β : Type v} (f : αβ) (a : ) :

Functorial action.

Equations
• = { down := f a.down }
Instances For
@[simp]
theorem ULift.map_up {α : Type u} {β : Type v} (f : αβ) (a : α) :
ULift.map f { down := a } = { down := f a }
def ULift.pure {α : Type u} :
α

Embedding of pure values.

Equations
• ULift.pure = ULift.up
Instances For
def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift (αβ)) (x : Unit) :

Applicative sequencing.

Equations
• f.seq x = { down := f.down (x ()).down }
Instances For
@[simp]
theorem ULift.seq_up {α : Type u} {β : Type v} (f : αβ) (x : α) :
({ down := f }.seq fun (x_1 : Unit) => { down := x }) = { down := f x }
def ULift.bind {α : Type u} {β : Type v} (a : ) (f : α) :