[Agda] Equivalence axiom => extensionality

[Andreas Abel]

On Jul 17, 2010, at 5:17 AM, Dan Doel wrote:
> 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

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

Such a definition can be justified for impredicative Set, but I have  
not yet seen any predicative semantics that handles it.

> 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.

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/