[Agda] Why is propositional equality "Set a" instead of just Set?
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
More information about the Agda