Commit 2023-10-23 14:19 1beeb5e5

refactor: remove redundant condition in HomotopyRel (#7848) For a homotopy F between f₀ and f₁ to be a homotopy relative to a set S, it suffices that F (t, x) = f₀ x for all x ∈ S and t : I, from which F (t, x) = f₁ x can be derived. Also add HomotopyRel.compContinuousMap.