∀ {C₀ : Type u_2} {C : Type u_5} [inst : CategoryTheory.Category.{u_1, u_2} C₀]
  [inst_1 : CategoryTheory.Category.{u_4, u_5} C] {F : CategoryTheory.Functor C₀ C}
  {J₀ : CategoryTheory.GrothendieckTopology C₀} {J : CategoryTheory.GrothendieckTopology C}
  (data : (X : C) → F.OneHypercoverDenseData J₀ J X) (X : C) (i₁ i₂ : (data X).I₀) {Y₀ : C₀}
  (p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)) (p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂))
  (fac : CategoryTheory.CategoryStruct.comp p₁ ((data X).f i₁) = CategoryTheory.CategoryStruct.comp p₂ ((data X).f i₂))
  (W₀ : C₀) (a : W₀ ⟶ Y₀) (b₁ : W₀ ⟶ (data X).X i₁) (h₁ : F.map b₁ = CategoryTheory.CategoryStruct.comp (F.map a) p₁)
  (b₂ : W₀ ⟶ (data X).X i₂) (h₂ : F.map b₂ = CategoryTheory.CategoryStruct.comp (F.map a) p₂)
  (motive : CategoryTheory.GrothendieckTopology.Cover.Arrow ⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩ → Prop)
  (h : CategoryTheory.GrothendieckTopology.Cover.Arrow ⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩),
  (∀ (U₀ : C₀) (c : U₀ ⟶ W₀) (j : (data X).I₁ i₁ i₂) (t : U₀ ⟶ (data X).Y j)
      (fac₁ : CategoryTheory.CategoryStruct.comp c b₁ = CategoryTheory.CategoryStruct.comp t ((data X).p₁ j))
      (fac₂ : CategoryTheory.CategoryStruct.comp c b₂ = CategoryTheory.CategoryStruct.comp t ((data X).p₂ j)),
      motive { Y := U₀, f := c, hf := ⋯ }) →
    motive h