Commit 2023-04-17 10:43 a51c8652

View on Github →

feat: add constructions about continuous map and homotopies (#2984)

  • Add ContinuousMap.fst, ContinuousMap.snd, ContinuousMap.eval, and ContinuousMap.piMap.
  • Add ContinuousMap.Homotopy.prodMk, ContinuousMap.Homotopy.prodMap, ContinuousMap.Homotopy.pi, ContinuousMap.Homotopy.piMap.
  • Add ContinuousMap.Homotopic.prodMk, ContinuousMap.Homotopic.prodMap, ContinuousMap.Homotopic.pi, ContinuousMap.Homotopic.piMap.
  • Add ContinuousMap.HomotopyEquiv.prodCongr and ContinuousMap.HomotopyEquiv.piCongrRight.

Estimated changes