[Agda] Highest Level seen?

[Darryl]

I've wondered on numerous occasions whether or not pure sets (ie no data declarations) gives a traditional iterated conception of set. I've never fully determined if the answer is yes or no. I think you might need Lift as the only data decl to get that, maybe? But the absence of pattern matching on types makes it useless.

- darryl



________________________________
 From: Jacques Carette <carette at mcmaster.ca>
To: Darryl <psygnisfive at yahoo.com> 
Cc: Agda <Agda at lists.chalmers.se> 
Sent: Monday, December 24, 2012 8:39 AM
Subject: Re: [Agda] Highest Level seen?
 

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
>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/2fede957/attachment.html