Re: Evil in bicategories

[Toby Bartels <toby@ugcs.caltech.edu>]

>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/ ]