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