feat(topology/covering): Define covering spaces (#16087)
This PR adds a definition of covering spaces.
We don't want to have to specify a constant index set `I`, and we don't want to say "there exists an index set `I : Type u` such that `f ⁻¹' U` is homeomorphic to `I × U`" (annoying universe issues). Instead, we can use the preimage of any point as our index set.
Supersedes #15276, where @alreadydone suggested that I drop the surjectivity assumption.
