{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {motive : J.RespectsIso → Sort u_1} →
        (t : J.RespectsIso) →
          ((of_iso :
                ∀ {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F),
                  E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S) →
              motive ⋯) →
            motive t