# Documentation

Mathlib.Control.ULift

# 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 }
@[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
def PLift.seq {α : Sort u} {β : Sort v} (f : PLift (αβ)) (x : Unit) :

Applicative sequencing.

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

Equations
• = f a.down
@[simp]
theorem PLift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α) :
PLift.bind { down := a } f = f a
@[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 }
@[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
def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift (αβ)) (x : Unit) :

Applicative sequencing.

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