> HoTT = théorie homotopique des types, pas théorie des types homotopiques

Personnellement je préfère « théorie des types homotopiques » (et je suis un des mathématiciens ayant écrit le livre).
En anglais, « homotopy type theory » peut se lire de deux façons différentes mais malheureusement ce n’est pas possible d’avoir la même chose en français. Sauf qu’à l’oral, « théorie des types homotopiques » peut plus ou moins s’entendre de deux façons différentes, alors que « théorie homotopique des types » non.