{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {motive : E.Hom F → Sort u_1} →
            ((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₁₁ :
                        ∀ {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)) →
                      (w₁₂ :
                          ∀ {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)) →
                        motive { toHom := toHom, s₁ := s₁, h₁ := h₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }) →
              (t : E.Hom F) → motive t