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

Wolfram Kahl kahl at cas.mcmaster.ca
Mon Aug 19 19:13:21 CEST 2013

On Mon, Aug 19, 2013 at 04:59:08PM +0100, Martin Escardo wrote:
> 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.

The next question then is:
How does this come out as a special case from an appropriate general
rule for parameterised and indexed inductive datatypes?

Because, as far as I know, that is what the definition of
propositional equality is for Agda, since Agda has no separate concept
of ``identity types'' in the language --- or am I mistaken here?


More information about the Agda mailing list