Ah, it's only for bicategories. I was expecting a definition in dependent type theory of omega-categories. That would have helped me understanding it.
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. Although Cheng--Lauda says that the objects form a set (so that, by default, it makes sense to compare them for equality), we never actually compare them for equality in the definition. So it is explicitly non-evil. (This is not to say that other definitions of higher category are evil; if they are equivalent to Trimble's definition, then they are not. But they are not usually *explicitly* non-evil; if they make reference to equality of objects anywhere, then they must be written in a language in which evil can be expressed.) In an almost completely different direction, Makkai's "multitopic" approach to omega-categories is also explicitly non-evil (and explicitly dependently typed too). Makkai's approach is non-algebraic (in the Cheng--Lauda sense), since it is based on composition predicates, not operations. In fact, Makkai's language does not allow one to speak of operations! (If X and Y are sets, that is types with equality predicates, then a function from X to Y can be defined as a relation on X and Y satisfying an axiom that makes reference to equality on Y. But if X and Y are types WITHOUT equality predicates, then an operation from X to Y can't be defined as a predicate on X and Y. Trimble's definition of n-category uses types and operations, while Makkai's definition of omega-category uses types and predicates.) --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]