Commit 2025-10-13 13:57 3c90d005
View on Github →feat(CategoryTheory/Sites): small 0-hypercovers (#30321)
A w-0-hypercover E is w'-small if there exists an indexing type ι in Type w' and a
restriction map ι → E.I₀ such that the restriction of E to ι is still covering.
This is weaker than E.I₀ being w'-small. For example, every Zariski cover of X : Scheme.{u} is u-small,
because X itself suffices as indexing type.