On Sun, Sep 12, 2010 at 10:13 AM, Toby Bartels <toby@ugcs.caltech.edu> wrote:
Well, omega-categories are harder, but the Trimble--May approach (chapter 8 in the guidebook) makes sense in dependent type theory, because it also begins (paraphrasing page 138 in Cheng--Lauda): * a collection of objects; * for each pair x,y of objects, an (n-1)-category Hom(x,y); * for each tuple x_1,...,x_k of objects, ... etc.
This is also true of Batanin's definition, which takes as basic underlying data a globular set. A globular set is usually defined as a sequence of sets with functions between them, but it can also be defined as * a collection of objects, and * for each pair x,y of objects, a globular set Hom(x,y). (this is a coinductive definition, but that's okay). Most other definitions of higher categories can also be expressed "non-evilly" in a similar way. For instance, a simplicial set can also be defined as * a collection X_0 of 0-simplices, * for each pair x,y of 0-simplices, a collection X_1(x,y) of 1-simplices * for each triple x,y,z of 0-simplices and each choice of 1-simplices f,g,h in X_1(x,y), X_1(y,z), and X_1(x,z) respectively, a collection X_2(f,g,h) of 2-simplices * ... This is an infinite definition which is at best tricky to express coinductively, so it may not fit into an existing dependent type theory, but it is non-evil. The key here is the "Reedy category" structure of the simplex category \Delta, so the same idea applies to many other geometric structures for higher categories, thereby potentially including (I believe) pretty much all definitions of higher category.
Maybe my english isn't so "beautiful", but in all cases where "evil" has been used, what is wrong with "wrong" instead?
I agree that the word "evil" is too strong and has the wrong connotations (especially since, as Peter May recently pointed out, there do exist uses for "evil categories" or "strict categories"). On the other hand, to my mind calling something "wrong" implies that it is mathematically false or incorrect, which is not the case here. I like Andre's observation that it is a question of invariance, but does that suggest a term for the "non-invariant" notions? Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]