Comment by cjfd

Well, I tried to have only one universe level but I found that I could not do some rather simple constructions without proof irrelevance. And that generally proof irrelevance seems to make quite a few things quite a bit easier, also requiring fewer axioms. The thing with proof irrelevance is, though, that it more or less forces one to have universe levels. If there is only one universe level then Prop and Set have to share that. In fact, in that kind of simple setup Prop and Set are just the same thing and one can just use two words as a syntactic sugar but not as anything meaningful. However, proof irrelevance then implies that every set only has one element, which is no good. So, then we we have at least two universe levels. But impredicativity is only consistent in the lowest universe level so then one is more or less automatically led to an infinite tower of universes.