I (Victor Porton) have the following (very preliminary) idea:
Replace “path” in the definition of homotopy with “monovalued funcoid with domain [0;1]”. It enables things like infinitely short paths. This way we may get another HoTT possibly not equivalent to the “main” HoTT.
This idea uses theory of funcoids (discovered by me).