[Agda] Size of propositional equality?

[Dan Licata]

On Dec17, Nils Anders Danielsson wrote:
> On 2010-12-17 16:11, Alan Jeffrey wrote:
> >Is the skepticism a general one about sets being indexed by a set from
> >a larger universe, or is it specific to propositional equality?
> 
> The former.
> 

I think that higher-dimensional structure, like in the groupoid
interpretation of type theory, provides an interesting perspective on
this.  Here

Set0 would be interpreted as the groupoid of small groupoids, 
  (and their equalities/isomorphisms/equivalences)
Set1 would be interpreted as the groupoid of large groupoids
Set2 would be interpreted as the groupoid of "larger" groupoids
and so on.
(I say "would be" because I believe Hofmann and Streicher's paper only
considers Set0 and a judgemental notion of types, which are larger.)  

Propositional equality Id_A(M,N), where A : Set i, is interpreted as the
morphisms in the groupoid A from M to N.

Thus, the version of Id that always lands in Set0 amounts to a
restriction that the interpretation of every type be locally small.
This precludes, for example, defining Set1 so that propositional
equality is isomorphism---because then you'd be jamming
functions A -> B, where A B : Set1, into Set0.  

While this doesn't say anything about Agda in its current form, it does
suggest preferring the definition of Id_A that inherits the universe
level of A, if we want to consider higher-dimensional extensions in the
future.

-Dan