Re: Evil in bicategories

[David Roberts <droberts@maths.adelaide.edu.au>]

Hi David,

We had a discussion about this at some point in the n-group
(n-category cafe, nLab etc), and it isn't evil to assume that source
and target must be equal, as this is a _typing_ issue, rather than an
equality predicate. A morphism f in a 1-category C is an element of
the set C(a,b) with a = s(f) and b=t(f). In this set it is not evil to
test for equality (unless one has gone so far as to negate equality on
hom-sets, but then I can't help you!). Composition is _defined_ as a
map

C(a,b) x C(b,c) ----> C(a,c)

and so even in a 1-category without an equality predicate on the
collection of objects, it isn't evil to say, for example that a square
commutes (i.e. the two composites of two different pairs of morphisms
are equal).

It is no different in a bicategory B: it may be evil to assert that
two arbitrary 1-arrows are equal, but the hom-categories are indexed
by the objects (I don't know if this requires an extension of
dependent type theory, or if one can have types depending on types,
themselves dependent on something else - I'm no expert on DTT). Thus
for two objects of a hom-category B(a,b) you may not assert two are
equal, but you do know that they have the same source a and target b.

David Roberts

On 11 September 2010 11:35, David Leduc <david.leduc6@googlemail.com> 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?
>


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