@HoTT: Non non, je dis « théorie des types de Martin-Löf » :-). La double lecture de « homotopy type theory » ne vient pas de moi, elle est expliquée par exemple par Mike Shulman sur le n-Category Café (http://golem.ph.utexas.edu/category...)
Et pour moi, « théorie homotopique des types » se traduirait plutôt en « homotopical type theory » en anglais.

PS : Merci :-)