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?
Reference for the fact that (0=1) implies false requires a universe in MLTT
reference request;lo.logic;pl.programming languages;type theory;dependent type
I know of:Jan M. Smith, The independence of Peano's fourth axiom from Martin-Lf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.