From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6137 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: Evil in bicategories Date: Sat, 11 Sep 2010 16:23:58 -0700 Message-ID: References: Reply-To: Toby Bartels NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: dough.gmane.org 1284320491 2599 80.91.229.12 (12 Sep 2010 19:41:31 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sun, 12 Sep 2010 19:41:31 +0000 (UTC) Cc: David Leduc To: categories Original-X-From: majordomo@mlist.mta.ca Sun Sep 12 21:41:29 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 1OusQY-0002YK-FJ for gsmc-categories@m.gmane.org; Sun, 12 Sep 2010 21:41:26 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:39943) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OusOx-00051y-GI; Sun, 12 Sep 2010 16:39:47 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OusOu-0001n5-C8 for categories-list@mlist.mta.ca; Sun, 12 Sep 2010 16:39:44 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6137 Archived-At: 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/ ]