∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X),
  S.arrows f → ∀ (Z : Cᵒᵖ) (g : (CategoryTheory.yoneda.obj Y).obj Z), S.arrows (CategoryTheory.CategoryStruct.comp g f)