Commit 2025-06-05 14:45 d7a2912f

chore(CategoryTheory/Opposites): pseudofunctoriality of opposites (#24662) We record lemmas dealing with pseudofunctoriality of the construction C ↦ Cᵒᵖ. More precisely, we give isomorphisms of the form (F ⋙ G).op ≅ F.op ⋙ G.op, and we study how they interact with constructions such as whiskering, unitors, and associators.