The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, May 05, 2012 04:30:49 AM you wrote:
> However the paradox using the type
> 
>  Inductive V : Type :=  | V_const : forall {X:Type}, (X->V) -> V
> 
> is particularly natural, I think, given Peter Aczel translation of set
> theory CZF in type theory who uses a similar inductive type as a type of
> all sets (seeing a set as well-founded tree).

Yes, that's exactly what I had in mind when I wrote my definition of V.  I 
just 
threw away the complex interdependent definitions of In and Eq which are 
needed 
to make Eq extensional, and In proper in its first argument with respect to 
Eq.  
And still had a structure that was close enough to be able to derive a 
contradiction if the type system allowed forming the "universal set of 
everything in V".
-- 
Daniel Schepler