Lean: `ConnectedComponents` under `open CategoryTheory` is the topological one

With open CategoryTheory in effect, a bare ConnectedComponents J resolves to the root-namespace topological ConnectedComponents. The error is a confusing failed to synthesize TopologicalSpace J. Write CategoryTheory.ConnectedComponents (also for .mk and .typeToCatHomEquiv). The same trap applies to other names: inside a namespace SSet... with open CategoryTheory, Quotient.lift picks core Quotient.lift, so you need CategoryTheory.Quotient.lift r F H. Inside namespace CategoryTheory..., Equivalence r is the category equivalence, so you need _root_.Equivalence. Once the name is right, Quotient.sound (Zigzag.of_hom f) typechecks against ConnectedComponents.mk.