3 ms·
Isn’t that the intuition behind homotopy type theory — that equivalence is a path between types? (And related, eg, cubical type theory.)
by zmgsabst 2y ago
Isn’t that the intuition behind homotopy type theory — that equivalence is a path between types?
(And related, eg, cubical type theory.)