[Agda] Why is propositional equality "Set a" instead of just Set?
m.escardo at cs.bham.ac.uk
Mon Aug 19 19:17:01 CEST 2013
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.
More information about the Agda