<div dir="ltr"><div>Hello,</div><div><br></div><div>I&#39;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.</div><div><br></div><div>Why not? Is it simply a matter of project goals, or is there something about Agda&#39;s underlying theory which is incompatible with having an impredicative sort at the bottom of the universe hierarchy?</div><div><br></div><div>Forgive me if this is an old topic or has an obvious answer; I&#39;m not a logician, but I use proof assistants at work.<br></div><div>-t</div><div><br></div></div>