{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.MorphismProperty C} →
      {K : CategoryTheory.Precoverage C} →
        [inst_1 : K.HasPullbacks] →
          {motive : P.IsLocalAtTarget K → Sort u_1} →
            ([toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)] →
                (pullbackSnd :
                    ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) (i : 𝒰.I₀),
                      P f → P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) →
                  (of_zeroHypercover :
                      ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y),
                        (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) →
                    motive ⋯) →
              (t : P.IsLocalAtTarget K) → motive t