The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

> Vladimir Voevodsky's terminology for homotopy levels, let's rather
> call it Type(-1).

Oups, sorry, I swapped. This is precisely not Vladimir's terminology
but the usual terminology extended so as to include Vladimir's level 1
(with a shift by 2 then). I wish HoTT specialists would correct me if
I'm still wrong.

Also, still with respect to HoTT, it should be noted that even if it
might be convenient to use -1 and 0 to refer to proof-irrelevant Prop
and to predicative Set, this would not scale to Type(1) and further,
as the Type(i) hierarchy for i>=1 would well remain a hierarchy of
"universes", not a hierarchy of homotopy levels.

Sorry for the confusion,

Hugo