Library HurkensTypeType

Lemma Hurkens (A : Type) : A.

Proof.
pose (P X := X -> Type).
pose (U := forall X, (P (P X) -> X) -> P (P X)).
pose (tau (t : P (P U)) X f p := t (fun x => p (f (x X f)))).
pose (sigma (s : U) := s U tau).
pose (Delta y := (forall p : P U, sigma y p -> p (tau (sigma y))) -> A).
pose (Omega := tau (fun p => forall x : U, sigma x p -> p x)).
assert (L : forall p : P U, (forall x : U, sigma x p -> p x) -> p Omega).
  intros p H. apply H. intros x. exact (H (tau (sigma x))).
cut (forall p : P U, sigma Omega p -> p (tau (sigma Omega))).
  apply (L Delta). intros x E F. refine (F Delta _ _).
  exact E.
  intros p. exact (F _).
intros p. exact (L _).
Show Proof.
Qed.