Commit 2022-05-24 12:33 9d193c59

View on Github →

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) := ...

Estimated changes

added structure category_theory.comm_sq