Girard's paradox #
Girard's paradox is a proof that
Type : Type entails a contradiction. We can't say this directly
in Lean because
Type : Type 1 and it's not possible to give
Type a different type via an axiom,
so instead we axiomatize the behavior of the Pi type and application if the typing rule for Pi was
(Type → Type) → Type instead of
(Type → Type) → Type 1.
Furthermore, we don't actually want false axioms in mathlib, so rather than introducing the axioms
constant declarations, we take them as assumptions to the
Based on Watkins' LF implementation of Hurkens' simplification of Girard's paradox: http://www.cs.cmu.edu/~kw/research/hurkens95tlca.elf.
Main statements #
girard: there are no Girard universes.
Girard's paradox: there are no universes
u such that
Type u : Type u.
Since we can't actually change the type of Lean's
Π operator, we assume the existence of
app and the
beta rule equivalent to the
app constructors of type theory.