A note on Russell's paradox in locally Cartesian closed categories
fragment of Martin-Löf's extensional type theory
scientific article; zbMATH DE number 4150149