Set Implicit Arguments.
Require Import Eqdep_dec.

Section Berardi.

(* We assume a proposition with two proofs.
   The goal is to show that both proofs are equal. *)

Inductive Bool : Prop :=
| T : Bool
| F : Bool.

(* We assume decidable equality for propositions. *)

Hypothesis DEP :
  forall (x y : Prop), x = y \/ ~ x = y.

(* Uniqueness of identity proofs follows. *)

Lemma UIP :
  forall (x : Prop) (H : x = x), H = eq_refl.
Proof.
  intros x H. pattern H. apply K_dec; auto.
Qed.

(* Powerset operation *)

Definition pow (P : Prop) :=
  P -> Bool.

(* Paradoxical universe *)

Definition U :=
  forall P, pow P.

(* We want to show that pow U is a retract of U.
   The surjection U -> pow U is easily defined. *)

Definition sur : U -> pow U :=
  fun u => u U.

(* The injection pow U -> U takes a set h : pow U and a proposition P.
   To return a set in pow P as desired, a case distinction on U = P is performed.
   If U = P, then we just return the set h.
   If U <> P, we can return any set in pow P, for instance the empty set fun _ => F. *)

Definition inj : pow U -> U :=
  fun h P => match DEP U P with
        | or_introl E => eq_ind U pow h P E
        | or_intror _ => fun p => F
        end.

(* We illustrate that these functions indeed make pow U a retract of U. *)

Lemma sur_inj (h: pow U) :
  sur (inj h) = h.
Proof. 
  unfold sur, inj. destruct (DEP U U) as [|H].
  - rewrite (UIP e). reflexivity.
  - contradiction.
Qed.

(* We define the paradoxical Russell set in the usual fashion. *)

Definition Not (b : Bool) :=
  if b then F else T.

Definition R : U :=
  inj (fun u => Not (u U u)).

(* This paradoxical set yields a fixed-point of Not. *)

Lemma Not_fix :
  R R = Not (R R).
Proof.
  unfold R at 1. unfold inj.
  destruct (DEP U U) as [H|H].
  - rewrite (UIP H). reflexivity.
  - contradiction.
Qed.

(* This implies that T = F. *)

Theorem PI' :
  T = F.
Proof.
  specialize Not_fix. unfold Not.
  destruct (R R); now intros ->.
Qed.

(* We conclude proof irrelevance. *)

Section PI.

Variables (P : Prop) (H1 H2 : P).

Definition f (b : Bool) :=
  if b then H1 else H2.

Theorem PI :
  H1 = H2.
Proof.
  change (f T = f F). now rewrite PI'.
Qed.

End PI.

End Berardi.