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?

  • $\begingroup$ 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... $\endgroup$
    – cody
    Jan 22, 2015 at 15:56
  • $\begingroup$ 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 $\endgroup$
    – user833970
    May 28, 2019 at 16:24

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.