[Agda] Highest Level seen?

[Jacques Carette]

I would be quite surprised if it were so.  I was more going for a rough 
analogy.

What I do find I am missing is a nice way to tell Agda that I want 
certain inhabitants of Set0 to be 'small'.  To be more precise, I 
sometimes want a Setoid S whose carrier set C : Set is such that I have 
a function interp : C -> Set.  Basically I want to interpret C as a 
set-of-sets in Set.  Another way to see it is that C is formed from 
those sets whose power-set is representable.  As far as I can tell, in 
such a situation C really ought to be in Set_{-1}, and assuming we have 
a 'small' equality as well, then Setoid S would be in Set0, not Set1.  
In the codes I have, this would definitely help keep universe sizes way 
down.

Jacques

On 12-12-23 11:25 PM, Darryl wrote:
> Is it strictly true that sets, classes, and conglomerates are 
> equivalent to Set0, Set1, and Set2, respectively?
> - darryl
> ------------------------------------------------------------------------
> *From:* Jacques Carette <carette at mcmaster.ca>
> *To:* Agda <Agda at lists.chalmers.se>
> *Sent:* Saturday, December 22, 2012 11:11 AM
> *Subject:* [Agda] Highest Level seen?
>
> I am curious about one point: what is the highest Level that has been 
> seen in practice in an Agda development?  [Of course, one can 
> artificially go arbitrarily high; by 'in practice', I mean in the 
> course of developing some theory for the purposes of applications]
>
> A lot of Agda is done in a level-polymorphic way.  What I mean by my 
> question is then: how many suc's did you have to put in to make things 
> go through?
>
> In standard mathematics, when people worry about size, they tend to go 
> with sets, classes, and super-classes (sometimes called 
> conglomerates), and no higher.  This would seem to indicate that, 'in 
> the wild', Set_2 is all that is really needed.  Of course, given the 
> sloppiness of standard mathematics, one wonders if what they do really 
> does level-check...
>
> Jacques
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121224/189111cc/attachment.html