no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsLimit (cospan h i) F
inst✝ : Faithful F
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)
simpa only [F.map_comp] using H.w