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.

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

Functorial action.

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

Embedding of pure values.

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

Applicative sequencing.

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

Monadic bind.

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

Functorial action.

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

Embedding of pure values.

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

Applicative sequencing.

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

Monadic bind.

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