Simon J. Thompson: Are Subsets Necessary in Martin-Löf Type Theory? Constructivity in Computer Science 1991: 46-57