Require Import Classical. 

(*** we start with Russell's paradox ***)

Definition is_injective (A B : Type) (f : A -> B) :=
  forall x y : A, f x = f y -> x = y.

Lemma russell :
 forall (X : Type) (f : (X -> Prop) -> X),
 is_injective (X -> Prop) X f -> False. 
intros. 
set (Q := fun x : X => exists P : X -> Prop, f P = x /\ ~ P x). 
set (y := f Q). assert (~ Q y). unfold not in |- *; intro. 
assert (Q y). assumption. unfold Q in H1. 
induction H1. induction H1. assert (x = Q). 
apply H. rewrite H1; trivial. apply H2. rewrite H3. 
assumption. apply H0. unfold Q in |- *. 
apply ex_intro with Q. apply conj. trivial. assumption. 
Qed. 

(*** the following injectivity is basically Marco Maggesi's proof 
that JMeqT => eqT, using eqT_rect. See also 
Alvarado Cuihtlauac's thesis. *******)

Export ProofIrrelevance. 

Lemma pi : forall (P : Prop) (p q : P), p = q. 
apply proof_irrelevance_cci. intro. apply classic. 
Qed. 

Definition transport : forall (A B : Type) (hyp : A = B), A -> B. 
intros A B hyp. rewrite hyp. intro; assumption. 
Defined. 

Lemma transport_id :
 forall (A : Type) (hyp : A = A) (a : A), transport A A hyp a = a.
intros. assert (hyp = refl_equal A). apply pi. rewrite H. trivial.
Qed. 

Inductive Term : Type :=
    term : forall T : Type, T -> Term.

Definition extend : forall (X : Type) (P : X -> Prop), Term -> Prop. 
intros. induction X0. exact (forall hyp : T = X, P (transport T X hyp t)). 
Defined.

Lemma extend_in :
 forall (X : Type) (P : X -> Prop) (x : X), P x -> extend X P (term X x). 
intros.  change (forall hyp : X = X, P (transport X X hyp x)) in |- *. 
intros.  rewrite transport_id. assumption.
Qed. 

Lemma extend_out :
 forall (X : Type) (P : X -> Prop) (x : X), extend X P (term X x) -> P x. 
intros.  assert (transport X X (refl_equal X) x = x).
split. change (forall hyp : X = X, P (transport X X hyp x)) in H. 
pose (H (refl_equal X)). clearbody p. rewrite <- H0. assumption. 
Qed. 

Lemma term_inj : forall (X : Type) (x y : X), term X x = term X y -> x = y. 
intros. set (P := fun z : X => z = x) in *. 
assert (extend X P (term X x)). apply extend_in. unfold P in |- *; trivial. rewrite H in H0. symmetry  in |- *. change (P y) in |- *. 
apply extend_out. assumption. 
Qed. 

(*** now we give a pair of seemingly contradictory 
theorems ***)

Definition term_injection_exists (X : Type) :=
  exists f : X -> Term, is_injective _ _ f. 

Theorem injections_dont_always_exist :
 (forall X : Type, term_injection_exists X) -> False.
intro. pose (H (Term -> Prop)). 
clearbody t. unfold term_injection_exists in t. 
induction t. apply russell with Term x. assumption. 
Qed. 

Theorem injections_exist : forall X : Type, term_injection_exists X.
unfold term_injection_exists in |- *. 
intro. apply ex_intro with (fun x : X => term X x). 
unfold is_injective in |- *; intros. apply term_inj. 
assumption. Qed. 

(*** If we restate the latter theorem as an axiom, then
we obtain a contradiction. ****)

Axiom injections_exist_axiom : forall X : Type, term_injection_exists X.

Lemma contradiction : False.
apply injections_dont_always_exist. 
intro. apply injections_exist_axiom. 
Qed. 

(*** however, combining with the actual theorem
leads to a Universe Inconsistency. ***)


Lemma combo : False. 
apply injections_dont_always_exist. 
intro. apply injections_exist. 
Save. 
---Error: Universe Inconsistency.


(**** the above file compiles (under v 7.4) except for the last line which generates a
Universe Inconsistency. The explanation is that the word Type in the phrase
"(X:Type)(term_injection_exists X)" is assigned a different universe index in
the two different cases. The universe index is lost when we restate the theorem 
as an axiom.  Thus, with typical ambiguity, one cannot just recopy theorems as 
axioms. 
---cs, tuesday oct. 14th 2003 ****)