Re: Evil in bicategories

Re: Evil in bicategories

[Michael Shulman]

On Mon, Sep 13, 2010 at 11:08 PM, Michael Shulman
<shulman@math.uchicago.edu> wrote:
> This is also true of Batanin's definition, which takes as basic
> underlying data a globular set....potentially including (I believe)
> pretty much all definitions of higher category.

I wrote this without thinking hard enough; sorry.  Of course, one also
has to consider the extra structure placed on the underlying data.
Extra structure of the "horn-filling" variety, as in Joyal's and
Street's definitions, consists of conditional assertions that certain
dependent types are inhabited, which is certainly "non-evil."  I would
expect that all the "non-algebraic" definitions could be dealt with
similarly; for instance, the Simpson-Tamsamani definition involves
also the assertion that certain maps of (n-1)-categories are
equivalences, which should itself be a "non-evil" assertion based
again on inhabitation of certain dependent types.  But it would be
tricky to write all of that out carefully.

For Batanin-type definitions, it is going to depend on what operad you
pick; for instance strict omega-categories are definitely "evil."  But
I would guess that if you use a "CW operad" which is built up freely,
as an operad, by attaching operations of successively higher dimension
whose boundaries are composite operations of lower dimension (which is
how I usually think of an operad for weak higher categories), then its
algebras should also be definable in a "non-evil" way.

Mike


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Vaughan Pratt]

On 9/13/2010 1:04 PM, Steve Vickers wrote (in response to Jean Benabou's
question as to whether CT is a religion):
> I'm not so sure of the answer for general category theory, but Topos
> Theory is undoubtedly a religion. At a monastery in Meteora, the monks
> have erected a sign saying "O topos einai ieros", i.e. "The topos is
> holy". And as Psalm 126 says, "He shall doubtless come again with
> rejoicing, bringing his sheaves with him."

For my part I'm not so sure of the answer for topos theory, but for
general category theory I would reply in the same vein as I did when
Paul Taylor opined to this list back in October of 1992:

    The strings, braids, etc., are a completely different matter.
    It is not belittling the work done on these topics, in
    Australia in particular, to say that they are of minority
    interest, compared to the use of the simpler forms of
    diagrams.

It seemed to me that Paul was making a religious issue out of category
theory that might have been sound English orthodoxy in those days but
that came across as heresy to Australian ears.  I therefore replied at
the time as follows.

=================================

Paul's representation of strings and braids as a flash in the category
theory pan is not borne out by the literature.  Strings have been an
integral part of the arrow business for a long time, witness Psalms
21:12, "Therefore shalt thou make them turn their back, when thou shalt
make ready thine arrows upon thy strings against the face of them."

Besides their supporting role with arrows, strings are also known to
every linguist and computer scientist to be an integral part of
language, as Mark 7:35 attests: "And straightway his ears were opened,
and the string of his tongue was loosed, and he spake plain."

Commutative algebra has been synonymous with mainstream algebra for a
long time.  But noncommutative algebra has been more than just a cottage
industry for many years, and moreover has found a warmer welcome in
linguistics and CS than the commutative variety, providing us with an
algebraic basis for Turing machine computations and formal grammar
derivations, both of which can be conveniently laid out in the
(oriented) plane, where they lend themselves to a 2-categorical formulation.

But as Zadeh reminds us, we live in a fuzzy world, neither clearly
commutative nor clearly orientedly planar, but somewhere in between.
The laws of this in-between world are braidal, with planarity
corresponding to the initial or discrete braids and commutativity to the
final braids, which can pass through themselves without losing their
identity altogether (commutativity without idempotence).  Under these
circumstances we can only keep our 2-categorical cool with braids,
suggesting the following slogan:

      Braids are the rule, of which commutativity and noncommutativity
are its two extremes.

This appears to be a natural idea in both senses of "natural."	It is a
natural mathematical idea to suggest and pursue; and it appears to be
one that can be found in nature, witness the Yang-Baxter equations
arising early on in physics, whose braidal character is now clear and
about which several mathematical physicists have started writing, e.g.
John Baez's recent MIT lecture notes on "Braids and Quantization."

Nor would I be accusing Ross of riding a bandwagon if I suggest that in
five years' time he'll probably be interested in something else and
drawing a completely different kind of diagram.

Nor would I be calling Paul shortsighted if I suggest that in five years
time many of us in both mathematics and physics, and conceivably even
philosophy, will be drawing braids.  (This is not to suggest that Jon
Barwise's reaction to my explanation of linear logic last February would
have been any different had I omitted the section on braids, which
included five braid diagrams I had to do in ASCII that I am looking
forward to being able to render in Taylorese.)

As for Ross, I rather expect that in five years time he will be drawing
whatever it is that those of us in the trenches will be drawing in ten
years time, and one might hope that these too would appear in some
diagram package, preferably in 1997 rather than 2002.

Meanwhile others on the fringe of the expanding categorical cosmos will
only just be learning to use commutative \square's.

This brings me back to my first theme.	Categories have been a pons
asinorum for "the rest of us" for a very long time, ever since the exam
in category theory given to the young lad who appeared briefly in the
story of David and Jonathan [I Samuel 20:21-22]:

      And, behold, I will send a lad, saying, "Go, find out the arrows."
If I expressly say unto the lad, "Behold, the arrows are on this side of
thee, take them;" then come thou: for there is peace to thee, and no
hurt; as the Lord liveth.  But if I say thus unto the young man,
"Behold, the arrows are beyond thee;" go thy way: for the LORD hath sent
thee away.

As it turned out the arrows were indeed beyond the lad, who "knew not
anything, only David and Jonathan knew the matter," and the lad was sent
off to the city [20:37-40], a drop-out who for all we know may have
later become the Bill Gates of his day.

Another biblical character who struggled mightily with the subject was
Job.  "For the arrows of the Almighty are within me, the poison whereof
drinketh up my spirit: the terrors of God do set themselves in array
against me." [Job 6:4]  One imagines him tackling either metacategories
or coherence on that occasion.

Job was thus afflicted for a long time, during which he complained
bitterly of his plight to his three friends and the Lord in three major
jam-sessions.  In the last of these, the Lord showed up in a Whirlwind
evidently hoping to be able undo Satan's mischief and set things
straight at last.  After spending the better part of three chapters
extolling the virtues of His nobler creatures and getting Job into the
proper frame of mind, the Lord came to the whale, of which He said "The
arrow cannot make him flee." [Job 41:28]  That apparently did the
trick:	Job immediately apologized for his ignorance of the subject: "I
have heard of thee by the hearing of the ear, but now mine eye seeth
thee.  Wherefore I abhor myself, and repent in dust and ashes." [Job
42:5-6].

The Lord then in unexpectedly firm tones told Job's friends that Job now
understood the subject better even than they did and to treat him
properly henceforth.  And He gave Job twice what he had before.  This
came to 14,000 sheep, 6,000 camels, 1,000 oxen, 1,000 she-asses, 7 sons,
and 3 daughters, so you can figure out what he had before, at least for
the livestock.  If Job's arrow anxiety lasted 25-35 years, that's around
2-3% p.a., probably a good rate for those days.

But I digress.	Anyway you can read it for yourself, you'll see it's
exactly as I said.

Coming from the electrical engineering side of the business myself, the
advice to "Cast forth lightning, and scatter them: shoot out thine
arrows, and destroy them." [Psalms 144:6] speaks more directly to me.

 	Vaughan Pratt



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Richard Garner]

Two that spring to mind are "inflexible" (after Kelly) or "impersistent"
(after Paré).

On 13 September 2010 10:16, David Roberts <droberts@maths.adelaide.edu.au>wrote:

> Dear Jean,
>
> You wrote:
>> Maybe my english isn't so "beautiful", but in all cases where "evil" has
>> been used, what is wrong with "wrong" instead?
>
> I'm not so enamoured with the use of the word 'evil', but it seems to
> be more entrenched than perhaps it was intended, namely as a joke.
> Regardless of my personal convictions, I like to remain a mathematical
> agnostic, so 'wrong' seems to me to be too strong. In my everyday
> mathematical work I use choice and excluded middle and equality at
> will, but I know that these foundational ideas ('evil' in categories,
> constuctivism etc) exist and are useful and interesting.
>
> Unfortunately I don't have any decent alternatives to offer, but the
> philosophy boils down to, in my opinion, a structuralist view of
> foundations (as opposed to the standard ZF with 'member of'
> foundations) combined with (even a simple grasp of) type theory. The
> former is essentially the 'sets are bags of points' approach and the
> latter is the 'you can't ask: is \pi = (sin:R \to [-1,1])?' idea.
> Perhaps readers of this list with the inclination and an eye for
> nomenclature will suggest some words.
>
> Toby Bartels calls categories where one is not allowed to test for
> equality between arbitrary objects 'weak' and those where one can do
> so 'strict' (most often these latter are internal categories in some
> version of Set, or perhaps using universes). This reflects thinking
> about higher categories (and completely exemplified by Makkai's
> approach via FOLDS). This terminology takes the 'moral dimension' out
> of talking about serious foundational ideas. But we don't have a word
> that replaces 'evil' in this context that conveys the sort of mild
> disdain for attempting to make the naive mistake of trying to ask if a
> scalar is contained in a vector, as one can do in traditional
> foundations (note that the answer depends on how one defines tuples).
>
> That's my two cents, for what it's worth.
> David
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Miles Gould]

On Sun, Sep 12, 2010 at 02:38:09PM +0200, JeanBenabou wrote:
> Maybe my english isn't so "beautiful", but in all cases where "evil"
> has been used, what is wrong with "wrong" instead?

An obvious reason not to do this is that "wrong" can also mean
"incorrect" in English, and plenty of definitions are evil but correct.

[It's probably irrelevant, but the term "evil" is well-established among
programmers in a broadly similar sense: "evil does not imply incompetence
or bad design, but rather a set of goals or design criteria fatally
incompatible with the speaker's". See
http://catb.org/jargon/html/E/evil.html .]

Miles

-- 
Time is an illusion; lunchtime doubly so.
   -- Ford Prefect


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Toby Bartels]

David Roberts wrote in part:

>Jean Bénabou wrote:

>>Maybe my english isn't so "beautiful", but in all cases where "evil" has
>>been used, what is wrong with "wrong" instead?

>I'm not so enamoured with the use of the word 'evil', but it seems to
>be more entrenched than perhaps it was intended, namely as a joke.
>Regardless of my personal convictions, I like to remain a mathematical
>agnostic, so 'wrong' seems to me to be too strong.

I feel the same way, which is why I *prefer* to say "evil" instead of "wrong".
The word "evil" is so over-the-top that someone who uses it *must* be kidding.
However, the word "wrong" sounds like it should be taken seriously,
but the mathematics of strict categories is valid, not wrong at all.
(It's just not the mathematics that I'm doing when I do category theory.)

Incidentally, this usage of "evil" fits in with a usage of "morally"
examined by Eugenia Cheng: http://www.cheng.staff.shef.ac.uk/morality/.
"Morally", one cannot compare objects of a given category for equality
(because the results are not preserved by an equivalence of categories);
even if it is possible, it is "evil".

>Toby Bartels calls categories where one is not allowed to test for
>equality between arbitrary objects 'weak' and those where one can do
>so 'strict'

Right: http://ncatlab.org/nlab/show/strict+category

In many cases, we can use "strict" instead of "evil".
For example, here is David Leduc's original post:

>>>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?

Let us replace each usage of "evil" by "too strict":

>>>In a bicategory, composition of 1-cells is associative up to
>>>isomorphism. Because it would be too strict 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 too strict? 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 even makes David's use of the verb "weaken" look very nice.

So while I like the noun "evil" to encapsulate the whole idea
(with the understanding that is not too be taken too seriously),
one can probably avoid it in serious mathematical questions.
(I don't mean to criticise David for using it, however.)


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[David Roberts]

Dear Jean,

You wrote:
> Maybe my english isn't so "beautiful", but in all cases where "evil" has
> been used, what is wrong with "wrong" instead?

I'm not so enamoured with the use of the word 'evil', but it seems to
be more entrenched than perhaps it was intended, namely as a joke.
Regardless of my personal convictions, I like to remain a mathematical
agnostic, so 'wrong' seems to me to be too strong. In my everyday
mathematical work I use choice and excluded middle and equality at
will, but I know that these foundational ideas ('evil' in categories,
constuctivism etc) exist and are useful and interesting.

Unfortunately I don't have any decent alternatives to offer, but the
philosophy boils down to, in my opinion, a structuralist view of
foundations (as opposed to the standard ZF with 'member of'
foundations) combined with (even a simple grasp of) type theory. The
former is essentially the 'sets are bags of points' approach and the
latter is the 'you can't ask: is \pi = (sin:R \to [-1,1])?' idea.
Perhaps readers of this list with the inclination and an eye for
nomenclature will suggest some words.

Toby Bartels calls categories where one is not allowed to test for
equality between arbitrary objects 'weak' and those where one can do
so 'strict' (most often these latter are internal categories in some
version of Set, or perhaps using universes). This reflects thinking
about higher categories (and completely exemplified by Makkai's
approach via FOLDS). This terminology takes the 'moral dimension' out
of talking about serious foundational ideas. But we don't have a word
that replaces 'evil' in this context that conveys the sort of mild
disdain for attempting to make the naive mistake of trying to ask if a
scalar is contained in a vector, as one can do in traditional
foundations (note that the answer depends on how one defines tuples).

That's my two cents, for what it's worth.
David


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Toby Bartels]

>Ah, it's only for bicategories. I was expecting a definition in
>dependent type theory of omega-categories. That would have helped me
>understanding it.

Well, omega-categories are harder, but the Trimble--May approach
(chapter 8 in the guidebook) makes sense in dependent type theory,
because it also begins (paraphrasing page 138 in Cheng--Lauda):
*  a collection of objects;
*  for each pair x,y of objects, an (n-1)-category Hom(x,y);
*  for each tuple x_1,...,x_k of objects, ... etc.
Although Cheng--Lauda says that the objects form a set
(so that, by default, it makes sense to compare them for equality),
we never actually compare them for equality in the definition.
So it is explicitly non-evil.

(This is not to say that other definitions of higher category are evil;
if they are equivalent to Trimble's definition, then they are not.
But they are not usually *explicitly* non-evil;
if they make reference to equality of objects anywhere,
then they must be written in a language in which evil can be expressed.)

In an almost completely different direction,
Makkai's "multitopic" approach to omega-categories
is also explicitly non-evil (and explicitly dependently typed too).
Makkai's approach is non-algebraic (in the Cheng--Lauda sense),
since it is based on composition predicates, not operations.
In fact, Makkai's language does not allow one to speak of operations!

(If X and Y are sets, that is types with equality predicates,
then a function from X to Y can be defined as a relation on X and Y
satisfying an axiom that makes reference to equality on Y.
But if X and Y are types WITHOUT equality predicates,
then an operation from X to Y can't be defined as a predicate on X and Y.
Trimble's definition of n-category uses types and operations,
while Makkai's definition of omega-category uses types and predicates.)


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Peter LeFanu Lumsdaine]

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), 
  we have the composite
g.f \in Mor(x,z).

So we never have an axiom "src(g.f) = src(f)"; this is just part of the _typing_ of composition.  

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é. 

-p.

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[JeanBenabou]

Dear  all,

Although I'm not a very "religious" person, I respect all religions,  
and I also deeply respect, of course, Category Theory. I hope someone  
will answer the following question:

Is Category Theory a religion?

As far as I know, it is the only part of mathematics (or of many  
other sciences) where words such as "dogma", "doctrine" (let alone  
hyper ones) are used. Recently a few other words with the same  
religious connotation have been added.
The most frequent one being "evil"

Maybe my english isn't so "beautiful", but in all cases where "evil"  
has been used, what is wrong with "wrong" instead?


Le 11 sept. 10 à 04:05, David Leduc a écrit :

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

Re: Evil in bicategories

[David Leduc]

> You can see examples at http://ncatlab.org/nlab/show/bicategory

Ah, it's only for bicategories. I was expecting a definition in
dependent type theory of omega-categories. That would have helped me
understanding it.

> The answer is the same: when stating the associativity law,
> you begin with objects W,X,Y,Z and go on from there.

Yes, it makes sense. Thank you.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Toby Bartels]

David Leduc wrote:

>You both mention a definition of higher categories based on dependent
>type theory.
>Where does it appear?
>I cannot find such definition in the guide book by Cheng and Lauda.
>Can/has it be implemented in a proof assistant like Coq?

Most authors (including Cheng and Lauda) don't get into
the logical details of what is and is not evil,
so they don't discuss how it works in dependent type theory.
Nevertheless, any definition of bicategory that runs like this:
*  a collection of objects;
*  for each pair of objects, a collection of morphisms;
*  etc
is written the language of dependent type theory.

You can see examples at http://ncatlab.org/nlab/show/bicategory
(the brief definition is perfectly explicit in this way,
although it does not include all of the details;
the detailed definition leaves the declarations of some variables implicit,
although you could always stick their definitions up front,
making it a complete and perfectly explict dependent-type definition).

Actually, talking about bicategories is a red herring;
all of the issues come up already for categories.
You might as well have asked, in your original post,
why we know that the source and target of (h o g) o f and h o (g o f)
are equal when stating the associativity law in the definition of a category.
The answer is the same: when stating the associativity law,
you begin with objects W,X,Y,Z and go on from there.

I haven't seen a definition of bicategories in Coq,
but certainly the explicit definition on the nLab could be done in Coq.
But as I said, the issues already arise for ordinary categories.
For a definition of these in Coq, see http://coq.inria.fr/contribs/ConCaT.html
with http://coq.inria.fr/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.Category.html
as the file that contains the definition of category itself.
(Although Coq has equality at all types, and so can express evil,
this equality is never used except within a given hom-set,
as you can see in that file and also in the other files there.)


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[David Leduc]

Hi Toby and David,

Toby Bartels <toby+categories@ugcs.caltech.edu> wrote:
> The non-evil algebraic definitions of higher categories
> are based on dependent type theory,

You both mention a definition of higher categories based on dependent
type theory.
Where does it appear?
I cannot find such definition in the guide book by Cheng and Lauda.
Can/has it be implemented in a proof assistant like Coq?

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[Jocelyn Paine]

On Sat, 11 Sep 2010, 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?
>

Your question made me wonder why the axioms for ordinary categories, i.e.
1-categories, insist that in composing f:A->B and g:C->D, B and C must be
equal. Isn't it just as evil not to allow them to be merely isomorphic?

Jocelyn Paine
http://www.j-paine.org

Jocelyn's Cartoons:
http://www.j-paine.org/blog/jocelyns_cartoons/


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Evil in bicategories

[David Roberts]

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

Re: Evil in bicategories

[Toby Bartels]

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

Evil in bicategories

[David Leduc]

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