mathlib

f9216640 - finished that equivalence of category transfers monoidal structure