∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [E.Small] {T : C} (f : T ⟶ S) [inst_2 : J.IsStableUnderBaseChange]
  [inst_3 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
  (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).Small