From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6145 Path: news.gmane.org!not-for-mail From: Peter LeFanu Lumsdaine Newsgroups: gmane.science.mathematics.categories Subject: Re: Evil in bicategories Date: Sun, 12 Sep 2010 13:52:42 -0300 Message-ID: References: Reply-To: Peter LeFanu Lumsdaine NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v1081) Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1284321172 5267 80.91.229.12 (12 Sep 2010 19:52:52 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sun, 12 Sep 2010 19:52:52 +0000 (UTC) Cc: categories To: David Leduc Original-X-From: majordomo@mlist.mta.ca Sun Sep 12 21:52:49 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 1OusbZ-0006u7-DF for gsmc-categories@m.gmane.org; Sun, 12 Sep 2010 21:52:49 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:52078) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OusaN-0005nS-W2; Sun, 12 Sep 2010 16:51:36 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OusaK-000248-Af for categories-list@mlist.mta.ca; Sun, 12 Sep 2010 16:51:32 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6145 Archived-At: On 10 Sep 2010, at 23:05, 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? This question can be asked not just in bicategories but even in = categories, and not just with associativity but even for a single = composite: the source and target of a composite are objects, so it's = already evil (well... I'd prefer to just say "uncategorical") to ask if = they're equal. There are two main flavours of answer: pragmatic and principled. The pragmatic one is: well, just try to give a definition that lets them = only be isomorphic! It's hopeless... because to do anything with the = composites, you then need to compose them with those isomorphisms, but = then you end up with more isomorphisms, proliferating endlessly, and it = gets more and more hopeless; it's worse than trying to to get a group of = mathematicians to agree where to go for dinner. The principled answer is, of course, the _right_ one, but if you've = first confronted the pragmatic answer, it's much more likely to seem a = welcome and elegant relief rather than a sneaky technicality. In one line: think of categories not just as an essentially algebraic = theory, but as a theory in some logic with _type-dependency_. But that's probably meaningless except to people who already know it, so = in more detail: don't think of categories as having a type "Mor" and a = type "Ob" with operations "src", "tgt" between them. Rather, think of = these as a _type dependency_: go back to the older style of definition = which says that there's a type "Ob", and for any two objects x,y \in Ob, = there's a type "Mor(x,y)". So we can never even _talk_ about a morphism = without bearing in mind what its source and target are. [If you're not familiar with this terminology, think of "type"(noun) as = synonymous with "set"; some people draw distinctions in how they use the = two, others don't, but at least to a first approximation it's close = enough.] Now, we can type the composition operation a bit more precisely: for any x,y,z \in Ob, and any f \in Mor(x,y), g \in Mor(y,z),=20 we have the composite g.f \in Mor(x,z). So we never have an axiom "src(g.f) =3D src(f)"; this is just part of = the _typing_ of composition. =20 On a formal level, we can do all this by formalising categories in = something like Makkai's "FOLDS" ("first-order logic with dependent = sorts") ("sorts" is just another name for "types"), or more = economically, in just an algebraic logic with dependent sorts. In such = a system, we can set it up with no way to even _talk_ about equality of = objects; as we've (partly) seen, the type-dependency is expressive = enough to capture the details we need, while being not nearly as strong = as having equality of objects around in general. The first appearance in print that I know of is in Makkai's papers on = FOLDS and related systems. Iirc, it's also discussed very nicely in = some of Mike Shulman's early posts on the n-category Caf=E9.=20 -p.= [For admin and other information see: http://www.mta.ca/~cat-dist/ ]