mathlib

9d193c59 - feat(category_theory/comm_sq): functors mapping pullback/pushout squares (#14351)

feat(category_theory/comm_sq): functors mapping pullback/pushout squares (#14351) ``` lemma map_is_pullback [preserves_limit (cospan h i) F] (s : is_pullback f g h i) : is_pullback (F.map f) (F.map g) (F.map h) (F.map i) := ... ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com>