feat(category_theory/is_connected): transfer across equivalence (#5021)
feat(category_theory/is_connected): transfer across equivalence (#5021)

Also renames some universes to match usual conventions 



leanprover-community/mathlib,leanprover-community/mathlib