Point-free paths sound similar to cubical type theory from HoTT. Is there a relation?

Great work!