[Agda] Why no impredicative prop?

[Timothy Carstens]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151229/5e62294a/attachment.html