mathlib

f585ce54 - feat(category_theory): monoidal natural transformations and discrete monoidal categories (#4112)