# [Agda] Highest Level seen?

Jacques Carette carette at mcmaster.ca
Mon Dec 24 14:39:03 CET 2012

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