∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀),
  (E.bind F).X ij = (F ij.fst).X ij.snd