∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {s₀ : E.I₀ → F.I₀} {h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)}
  {w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam}
  {s₀_1 : E.I₀ → F.I₀} {h₀_1 : (i : E.I₀) → E.X i ⟶ F.X (s₀_1 i)}
  {w₀_1 :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀_1 i) (F.f (s₀_1 i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam},
  { s₀ := s₀, h₀ := h₀, w₀ := w₀ } = { s₀ := s₀_1, h₀ := h₀_1, w₀ := w₀_1 } → s₀ = s₀_1 ∧ h₀ ≍ h₀_1