Odniesienie do faktu, że (0 = 1) oznacza fałsz, wymaga wszechświata w MLTT

Jest to dość dobrze znany fakt, że wywodzenie sprzeczności z nierówności (na przykład ) w teorii typu Martina-Loefa wymaga wszechświata.$(0=1) \to \bot$

Dowód jest również dość prosty - w przypadku braku wszechświatów możemy usunąć zależności od dowolnego typu zależnego, aby uzyskać prosty typ jako jego kształt, a więc udowodnienie, że oznacza, że ​​możemy udowodnić p → ⊥ dla dowolnego atomu p , co oczywiście nie jest możliwe.$(0=1) \to \bot$$p \to \bot$$p$

Nie mogę jednak znaleźć, kto udowodnił to pierwszy! Czy ktoś ma referencje?

Wiem o:

Jan M. Smith, Niezależność czwartego aksjomatu Peano od teorii typów Martina-Löfa bez wszechświatów, The Journal of Symbolic Logic 53 (3), s. 1. 840–845, 1988.