[Agda] Why is propositional equality "Set a" instead of just Set?
jleivent at comcast.net
Mon Aug 19 17:45:36 CEST 2013
On 08/18/2013 04:39 PM, Andreas Abel wrote:
> Putting propositional equality in a lower universe than the type it
> speaks about is at least problematic when you want to construct a PER
> model of type theory predicatively.
As a non-type-theorist trying to use Agda, I don't have the intuitions
needed here to know I'm treading on uncertain ground. So, I was relying
on the type checker. Is there some option I can use that will cause the
type checker to enforce this rule?
More information about the Agda