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