Is there a way to quantify over all indexed unions?

Stream: new members

[zzhevelt]

One axiom of a topological space is that it's open sets are closed under arbitrary unions. In mathlib, it's expressed as a following fact (link):
isOpen_sUnion : ∀ s, (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)
Is there a way to express the same axiom using indexed union instead of unindexed? My attempt is the following:
isOpen_iUnion : ∀ I: Type, ∀ S: I → Set α, (∀ i, IsOpen (S i)) → IsOpen (⋃ i, S i)
However, not every type lies in Type 0. In particular, I can't prove the two axioms are equivalent, since for that I would need I to depend on α, which is of arbitrary type.