The Coq mailing list

[James McKinna <james AT fixedpoint.org>]

Daniel,

and friends on the co-club list.

Please find below the LEGO formalisation (1995ish?) by Herman Geuvers of 
Tonny Hurkens' argument.
Needs Type in Type (obv.),and should be readily translatable into 
Coq/Gallina.
Bindings [x:A] correspond to Hypothesis/Axiom declarations,
[x:A= M] to Definitions, etc.

best,

James McKinna

Daniel Schepler wrote:
> On Fri, May 4, 2012 at 9:36 PM, Randy Pollack 
> <rpollack0 AT gmail.com>
>  wrote:
>   
> > Hurken's paradox, TLCA 1995.
> >     
>
> Umm, could you be more specific?  When I tried a Google search on
> those terms, all I got was some random Agda patch where "Hurken's
> paradox" was just by itself in the middle with no context.  And afaict
> HurkensParadox.v in the Coq source would require something like
> Axiom classicT : forall {X:Type}, X + (X -> False).
===============


[V = {A|Type}((A->Type)->(A->Type))->A->Type];

[U = V->Type];

[sb [A|Type][r:(A->Type)->(A->Type)][a:A] = [z:V]r (z r) a : U];

[le [i:U->Type][x:U] =
      x ([A|Type][r:(A->Type)->(A->Type)][a:A]i (sb r a)) : Type];

[induct [i:U->Type] = {x:U}(le i x)->i x : Type];

[WF = [z:V]induct (z le) : U];

[B:Type];
[I [x:U] = ({i:U->Type}(le i x)->i (sb le x))->B : Type];

Goal {i:U->Type}(induct i)->i WF;
intros i y;
Refine y WF ([x:U]y (sb le x));
Save omega;

Goal induct I;
Intros x p q;
Refine q I p ([i:U->Type]q ([y:U]i (sb le y)));
Save lemma;

Goal  ({i:U->Type}(induct i)->i WF)->B;
intros x;
Refine x I lemma ([i:U->Type]x ([y:U]i (sb le y)));
Save lemma2;

Goal B;
Refine lemma2 omega;
Save paradox;