[Agda] Equivalence axiom => extensionality

[Dan Doel]

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