[Agda] Highest Level seen?

[Dan Doel]

Standard mathematics is also impredicative. The power set of a set is a
set. This is not true in Agda.

There are also certain things one does in Agda that don't seem to be done
explicitly in set theory via the hierarchy. For instance, it's not terribly
far out to want a list of types, and for that we need to talk about the
type of lists of types, which inhabits a higher universe. But a set or list
of sets isn't necessarilly a very large object in set theory, and I doubt
the class of all lists of sets (which surely is a proper class) is talked
about much in set theory. One would  probably avoid talking about the
entire class, but work with the elements that are a) not big and b) exist
independently of the entire class, in set theory. Similarly, one can
manipulate sets and sets of sets and so on without mentioning the class of
all sets at all in the theory.

-- Dan
On Dec 22, 2012 11:12 AM, "Jacques Carette" <carette at mcmaster.ca> wrote:

> 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
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121222/be0259b3/attachment.html