mathlib docs: data.ulift

source

@[simp]

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

plift α → plift β

Functorial action.

Equations

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

source

@[simp]

def plift.pure {α : Sort u} :

α → plift α

Embedding of pure values.

Equations

plift.pure = plift.up

source

@[simp]

def plift.seq {α : Sort u} {β : Sort v} :

plift (α → β) → plift α → plift β

Applicative sequencing.

Equations

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

source

@[simp]

def plift.bind {α : Sort u} {β : Sort v} :

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

ulift α → ulift β

Functorial action.

Equations

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

source

@[simp]

def ulift.pure {α : Type u} :

α → ulift α

Embedding of pure values.

Equations

ulift.pure = ulift.up

source

@[simp]

def ulift.seq {α : Type u} {β : Type v} :

ulift (α → β) → ulift α → ulift β

Applicative sequencing.

Equations

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

source

@[simp]

def ulift.bind {α : Type u} {β : Type v} :

ulift α → (α → 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