Commit 2023-03-23 16:06 fa9ff1ab

feat: port Topology.PathConnected (#2755) The major thing to note is that I have replaced the CoeFun instance (which was p ↦ p.toContinuousMap.toFun) with FunLike.coe, but previously Path did not have a FunLike instance, so I have added a ContinuousMapClass instance. These are defeq. This also meant there would have been two coercions from Path x y to C(I, X), namely, the one which was originally declared in this file (:= p ↦ p.toContinuousMap) and the one inherited from ContinuousMapClass. As a result I have opted for the deleting the former in favor of the latter. These are not definitionally equal, but with the rewrite lemmas in place, there seem to be no real issues. Note: the biggest reason for switching to FunLike was that the previous coercions were causing absolute hell early in the file with timeouts. If you want to see what I mean, checkout an early commit and attempt to start fixing.