[Agda] Size of propositional equality?

[Thorsten Altenkirch]

I am just trying to understand this: Are you saying at large equality types wouldn't be consistent if we adopt the interpretation that equality of sets is isomorphism (or more precisely "weak equivalence")? 

While there clearly is a size problem, it is not clear that this would be unsound. In particular if you are not allowed to project out the large components of the proof of isomorphism. 

Cheers,
Thorsten

On 23 Dec 2010, at 03:25, Dan Licata wrote:

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