[Agda] Equivalence axiom => extensionality

[Dan Doel]

On Tuesday 29 June 2010 7:18:46 am Peter LeFanu Lumsdaine wrote:
> On 29 Jun 2010, at 01:22, Dan Doel wrote:
> > Is this a renaming of the notion of equivalence of n-categories?
> 
> Yep --- or at least of the n-categories themselves, not the notion of
> equivalence.  Maybe this is a good place to go into more of the background
> to this thread:

Something popped into my head regarding this while contemplating another 
topic: would this not rather invalidate or at least significantly change the 
meaning of some inductive families as implemented in Agda? Agda allows 
families with large indices, so one can write:

  data Rep : Set -> Set where
    N  : Rep Nat
    B  : Rep Bool
    F2 : Rep (Fin 2)
    ...

I'd previously heard Conor McBride remark that it's sort of an open problem 
whether such "large" indices are okay. I'd previously thought, "what could be 
wrong with them?" But, it occurred to me that they are in conflict with the 
above idea of equivalences. For instance, Bool is isomorphic to Fin 2, so (if 
my understanding of homotopy lambda calculi/type theory/whatnot is correct), 
any predicate P : Set -> Set which holds for Bool should also hold for Fin 2. 
Here we have non-identical proofs for the two, and we could remove one and get 
a predicate which fails to hold for one of the two, and violates the 
principle.

Alternately, we could view Rep as being implemented via equality types and 
get:

  data Rep (S : Set) : Set where
    N  : S = Nat   -> Rep S
    B  : S = Bool  -> Rep S
    F2 : S = Fin 2 -> Rep S

In which case, the B constructor should work not just for Bool itself, but for 
any type isomorphic to Bool (and so F2 is redundant).

Or, for another way to look at it (which relates to what caused me to think of 
the issue), it seems like the homotopy approach is a little more committed to 
a certain sort of parametricity (though perhaps more limited than what the 
word usually means) for Set, whereas inductive families with large indices 
commit to a more discrete Set.

And by contrast, sets (1-sets) themselves would remain sensible indices 
without any modification, being discrete already.

-- Dan