mathlib

52a270e2 - feat(category_theory/limits): bicartesian squares (#14375)

feat(category_theory/limits): bicartesian squares (#14375) ``` X ⊞ Y --fst--> X | | snd 0 | | v v Y Co-authored-by: Scott Morrison <scott.morrison@gmail.com>