mathlib3

d49ae127 - feat(topology/homotopy): Add homotopy product (#10946)

feat(topology/homotopy): Add homotopy product (#10946) Binary product and pi product of homotopies. Co-authored-by: prakol16 <prakol16@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>