mathlib

7ccc7ae6 - feat(topology/homotopy/fundamental_groupoid): The functor from `Top` to `Groupoid` (#10195)

feat(topology/homotopy/fundamental_groupoid): The functor from `Top` to `Groupoid` (#10195) I have no idea if the ways I've done things is the right way, eg. I don't know if I need to be thinking about universes when defining the functor, so comments about that are definitely welcome.