no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
⊢ S.arrows f ↔ pullback f S = ⊤
rw [← id_mem_iff_eq_top, pullback_apply, id_comp]