mathlib3

bdab9072 - porting functoriality.lean ' (wip)