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

Martin Escardo m.escardo at cs.bham.ac.uk
Mon Aug 19 17:59:08 CEST 2013

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. 

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

More information about the Agda mailing list