mathlib3

chore(category_theory/whiskering): clean up

#1613

Merged