mathlib3 documentation

control.ulift

Monadic instances for ulift and plift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α) :
plift.map f {down := a} = {down := f a}
@[protected, simp]
def plift.pure {α : Sort u} :
α plift α

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 : α plift β) :

Monadic bind.

Equations
@[simp]
theorem plift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α plift β) :
{down := a}.bind f = f a
@[protected, instance]
Equations
@[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 : α) :
ulift.map f {down := a} = {down := f a}
@[protected, simp]
def ulift.pure {α : Type u} :
α ulift α

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 : α ulift β) :

Monadic bind.

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