Commit 2022-07-28 00:18 00e7ca52
View on Github →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.