Reference for the fact that (0=1) implies false requires a universe in MLTT
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.