Commit 2026-03-24 19:17 cf534780

feat(CategoryTheory/Limits/Cones): use to_dual (#35031) This PR uses to_dual to generate Cocone from Cone. Notes:

• Sadly, it is not possible to translate cones : Cᵒᵖ ⥤ Type max u₁ v₃ and cocones : C ⥤ Type max u₁ v₃ (and similarly yoneda and coyoneda), because one version has ᵒᵖ in the type and the other doesn't. To allow dualizing Cone.extend, I've inlined the definition of Cone.extensions.
• This PR makes many changes in other files where to_dual tags were missing. Only the minimal necessary changes have been made. Those files may be extended with more to_dual tags in future PRs.
• Cone.extendIso and Cocone.extendIso weren't compatible for to_dual because they were the other way around. I chose to swap the direction of the isomorphisms in Cone.extendIso. Similarly precomposeEquivalence and postComposeEquivalence weren't compatible. I chose to swap the direction of an isomorphism in precomposeEquivalence. These changes required a few adaptations in Mathlib.CategoryTheory.Limits.IsLimit and elsewhere.