# 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?

• Coquand's "A New Paradox in Type Theory" (94) describes the truth valued semantics of minimal higher-order logic, and seems to suggest that this interpretation was known before. I seem to recall a mention of such a model even for Russell's Type Theory but I can't seem to find it... – cody Jan 22 '15 at 15:56
• This Martin Hoffman text confirms the Jan Smith reference in the answer, and has a reasonable presentation of that proof with categorical semantics in the exercises ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf – user833970 May 28 '19 at 16:24