mathlib documentation

core / init.control.functor

@[class]
structure functor (f : Type uType v) :
Type (max (u+1) v)
  • map : Π {α β : Type ?}, (α → β)f αf β
  • map_const : Π {α β : Type ?}, α → f βf α
Instances
def functor.map_const_rev {f : Type uType v} [functor f] {α β : Type u} :
f βα → f α
Equations