Monadic instances for ULift and PLift

In this file we define Monad and IsLawfulMonad instances on PLift and ULift.

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

Functorial action.

Equations

• PLift.map f a = { down := f a.down }

@[simp]

theorem PLift.map_up {α : Sort u} {β : Sort v} (f : α → β) (a : α) : PLift.map f { down := a } = { down := f a }

def PLift.pure {α : Sort u} : α → PLift α

Embedding of pure values.

Equations

• PLift.pure = PLift.up

def PLift.seq {α : Sort u} {β : Sort v} (f : PLift (α → β)) (x : Unit → PLift α) : PLift β

Applicative sequencing.

Equations

• PLift.seq f x = { down := f.down (x ()).down }

@[simp]

theorem PLift.seq_up {α : Sort u} {β : Sort v} (f : α → β) (x : α) : (PLift.seq { down := f } fun (x_1 : Unit) => { down := x }) = { down := f x }

def PLift.bind {α : Sort u} {β : Sort v} (a : PLift α) (f : α → PLift β) : PLift β

Monadic bind.

Equations

• PLift.bind a f = f a.down

@[simp]

theorem PLift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α → PLift β) : PLift.bind { down := a } f = f a

instance PLift.instMonadPLift : Monad PLift

Equations

• PLift.instMonadPLift = Monad.mk

instance PLift.instLawfulFunctorPLiftToFunctorToApplicativeInstMonadPLift : LawfulFunctor PLift

Equations

• PLift.instLawfulFunctorPLiftToFunctorToApplicativeInstMonadPLift = (_ : LawfulFunctor PLift)

instance PLift.instLawfulApplicativePLiftToApplicativeInstMonadPLift : LawfulApplicative PLift

Equations

• PLift.instLawfulApplicativePLiftToApplicativeInstMonadPLift = (_ : LawfulApplicative PLift)

instance PLift.instLawfulMonadPLiftInstMonadPLift : LawfulMonad PLift

Equations

• PLift.instLawfulMonadPLiftInstMonadPLift = (_ : LawfulMonad PLift)

@[simp]

theorem PLift.rec.constant {α : Sort u} {β : Type v} (b : β) : (PLift.rec fun (x : α) => b) = fun (x : PLift α) => b

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

Functorial action.

Equations

• ULift.map f a = { down := f a.down }

@[simp]

theorem ULift.map_up {α : Type u} {β : Type v} (f : α → β) (a : α) : ULift.map f { down := a } = { down := f a }

def ULift.pure {α : Type u} : α → ULift α

Embedding of pure values.

Equations

• ULift.pure = ULift.up

def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift (α → β)) (x : Unit → ULift α) : ULift β

Applicative sequencing.

Equations

• ULift.seq f x = { down := f.down (x ()).down }

@[simp]

theorem ULift.seq_up {α : Type u} {β : Type v} (f : α → β) (x : α) : (ULift.seq { down := f } fun (x_1 : Unit) => { down := x }) = { down := f x }

def ULift.bind {α : Type u} {β : Type v} (a : ULift α) (f : α → ULift β) : ULift β

Monadic bind.

Equations

• ULift.bind a f = f a.down

@[simp]

theorem ULift.bind_up {α : Type u} {β : Type v} (a : α) (f : α → ULift β) : ULift.bind { down := a } f = f a

instance ULift.instMonadULift : Monad ULift

Equations

• ULift.instMonadULift = Monad.mk

instance ULift.instLawfulFunctorULiftToFunctorToApplicativeInstMonadULift : LawfulFunctor ULift

Equations

• ULift.instLawfulFunctorULiftToFunctorToApplicativeInstMonadULift = (_ : LawfulFunctor ULift)

instance ULift.instLawfulApplicativeULiftToApplicativeInstMonadULift : LawfulApplicative ULift

Equations

• ULift.instLawfulApplicativeULiftToApplicativeInstMonadULift = (_ : LawfulApplicative ULift)

instance ULift.instLawfulMonadULiftInstMonadULift : LawfulMonad ULift

Equations

• ULift.instLawfulMonadULiftInstMonadULift = (_ : LawfulMonad ULift)

@[simp]

theorem ULift.rec.constant {α : Type u} {β : Sort v} (b : β) : (ULift.rec fun (x : α) => b) = fun (x : ULift α) => b