Re: Evil in bicategories

[Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>]

On 10 Sep 2010, at 23:05, David Leduc wrote:

> In a bicategory, composition of 1-cells is associative up to
> isomorphism. Because it would be evil to insist that h o (g o f) is
> equal to (h o g) o f. However the source and target objects of those
> compositions must be equal. Isn't it evil? Why not weaken this
> requirement by saying that the sources (respectively, targets) of h o
> (g o f) and (h o g) o f must only be isomorphic?

This question can be asked not just in bicategories but even in categories, and not just with associativity but even for a single composite: the source and target of a composite are objects, so it's already evil (well... I'd prefer to just say "uncategorical") to ask if they're equal.

There are two main flavours of answer: pragmatic and principled.

The pragmatic one is: well, just try to give a definition that lets them only be isomorphic!  It's hopeless... because to do anything with the composites, you then need to compose them with those isomorphisms, but then you end up with more isomorphisms, proliferating endlessly, and it gets more and more hopeless; it's worse than trying to to get a group of mathematicians to agree where to go for dinner.

The principled answer is, of course, the _right_ one, but if you've first confronted the pragmatic answer, it's much more likely to seem a welcome and elegant relief rather than a sneaky technicality.

In one line: think of categories not just as an essentially algebraic theory, but as a theory in some logic with _type-dependency_.

But that's probably meaningless except to people who already know it, so in more detail: don't think of categories as having a type "Mor" and a type "Ob" with operations "src", "tgt" between them.  Rather, think of these as a _type dependency_: go back to the older style of definition which says that there's a type "Ob", and for any two objects x,y \in Ob, there's a type "Mor(x,y)".  So we can never even _talk_ about a morphism without bearing in mind what its source and target are.

[If you're not familiar with this terminology, think of "type"(noun) as synonymous with "set"; some people draw distinctions in how they use the two, others don't, but at least to a first approximation it's close enough.]

Now, we can type the composition operation a bit more precisely:

for any x,y,z \in Ob, and any f \in Mor(x,y), g \in Mor(y,z), 
  we have the composite
g.f \in Mor(x,z).

So we never have an axiom "src(g.f) = src(f)"; this is just part of the _typing_ of composition.  

On a formal level, we can do all this by formalising categories in something like Makkai's "FOLDS" ("first-order logic with dependent sorts") ("sorts" is just another name for "types"), or more economically, in just an algebraic logic with dependent sorts.  In such a system, we can set it up with no way to even _talk_ about equality of objects; as we've (partly) seen, the type-dependency is expressive enough to capture the details we need, while being not nearly as strong as having equality of objects around in general.


The first appearance in print that I know of is in Makkai's papers on FOLDS and related systems.  Iirc, it's also discussed very nicely in some of Mike Shulman's early posts on the n-category Café. 

-p.

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]