This didn't work when I tried to post it the first time, hope this won't wind up as a double post.
Thorsten Altenkirch, a constructive logician and computer scientist, made a memorable quote on the TYPES Forum mailing list in June 2008 which is very much in the spirit of Voevodsky's talk:
It seems to me that Type:Type is an honest form of impredicativity, because at least you know that the system is inconsistent as a logic (as opposed to System F where so far nobody has been able to show this :-). Type:Type includes System F and the calculus of constructions and I think all reasonable programs can be reformed into Type(i):Type(i+1) possibly parametric in i. However, sometimes you don't want to think about the levels initially and sort this out later - i.e. use Type:Type. A similar attitude makes sense in Mathematics, in particular Category Theory, where it is convenient to worry about size conditions later...The system he is tongue-in-cheek questioning the consistency of is System F, which would correspond to second-order, not first-order, arithmetic. Type:type is an axiom that makes constructive type theory inconsistent (Girard's Paradox), so the "honest impredicativity" he refers to is therefore similar to what Voevodsky was talking about: we're admitting that everything is inconsistent and then doing our work anyway.
