Documentation

Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

theorem CategoryTheory.Functor.reflect_isPullback {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {X Y Z W : C} (f : X Y) (g : X Z) (h : Y W) (i : Z W) [rl : Limits.ReflectsLimit (Limits.cospan h i) F] [F.Faithful] :
IsPullback (F.map f) (F.map g) (F.map h) (F.map i)IsPullback f g h i