Homotopy Type Theory fully faithful > history (Rev #1)

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).