The interpretation of types in intensional Martin-Löf type theory as spaces and their equalities as paths leads to a surprising new view on the identity type: not only are higher-dimensional equalities explained as homotopies, ...