{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {property : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X)} →
        {iff_shrink : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property E ↔ property E.shrink} →
          {property' : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X)} →
            {iff_shrink' : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property' E ↔ property' E.shrink} →
              { property := property, iff_shrink := iff_shrink } =
                  { property := property', iff_shrink := iff_shrink' } →
                (property ≍ property' → P) → P