∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F),
  (CategoryTheory.PreOneHypercover.cylinder f g).sieve₀ =
    CategoryTheory.Sieve.generate
      (CategoryTheory.Presieve.bindOfArrows E.X E.f fun i =>
        (CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯)
            (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)