Commit 2022-04-15 20:29 449e06a9

feat(algebraic_topology/fundamental_groupoid/fundamental_group): add type checker helpers for convertings paths to/from elements of fundamental group (#13182) This pr adds the following helper functions for converting paths to and from elements of the fundamental group:

• to_arrow: converts element of the fundamental group to an arrow in the fundamental groupoid
• to_path: converts element of the fundamental group to a (quotient of homotopic) path in the space
• from_arrow: constructs an element of the fundamental group from a self-arrow in the fundamental groupoid
• from_path: constructs an element of the fundamental group from a (quotient of homotopic) path in the space These parallel the similarly named functions for the fundamental group here. They will prove helpful in doing computations with the fundamental group later e.g. for the disk, circle, etc.