∀ {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)
  {p q : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ p q),
  (CategoryTheory.PreOneHypercover.cylinderHom f g).h₁ k =
    CategoryTheory.Limits.pullback.snd
      (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
        (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯)
          (F.toPullback p.snd))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯)
          (F.toPullback q.snd))
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)