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

[Martin Escardo]

On 19/08/13 17:51, Wolfram Kahl wrote:
 > 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?

I certainly agree with the question. Agda can write down more kinds of 
inductive definitions than were originally envisaged in intensional 
MLTT, and also after iMLTT. Various research groups are trying to 
understand/make sense of that.

Although identity types may be a particular case of this (when the 
answer is known), they certainly (seem to) have a primary role, as the 
articulation of equality in propositions-as-types. So it is worth 
looking at this particular case (first) with close attention.

For example, a question that comes to mind immediately is what universe 
level assignments are (in)compatible with univalence. Even if one 
doesn't want to postulate univalence, I think it is interesting to be 
compatible with univalence. (In the same way one wants to be compatible 
with excluded middle, with continuity, with function extensionality, etc.)

Because of the (seemingly) primary and unavoidable notion of equality, 
and because of the need of universes to avoid impredicativity, it would 
be good to clarify how identity types interact with universe levels. And 
then, also, answer your more general question above.

Martin



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