theorem CategoryTheory.Functor.reflect_commSq {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) [F.Faithful] {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {i : Z ⟶ W} : CommSq (F.map f) (F.map g) (F.map h) (F.map i) → CommSq f g h i