mathlib3

52a454af - feat(category_theory/limits): pushouts and pullbacks in the opposite category (#13495)

feat(category_theory/limits): pushouts and pullbacks in the opposite category (#13495) This PR adds duality isomorphisms for the categories `wide_pushout_shape`, `wide_pullback_shape`, `walking_span`, `walking_cospan` and produce pullbacks/pushouts in the opposite category when pushouts/pullbacks exist.