mathlib

13046edf - delete `equivalence` and add a partial proof that equivalence of category induces equivalence of Mon_