mathlib3

refactor(category_theory/opposites): Make `opposite` irreducible

#627

Merged