Commit 2023-09-23 22:49 37ef3d5d

chore(CategoryTheory): swapping the names of opOp and unopUnop (#7344) This PR swaps the names of opOp and unopUnop which are the functors of the equivalence of categories opOpEquivalence : Cᵒᵖᵒᵖ ≌ C. As Opposite.op is the map C → Cᵒᵖ, the functor C ⥤ Cᵒᵖᵒᵖ should be named opOp and the functor Cᵒᵖᵒᵖ ⥤ C should be named unopUnop. It was previously the opposite; this PR fixes this.