Author Archives: vladimirias

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 →