[Agda] Size of propositional equality?

[Vladimir Voevodsky]

Or may be a cleaner example can be obtained by looking at the type of sets with well orderings. Showing that this type is a set (of h-level 2) and looking at its automorphisms. Then one does not need isomorphism classes.

V. 




On Jan 3, 2011, at 11:17 AM, Vladimir Voevodsky wrote:

> 
> 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.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda