mathlib docs: data.ulift

source

@[simp]

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

plift β

Functorial action.

Equations

plift.map f {down := a} = {down := f a}

source

@[simp]

def plift.pure {α : Sort u} (a : α) :

plift α

Embedding of pure values.

Equations

plift.pure = plift.up

source

@[simp]

def plift.seq {α : Sort u} {β : Sort v} (a : plift (α → β)) (a_1 : plift α) :

plift β

Applicative sequencing.

Equations

{down := f}.seq {down := a} = {down := f a}

source

@[simp]

def plift.bind {α : Sort u} {β : Sort v} (a : plift α) (a_1 : α → plift β) :

plift β

Monadic bind.

Equations

{down := a}.bind f = f a

source

@[instance]

def plift.monad :

monad plift

Equations

plift.monad = monad.mk

source

@[instance]

def plift.is_lawful_functor :

is_lawful_functor plift

source

@[instance]

def plift.is_lawful_applicative :

is_lawful_applicative plift

source

@[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

@[simp]

def ulift.map {α : Type u} {β : Type v} (f : α → β) (a : ulift α) :

ulift β

Functorial action.

Equations

ulift.map f {down := a} = {down := f a}

source

@[simp]

def ulift.pure {α : Type u} (a : α) :

ulift α

Embedding of pure values.

Equations

ulift.pure = ulift.up

source

@[simp]

def ulift.seq {α : Type u} {β : Type v} (a : ulift (α → β)) (a_1 : ulift α) :

ulift β

Applicative sequencing.

Equations

{down := f}.seq {down := a} = {down := f a}

source

@[simp]

def ulift.bind {α : Type u} {β : Type v} (a : ulift α) (a_1 : α → ulift β) :

ulift β

Monadic bind.

Equations

{down := a}.bind f = {down := (f a).down}

source

@[instance]

def ulift.monad :

monad ulift

Equations

ulift.monad = monad.mk

source

@[instance]

def ulift.is_lawful_functor :

is_lawful_functor ulift

source

@[instance]

def ulift.is_lawful_applicative :

is_lawful_applicative ulift

source

@[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