Hurkens' paradox is an argument that a certain combination of features in a dependent type theory is inconsistent, i.e. proves the falsum. Like Girard's paradox, it is not really a paradox per se.
The particular features here are two impredicative universes:
Such a system was historically called System , especially in the pure type system literature.
As such, it is impossible to have an impredicative universe Prop of propositions be a member Prop : Set of a universe Set which is also impredicative. This is the reason why Coq has made Set predicative in the more recent past.
Hurkens, Antonius J. C. ‘A Simplification of Girard’s Paradox’. In Typed Lambda Calculi and Applications, edited by Mariangiola Dezani-Ciancaglini and Gordon Plotkin, 902:266–78. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995. https://doi.org/10.1007/BFb0014058. [pdf]
@inproceedings{hurkens_1995,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {A simplification of {Girard}'s paradox},
volume = {902},
booktitle = {Typed {Lambda} {Calculi} and {Applications}},
publisher = {Springer Berlin Heidelberg},
author = {Hurkens, Antonius J. C.},
editor = {Dezani-Ciancaglini, Mariangiola and Plotkin, Gordon},
year = {1995},
doi = {10.1007/BFb0014058},
pages = {266--278},
}
Coquand, T. ‘Metamathematical Investigations of a Calculus of Constructions’. INRIA, 1989. https://inria.hal.science/inria-00075471.
@techreport{coquand_metamathematical_1989,
title = {Metamathematical investigations of a calculus of constructions},
url = {https://inria.hal.science/inria-00075471},
number = {RR-1088},
institution = {INRIA},
author = {Coquand, T.},
year = {1989},
file = {meta.pdf:C\:\\Users\\Alex\\Zotero\\storage\\V9WNAUTZ\\meta.pdf:application/pdf},
}
Some notes on formalizing Hurkens' paradox by Arnaud Spiwack.
A blog post with a version in Agda by Jonathan Chan