{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} →
        (toPreOneHypercover : CategoryTheory.PreOneHypercover S) →
          toPreOneHypercover.sieve₀ ∈ J S →
            (∀ (i₁ i₂ : toPreOneHypercover.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover.X i₁)
                (p₂ : W ⟶ toPreOneHypercover.X i₂),
                CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover.f i₁) =
                    CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover.f i₂) →
                  toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W) →
              J.OneHypercover S