Almost at the top of the HoTT website are the words: “Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  ” I think it is time to change these words … Continue reading HoTT is not an interpretation of MLTT into abstract homotopy theory