Reference for the fact that (0=1) implies false requires a universe in MLTT It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe. 

The proof is also fairly straightforward -- in the absence of universes, we can erase the dependencies from any dependent type to get a simple type as its shape, and so proving that $(0=1) \to \bot$ implies we can prove $p \to \bot$ for an arbitrary atom $p$, which is of course not possible.

However, I can't find who proved this first! Does anyone have a reference?
I know of:

Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.