mathlib

6d25f3ae - feat(category_theory/opposites): Adds equivalences for functor categories. (#7505)

feat(category_theory/opposites): Adds equivalences for functor categories. (#7505) This PR adds the following equivalences for categories `C` and `D`: 1. `(C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ` induced by `op` and `unop`. 2. `(Cᵒᵖ ⥤ D)ᵒᵖ ≌ (C ⥤ Dᵒᵖ)` induced by `left_op` and `right_op`.