mathlib documentation

core / init.control.functor

@[class]

structure functor (f : Type u → Type v) :

Type (max (u+1) v)

map : Π {α β : Type ?}, (α → β) → f α → f β
map_const : Π {α β : Type ?}, α → f β → f α

Instances

def functor.map_const_rev {f : Type u → Type v} [functor f] {α β : Type u} :

f β → α → f α

Equations

functor.map_const_rev = λ (a : f β) (b : α), b <$ a