[Agda] Size of propositional equality?

[Vladimir Voevodsky]

On Jan 3, 2011, at 11:00 AM, Thorsten Altenkirch wrote:

>> 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.
> 


This is definitely true. The size of Id_A for a type of size-level n should have size-level n. Otherwise one will have that the set of permutations on the set of isomorphism classes of "small" sets is small. Since it is possible to show that it is at least as large as the set of isomorphism classes of "small" sets itself one can get a contradiction. 

Vladimir.