mathlib documentation

data.ulift

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

Functorial action.

Equations
@[simp]
def plift.pure {α : Sort u} :
α → plift α

Embedding of pure values.

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

Applicative sequencing.

Equations
@[simp]
def plift.bind {α : Sort u} {β : Sort v} :
plift α(α → plift β)plift β

Monadic bind.

Equations
@[instance]

Equations
@[simp]
theorem plift.rec.constant {α : Sort u} {β : Type v} (b : β) :
plift.rec (λ (_x : α), b) = λ (_x : plift α), b

@[simp]
def ulift.map {α : Type u} {β : Type v} :
(α → β)ulift αulift β

Functorial action.

Equations
@[simp]
def ulift.pure {α : Type u} :
α → ulift α

Embedding of pure values.

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

Applicative sequencing.

Equations
@[simp]
def ulift.bind {α : Type u} {β : Type v} :
ulift α(α → ulift β)ulift β

Monadic bind.

Equations
@[instance]

Equations
@[simp]
theorem ulift.rec.constant {α : Type u} {β : Sort v} (b : β) :
ulift.rec (λ (_x : α), b) = λ (_x : ulift α), b