The Coq mailing list

[roconnor AT theorem.ca]

On Fri, 8 Jan 2010, Chung Kil Hur wrote:

> But, in this proof, we need to notice that we use "False : Prop" rather than 
> "Empty_set : Set".
> If you change "False" to "Empty_set", then the type of R cannot be "Set -> Set", rather it 
> should "Set -> Type".
> The reason why R is typable as Set -> Set is due to the impredicativity of Prop, 
> because R is typepable as Set -> Prop, which is
> coercible to Set -> Set.

Ah, I didn't realize that Set was coercable to Prop otherwise I wouldn't 
have done my Type1 nonsense.

> This proof does not need any axiom, but just the impredicativity of Prop.
>
> So, this idea does not aplly to Agda because it does not have any 
> impredicative set like Prop.
> So, I applied cantor's diagonalization assuming the law of excluded middle.
>
> I think the presence of Prop is one of the fancy features of Coq as a proof 
> assistant (at least to me).
> So, the injectivity seems unatural to me in this view point.

To be honest, the impredicativity of Prop in Coq worries me just a little 
<http://r6.ca/blog/20091101T231201Z.html>

"Coq’s impredicative in Prop seems innocent because no information is 
allowed to flow from the Prop universe to the Set universe; however Prop 
values can witness termination of functions in Set. Perhaps there is an 
inconsistency arising from the impredicativity of Prop that “proves” the 
termination of some non-terminating function.

But worries about impredicativity is another story.

Thanks repeating the info on the Agda list for me.

--
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.''