control.ulift

# Monadic instances for ulift and plift#

In this file we define monad and is_lawful_monad instances on plift and ulift.

@[protected]
def plift.map {α : Sort u} {β : Sort v} (f : α → β) (a : plift α) :

Functorial action.

Equations
@[simp]
theorem plift.map_up {α : Sort u} {β : Sort v} (f : α → β) (a : α) :
{down := a} = {down := f a}
@[protected, simp]
def plift.pure {α : Sort u} :
α →

Embedding of pure values.

Equations
@[protected]
def plift.seq {α : Sort u} {β : Sort v} (f : plift (α → β)) (x : plift α) :

Applicative sequencing.

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

Equations
@[simp]
theorem plift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α → ) :
{down := a}.bind f = f a
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem plift.rec.constant {α : Sort u} {β : Type v} (b : β) :
plift.rec (λ (_x : α), b) = λ (_x : plift α), b
@[protected]
def ulift.map {α : Type u} {β : Type v} (f : α → β) (a : ulift α) :

Functorial action.

Equations
@[simp]
theorem ulift.map_up {α : Type u} {β : Type v} (f : α → β) (a : α) :
{down := a} = {down := f a}
@[protected, simp]
def ulift.pure {α : Type u} :
α →

Embedding of pure values.

Equations
@[protected]
def ulift.seq {α : Type u} {β : Type v} (f : ulift (α → β)) (x : ulift α) :

Applicative sequencing.

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

Equations
@[simp]
theorem ulift.bind_up {α : Type u} {β : Type v} (a : α) (f : α → ) :
{down := a}.bind f = f a
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem ulift.rec.constant {α : Type u} {β : Sort v} (b : β) :
ulift.rec (λ (_x : α), b) = λ (_x : ulift α), b