[Agda] Why is propositional equality "Set a" instead of just Set?

[Martin Escardo]

It would be good if somebody with experience in both intensional MLTT 
and HoTT wrote down explicitly what the correct universe levels of 
identity types are in the presence of a tower of universes indexed by 
natural numbers, for the record. I am not sure how explicit the HoTT 
book is about that, or even the earlier references for intensional MLTT. 
Martin

On 19/08/13 16:45, Jonathan Leivent wrote:
> 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?
>
> -- Jonathan
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe