[Agda] Why no impredicative prop?

[Harley Eades III]

Hi, Thorsten.

> On Dec 29, 2015, at 5:11 PM, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> 
> More on the philosphical side: impredicativity is basically a classical idea which arises from the identification of Prop and Bool. I don’t know an intuitionistic justification of impredicativity.

I am not sure I understand what this means.  Do you have a reference regarding this?  System F is intuitionistic, but doesn’t this claim it isn’t?

Very best,
Harley

> 
> Thorsten
> 
> From: <agda-bounces at lists.chalmers.se <mailto:agda-bounces at lists.chalmers.se>> on behalf of Timothy Carstens <intoverflow at gmail.com <mailto:intoverflow at gmail.com>>
> Date: Tuesday, 29 December 2015 17:19
> To: "agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>>
> Subject: [Agda] Why no impredicative prop?
> 
> Hello,
> 
> I'm a relatively new Agda user, coming from a background using Coq for the past few years. As is well known, Coq has an impredicative Prop sort, while Agda does not.
> 
> Why not? Is it simply a matter of project goals, or is there something about Agda's underlying theory which is incompatible with having an impredicative sort at the bottom of the universe hierarchy?
> 
> Forgive me if this is an old topic or has an obvious answer; I'm not a logician, but I use proof assistants at work.
> -t
> 
>  
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it. 
> 
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
> 
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151230/69918203/attachment.html