Re: Evil in bicategories

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

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?

What do you mean, the source and target are equal?
Nobody said anything about that until YOU brought it up,
so the evil is YOUR fault, not the bicategory's.

I'm being facetious, of course, but here's the serious version:

The non-evil algebraic definitions of higher categories
are based on dependent type theory, and you are not allowed
to mention a 1-cell until you have got a type for it,
which requires mentioning two 0-cells first.
But once you mention these 0-cells, you may refer to them again.

So the associativity-up-to-isomorphism clause does NOT begin:
For all f,g,h such that (g o f) and (h o g) exist, ...;
that would indeed be evil (already when claiming that g o f exists).
Instead, the clause begins:  For all 0-cells W,X,Y,Z
and all 1-morphisms f: W -> X, g: X -> Y, h: Y -> Z,
there is an isomorphism a_{f,g,h}: h o (g o f) -> (h o g) o f.
(Then coherence requirements follow.)

Once you pick 0-cells W,X,Y,Z, you have access to some dependent types:
the type of 1-cells from W to X, the type of 1-cells from W to Z, etc.
The fact that "W" shows up in both places is not evil;
you are just talking about W twice, not claiming that W = W
(innocuous as that might seem, you're not even doing that).


--Toby

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