mathlib3

20997252 - feat(topology/homotopy/product): Product of homotopic paths (#11153)

feat(topology/homotopy/product): Product of homotopic paths (#11153) Specialize homotopy products to paths and prove some theorems about the product of paths. Co-authored-by: prakol16 <prakol16@users.noreply.github.com>