monoidal-categories-reboot (WIP) This is a work-in-progress formalization of monoidal categories depending only on mathlib.