Commit 2021-11-15 21:01 7ccc7ae6

View on Github →

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.

Estimated changes

Modified src/data/quot.lean

added theorem quotient.map₂_mk

Modified src/topology/homotopy/basic.lean

modified theorem continuous_map.homotopic.symm

modified theorem continuous_map.homotopic_rel.symm

Modified src/topology/homotopy/fundamental_groupoid.lean

added theorem fundamental_groupoid.comp_eq

added def fundamental_groupoid.fundamental_groupoid_functor

Modified src/topology/homotopy/path.lean

added theorem path.homotopic.hcomp

added theorem path.homotopic.map

modified theorem path.homotopic.symm

added def path.homotopy.map

Modified src/topology/path_connected.lean

added theorem path.map_id

added theorem path.map_map

added theorem path.map_symm

added theorem path.map_trans