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