mathlib

ad080011 - feat(category_theory/limits): opposites of limit pullback cones (#14526)

feat(category_theory/limits): opposites of limit pullback cones (#14526) Among other similar statements, this PR associates a `pullback_cone f g` to a `pushout_cocone f.op g.op`, and it is a limit pullback cone if the original cocone is a colimit cocone. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>