∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X}
  {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.ofArrows.h hg)
      (CategoryTheory.CategoryStruct.comp (f (CategoryTheory.Sieve.ofArrows.i hg)) h) =
    CategoryTheory.CategoryStruct.comp g h