From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6138 Path: news.gmane.org!not-for-mail From: David Roberts Newsgroups: gmane.science.mathematics.categories Subject: Re: Evil in bicategories Date: Sun, 12 Sep 2010 10:58:01 +0930 Message-ID: References: Reply-To: David Roberts NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: dough.gmane.org 1284320529 2778 80.91.229.12 (12 Sep 2010 19:42:09 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sun, 12 Sep 2010 19:42:09 +0000 (UTC) Cc: categories To: David Leduc Original-X-From: majordomo@mlist.mta.ca Sun Sep 12 21:42:07 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpy.mta.ca ([138.73.1.139]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OusRD-0002rF-Fx for gsmc-categories@m.gmane.org; Sun, 12 Sep 2010 21:42:07 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:39948) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OusQ2-00055Z-Il; Sun, 12 Sep 2010 16:40:54 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OusPy-0001oF-2N for categories-list@mlist.mta.ca; Sun, 12 Sep 2010 16:40:50 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6138 Archived-At: 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 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/ ]