∀ {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 f_1 : E.Hom F),
  f = f_1 →
    ∀ (g g_1 : E.Hom F),
      g = g_1 → CategoryTheory.PreOneHypercover.cylinder f g = CategoryTheory.PreOneHypercover.cylinder f_1 g_1