Comment by zmgsabst

Isn’t that the intuition behind homotopy type theory — that equivalence is a path between types?

(And related, eg, cubical type theory.)