mathlib

31f13771 - define the ends functors, _again_