∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {toHom : E.Hom F.toPreZeroHypercover}
  {s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j)}
  {h₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k)}
  {w₁₁ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam}
  {w₁₂ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam}
  {toHom_1 : E.Hom F.toPreZeroHypercover} {s₁_1 : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom_1.s₀ i) (toHom_1.s₀ j)}
  {h₁_1 : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁_1 k)}
  {w₁₁_1 :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁_1 k) (F.p₁ (s₁_1 k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom_1.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam}
  {w₁₂_1 :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁_1 k) (F.p₂ (s₁_1 k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom_1.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam},
  { toHom := toHom, s₁ := s₁, h₁ := h₁, w₁₁ := w₁₁, w₁₂ := w₁₂ } =
      { toHom := toHom_1, s₁ := s₁_1, h₁ := h₁_1, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 } →
    toHom = toHom_1 ∧ s₁ ≍ s₁_1 ∧ h₁ ≍ h₁_1