mathlib3 documentation

core / init.control.functor

@[reducible]
def functor.map_const_rev {f : Type u Type v} [functor f] {α β : Type u} :
f β α f α
Equations