The Coq mailing list

[roconnor AT theorem.ca]

I spent some time trying to extend Chung-Kil's proof to an outright 
contradiction, but Agda's predicativity thwarted my attempts.  If Agda had 
an impredictiave Prop universe like Coq does, there would be an outright 
contradiciton.  Below is my proof that Coq has non-injective type 
constructors:

Definition Type1 := Type.

Inductive I : (Type1 -> Type1) -> Type1 := .

Section ChungKil.

Hypothesis InjI : forall x y, I x = I y -> x = y.

Definition P (x:Type1) : Type1 := exists a, I a = x /\ (inhabited (a x) -> 
False).

Definition p := I P.

Lemma contradiction : inhabited (P p) <-> (inhabited (P p) -> False).
Proof.
unfold P at 1.
unfold p at 1.
split.
 intros [[a [Ha0 Ha1]]].
 replace a with P in Ha1; [assumption|].
 firstorder.
intros H.
constructor.
exists P.
firstorder.
Qed.

Lemma absurd : False.
assert (Z:=contradiction).
tauto.
Qed.

End ChungKil.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''