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 using axiom or constant declarations, we take them as assumptions to the girard theorem.

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.

theorem Counterexample.girard (pi : (Type u → Type u) → Type u) (lam : {A : Type u → Type u} → ((x : Type u) → A x) → pi A) (app : {A : Type u → Type u} → pi A → (x : Type u) → A x) (beta : ∀ {A : Type u → Type u} (f : (x : Type u) → A x) (x : Type u), app (lam f) x = f x) : False

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 pi, lam, app and the beta rule equivalent to the Π and app constructors of type theory.