feat(category_theory/limits): pullback squares (#14220)
Per [zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/pushout.20of.20biprod.2Efst.20and.20biprod.2Esnd.20is.20zero).
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
