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/ ]
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/ ]
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/ ]
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/ ]
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/ ]
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/ ]
To All, A few thoughts about the "evilness" of equality. There is a well established doctrine, possibly going back to Felix Klein, that mathematical reality should be described in invariant terms. For examples, many aspects of the theory of vector spaces can be developed independantly of the choice of a basis. The fact that the (in)equality relation between the objects of a category is not respected by equivalences of categories can be disturbing. By loosing its invariance, the relation seems to be loosing its objectivity, its value. This is why some category theorists have declared war on it by calling it "evil". The cardinality of the set of objects of a category is not invariant under equivalences. Similarly, the cardinality of the set of points of a topological space is not invariant under homotopy equivalences. Where is the problem? Best, andré -------- Message d'origine-------- De: JeanBenabou [mailto:jean.benabou@wanadoo.fr] Date: dim. 12/09/2010 08:38 À: David Leduc Cc: categories Objet : categories: Re: Evil in bicategories 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? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
I suggest "kosher" David Roberts 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/ ]
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/ ]
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/ ]
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/ ]
Dear Jean, 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." Best wishes, Steve Vickers. On 12 Sep 2010, at 13:38, JeanBenabou wrote:
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?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
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/ ]
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/ ]
On Sun, Sep 12, 2010 at 10:13 AM, Toby Bartels <toby@ugcs.caltech.edu> wrote:
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.
This is also true of Batanin's definition, which takes as basic underlying data a globular set. A globular set is usually defined as a sequence of sets with functions between them, but it can also be defined as * a collection of objects, and * for each pair x,y of objects, a globular set Hom(x,y). (this is a coinductive definition, but that's okay). Most other definitions of higher categories can also be expressed "non-evilly" in a similar way. For instance, a simplicial set can also be defined as * a collection X_0 of 0-simplices, * for each pair x,y of 0-simplices, a collection X_1(x,y) of 1-simplices * for each triple x,y,z of 0-simplices and each choice of 1-simplices f,g,h in X_1(x,y), X_1(y,z), and X_1(x,z) respectively, a collection X_2(f,g,h) of 2-simplices * ... This is an infinite definition which is at best tricky to express coinductively, so it may not fit into an existing dependent type theory, but it is non-evil. The key here is the "Reedy category" structure of the simplex category \Delta, so the same idea applies to many other geometric structures for higher categories, thereby potentially including (I believe) pretty much all definitions of higher category.
Maybe my english isn't so "beautiful", but in all cases where "evil" has been used, what is wrong with "wrong" instead?
I agree that the word "evil" is too strong and has the wrong connotations (especially since, as Peter May recently pointed out, there do exist uses for "evil categories" or "strict categories"). On the other hand, to my mind calling something "wrong" implies that it is mathematically false or incorrect, which is not the case here. I like Andre's observation that it is a question of invariance, but does that suggest a term for the "non-invariant" notions? Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
participants (14)
-
David Leduc -
David Roberts -
Eduardo J. Dubuc -
JeanBenabou -
Jocelyn Paine -
Joyal, André -
Michael Shulman -
Miles Gould -
Peter LeFanu Lumsdaine -
Richard Garner -
Steve Vickers -
Toby Bartels -
Toby Bartels -
Vaughan Pratt