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