La référence au fait que (0 = 1) implique faux nécessite un univers en MLTT

C'est un fait assez bien connu que dériver une contradiction d'une inégalité (par exemple, ) dans la théorie de type Martin-Loef nécessite un univers.$(0=1) \to \bot$

La preuve est également assez simple - en l'absence d'univers, nous pouvons effacer les dépendances de tout type dépendant pour obtenir un type simple comme sa forme, et donc prouver que implique que nous pouvons prouver p → ⊥ pour un atome arbitraire p , ce qui n'est bien sûr pas possible.$(0=1) \to \bot$$p \to \bot$$p$

Cependant, je ne trouve pas qui l'a prouvé en premier! Quelqu'un at-il une référence?

Je connais:

Jan M. Smith, L'indépendance du quatrième axiome de Peano par rapport à la théorie des types sans univers de Martin-Löf, The Journal of Symbolic Logic 53 (3), p. 840-845, 1988.