Require Classical. 

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

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

Lemma russell : (X:Type; f:(X->Prop) -> X)
(is_injective X-> Prop X f) -> False. 
Intros. 
Pose Q := [x:X](exT ? [P:X->Prop]((f P) == x) /\~(P x)). 
Pose y := (f Q). Assert ~(Q y). Unfold not; Intro. 
Assert (Q y ). Assumption. Unfold Q in H1. 
NewInduction H1. NewInduction H1. Assert x == Q. 
Apply H. Rewrite H1; Trivial. Apply H2. Rewrite H3. 
Assumption. Apply H0. Unfold Q. 
Apply exT_intro with Q. Apply conj. Trivial. Assumption. 
Save. 

(*** 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: (P:Prop; p,q:P)p==q. 
Apply proof_irrelevance_cci. Intro. Apply classic. 
Save. 

Definition transport : (A,B:Type; hyp : A==B)A->B. 
Intros A B hyp. Rewrite hyp. Intro; Assumption. 
Defined. 

Lemma transport_id : (A:Type; hyp : A == A; a:A)(transport A A hyp a) == a.
Intros. Assert hyp == (refl_eqT ? A). Apply pi. Rewrite H. Split. 
Save. 

Inductive Term : Type := term : (T:Type)T->Term.

Definition extend : (X:Type; P:X->Prop)Term -> Prop. 
Intros. NewInduction X0. Exact (hyp : T == X)(P (transport T X hyp t)). 
Defined.

Lemma extend_in : (X:Type; P:X->Prop; x:X)
(P x) -> (extend X P (term X x)). 
Intros.  Change (hyp : X == X)(P (transport X X hyp x)). 
Intros.  Rewrite transport_id. Assumption.
Save. 

Lemma extend_out : (X:Type; P:X->Prop; x:X)
(extend X P (term X x))-> (P x). 
Intros.  Assert (transport X X (refl_eqT ? X) x) == x.
Split. Change (hyp : X == X)(P (transport X X hyp x)) in H. 
Pose (H (refl_eqT ? X)). ClearBody p. Rewrite <- H0. Assumption. 
Save. 

Lemma term_inj : (X:Type; x,y:X)(term X x) ==
(term X y) -> x == y. 
Intros. LetTac P := [z:X]z==x. 
Assert (extend X P (term X x)). Apply extend_in. Unfold P; 
Trivial. Rewrite H in H0. Symmetry . Change (P y). 
Apply extend_out. Assumption. 
Save. 

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

Definition term_injection_exists := [X:Type]
(exT ? [f:X->Term](is_injective ? ? f)). 

Theorem injections_dont_always_exist : 
((X:Type)(term_injection_exists X))-> False.
Intro. Pose (H Term->Prop). 
ClearBody t. Unfold term_injection_exists in t. 
NewInduction t. Apply russell with Term x. Assumption. 
Save. 

Theorem injections_exist : (X:Type)(term_injection_exists X).
Unfold term_injection_exists. 
Intro. Apply exT_intro with [x:X](term X x). 
Unfold is_injective; Intros. Apply term_inj. 
Assumption. Save. 

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

Axiom injections_exist_axiom : (X:Type)(term_injection_exists X).

Lemma contradiction : False.
Apply injections_dont_always_exist. 
Intro. Apply injections_exist_axiom. 
Save. 

(*** 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 ****)