[Agda] Equivalence axiom => extensionality

[Dan Licata]

Hi Dan,

These are interesting thoughts.  I'd just like to tease apart a couple
of distinctions:

(1) I think the ideas of dimension (how long until the maps betwen maps
between ... become discrete) and size (in the predicative hierarchy
sense) are different.  You can have Set0's of higher dimension (make up
an inductive data U : Set0 of codes for a universe, but take equality to
be isomorphism) and you can have (Set n)'s of lower dimension (e.g. Set
n's considered up to "syntactic identity" (if the type theory has such a
notion), rather than isomorphism).  That said, Set n with isomorphisms
does provide a good example of higher-dimensional structure.

(2) Similarly, the question "what does it mean to index by
higher-dimensional data" (especially indexing non-uniformly) is
separable from the question of indexing by higher-sized data, and
whether types indexed non-uniformly by higher-sized data can fit into a
lower universe.  You could recast your examples in terms of a universe U
: Set whose equality is isomorphism, so that the index would have size 0
but dimension 1.  

-Dan


On Jul19, Dan Doel wrote:
> On Monday 19 July 2010 3:25:52 am Andreas Abel wrote:
> > On Jul 17, 2010, at 5:17 AM, Dan Doel wrote:
> > >
> > >  data Rep (S : Set) : Set where
> > >  
> > >    N  : S = Nat   -> Rep S
> > >    B  : S = Bool  -> Rep S
> > >    F2 : S = Fin 2 -> Rep S
> > 
> > If you do this in Agda, you still use large indices, but they are
> > shifted to the definition of =.
> > 
> > data Eq {i:Level}{s : Set i}(A : s) : s -> Set where
> >    refl : Eq A A
> 
> I was thinking more of a situation where equality was taken as a primitive of 
> the language (as might be the case for a language with homotopy identity 
> types? I'm not really sure). Of course, what universe would classify identity 
> types for some other universe in that case would be open to debate.
> 
> I was originally going to include a note about ignoring the fact that the 
> universes would no longer work out. But then I remembered that all equality 
> could (be made to) inhabit Set in Agda. The main idea was to try to infer how 
> 'large' indexing would behave from implementation with different identity 
> types.
> 
> > Such a definition can be justified for impredicative Set, but I have
> > not yet seen any predicative semantics that handles it.
> 
> Really? I was somewhat surprised when something like the above Eq definition 
> first worked for me. But it seemed somewhat keeping with Agda's rules. A is a 
> parameter, and so doesn't increase the size of the datatype. And no other Set 
> is actually stored in the constructor of the datatype, so it makes a bit of 
> sense. And if one tries to implement it with a built-in identity type:
> 
>   data Eq {i : Level}{s : Set i} (A B : s) : Set ? where
>     refl : A = B -> Eq A B
> 
> it depends entirely on where the primitive identity types live.
> 
> I suppose I could believe that Agda's checking in this regard is just that, 
> though: checking that makes things work out, but isn't justified by the sort 
> of underlying theory one would expect (similar to how the productivity checker 
> doesn't match the expected semantics, which would allow mu-nu fixed points).
> 
> ----
> 
> One final thought that occurred to me since my original message was that 
> "large" indices don't simply correspond to inhabitants of Set1 or above. I can 
> write:
> 
>   data Nat : Set1 where
>     z : Nat
>     s : Nat -> Nat
> 
> and there's nothing weird with that being an index from a homotopy perspective 
> (if my last mail is on target), because Nat is still a 0-groupoid. What causes 
> strangeness is indexing by Set i, not arbitrary inhabitants of Set (suc i). 
> Then again, we can create weird (to my naive observation) hybrids in Agda:
> 
>   data Maybe (T : Set1) : Set1 where
>     nothing : Maybe T
>     just    : T -> Maybe T
> 
> I'm not sure how to classify Maybe Set.
> 
> I suppose a possibility one could imagine is that things like Set i are 
> revealed to be ad-hoc (it does feel a bit that way), and that a more natural 
> hierarchy could be had by classifying i-groupoids (or categories) together 
> (not my idea originally of course). Then all 0-groupoids would be classified 
> together, and saying only they can be indices would be a straight-forward 
> characterization. Then again, I don't even know if such a hierarchy works, or 
> if it would be considered predicative if it did. And I'm not sure how 
> datatypes over 1-groupoids and above would fit in (and they are useful, 
> certainly).
> 
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>