[Agda] Equivalence axiom => extensionality

[Dan Doel]

On Monday 19 July 2010 11:22:40 am Dan Licata wrote:
> (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.

Yes, certainly as they are now, they're distinct. Of course, there's no way in 
Agda to define a higher-dimensional structure (such that the dimensionality is 
enforced). Any inductive type is automatically discrete. I suppose part of 
fully embracing a (n-)groupoid/category model of computation might be allowing 
higher structures to be defined similarly to discrete ones.

But, another question is whether dimension and size need to be distinct, or 
whether you need the latter if you have the former. And as I said it isn't an 
idea I can claim. I've seen categorists discontented with the current set 
theoretic distinction of sets versus classes (or, hierarchies of set theoretic 
universes), because the "classes are 'too big' to be sets, and we get a 
paradox if we have a set of all sets" motivation isn't very satisfying.

What is somewhat more satisfying is: the natural structure of a collection of 
all sets is a category. So there should be a category of all sets. But, the 
right notion of equivalence in a category is isomorphism, and for our 
formalism to enforce this, we should not be able to talk about the set of all 
objects in a category, because it would allow isomorphic objects to be 
distinguished by equality. So, in such a formalism, the set of all sets is not 
disallowed merely by concerns of paradox, but because of a design principle.

Type theories like Agda are in a similar boat. So, if one follows the homotopy 
line of thought, it would be similarly interesting if the collection of n-
dimensional things was an (n+1)-dimensional thing, and that was all. But, as 
far as I know, no one has a formal enough specification of the idea to be 
confident that it avoids paradox in the same way that segregating things into 
different sizes does. And if it does, it's a further question whether it's 
predicative in the same way.

(It's also not clear that this approach wouldn't invalidate some actual 
mathematical practice. I'm pretty sure I've seen category theory that makes 
use of the idea that there is actually a set of objects, and anything that 
does so would have to be reformulated or thrown out. Also, is it problematic 
that some categories (say, arrow categories) are defined by taking as objects 
things that are already in a set by necessity?)

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

Yes. A fair amount of what I've seen with regard to talking about special 
'large' constructs happens to be in systems that don't have the sort of 
hierarchy Agda has. So 'large elimination' is elimination into Set, or 
functions spaces over Set, perhaps. So, I associated 'large index' with 
indexed-by-Set, which happens to be higher-dimensional as well, leading to the 
concern.

I can't really say that indexing by discrete types that are classified as 
large seems that concerning to me. But I can see how it leads the theory to be 
impredicative in a sense. I'm not particularly against impredicativity, and 
large-size indexing seems like a particularly weak form of it, but if we can 
get by well enough in a predicative system, so much the better.

-- Dan