Standard Library | The Coq Proof Assistant

Exploiting Hurkens's paradox [Hurkens95] for system U- so as to derive various contradictory contexts. The file is divided into various sub-modules which all follow the same structure: a section introduces the contradictory hypotheses and a theorem named paradox concludes the module with a proof of False. The Generic module contains the actual Hurkens's paradox for a postulated shallow encoding of

[qnighy]

ある命題の証明の集合の濃度は、命題全体の族の濃度より小さい。

[ytb]

This is Hurkens paradox Hurkens in system U-, adapted by Herman Geuvers Geuvers to show the inconsistency in the pure calculus of constructions of a retract from Prop into a small type.