mathlib

00e7ca52 - feat(category_theory/limits/shapes/comm_sq): opposites of is_pullback and is_pushout (#15269)

feat(category_theory/limits/shapes/comm_sq): opposites of is_pullback and is_pushout (#15269) This PR shows that the dual of a pushout commutative square is a pullback square, and similar other results. The most basic `comm_sq` API is also moved to a separate file with fewer dependencies so as to prepare for a refactor of lifting properties which shall be based on `comm_sq`.