# 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.

**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.