Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownIf you're not following the `categories` mailing list, then you're missing out on a great discussion of [[evil]]. [[Peter Selinger]] has come from the list to the Lab to discuss it here too!

   If you're not following the categories mailing list, then you're missing out on a great discussion of evil. Peter Selinger has come from the list to the Lab to discuss it here too!

2. • CommentRowNumber2.
   • CommentAuthorAndrew Stacey
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownOh goody! When I read his post this morning I was sorely tempted to send a reply saying "Put this on the nLab!".

   Oh goody! When I read his post this morning I was sorely tempted to send a reply saying "Put this on the nLab!".

3. • CommentRowNumber3.
   • CommentAuthordomenico_fiorenza
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: domenico_fiorenza
   Format: Htmlthanks. by the way, it seems to me that something like "let <latex>F:C\to D_1</latex> and <latex>\tilde{F}:C\to D_2</latex> be functors; consider the set of functors <latex>G:D_1\to D_2</latex> such that <latex>G\circ F=\tilde{F}</latex>" is evil, unless all categories involved are small. so I find there's a touch of evil in the definition of [[over quasi-category]] and in those built over it, e.g., [[limit]]. it is not hard to make these definitions/constructions non-evil, and I'm planning to revise them in this direction. but this points to a more fundamental question: quasi-categories seems to generalize small categories rather than categories; though the distinction between small and non small category is something whose formalization goes to the heart of foundations of set theory (what really is Objects(C)? a set? a class? which is the difference?), at least naively one can use the principle "think of Objects(C) as a set, but never never never say that two objects are equal: say that they are isomorphic, and specify the isomorphism between them" so a naive principle for weak categories would be "think to a n-quasi-category as a weak kan complex where you are never never never allowed to say that two simplices of dimension lower than n are equal." for instance, the nerve of a category is a 1-quasi-category.

   thanks. by the way, it seems to me that something like "let and be functors; consider the set of functors such that " is evil, unless all categories involved are small. so I find there's a touch of evil in the definition of over quasi-category and in those built over it, e.g., limit. it is not hard to make these definitions/constructions non-evil, and I'm planning to revise them in this direction. but this points to a more fundamental question: quasi-categories seems to generalize small categories rather than categories; though the distinction between small and non small category is something whose formalization goes to the heart of foundations of set theory (what really is Objects(C)? a set? a class? which is the difference?), at least naively one can use the principle "think of Objects(C) as a set, but never never never say that two objects are equal: say that they are isomorphic, and specify the isomorphism between them" so a naive principle for weak categories would be "think to a n-quasi-category as a weak kan complex where you are never never never allowed to say that two simplices of dimension lower than n are equal." for instance, the nerve of a category is a 1-quasi-category.
4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownI don't see what smallness has to do with it. If we start with set theory and try to define higher concepts within that, then we will be able to speak evil, because all of our collections will form sets. Whether these sets are small or large (call the latter ‘classes’ if you like) makes no difference. So we need to test for evil, either by trying to see if equality of objects (and the like) is ever mentioned, or by applying definitions like those proposed at [[evil]]. On the other hand, if we use some form of type theory, or a logic like FOLDS, in which we cannot always state equalities, then we might be able to avoid evil syntactically.

   I don't see what smallness has to do with it. If we start with set theory and try to define higher concepts within that, then we will be able to speak evil, because all of our collections will form sets. Whether these sets are small or large (call the latter ‘classes’ if you like) makes no difference. So we need to test for evil, either by trying to see if equality of objects (and the like) is ever mentioned, or by applying definitions like those proposed at evil.

   On the other hand, if we use some form of type theory, or a logic like FOLDS, in which we cannot always state equalities, then we might be able to avoid evil syntactically.

5. • CommentRowNumber5.
   • CommentAuthordomenico_fiorenza
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: domenico_fiorenza
   Format: Htmlindeed, what I wrote is really badly expressed. I see your point: evilness has nothing to do with the size. the fact is that with small categories it is easy to speak evil without noticing.. :) still I hope some sense in what I wrote can be found, despite its set theoretic weirdness..

   indeed, what I wrote is really badly expressed. I see your point: evilness has nothing to do with the size. the fact is that with small categories it is easy to speak evil without noticing.. :) still I hope some sense in what I wrote can be found, despite its set theoretic weirdness..
6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownIt's quite true that quasi-categories are a set-theoretic approach to higher categories. (You can, however, talk about "large quasi-categories" in the size-theoretic sense, without any problems.) However, I don't think the "evil" definitions should be changed; part of the point of quasi-category theory (and of the model categorical approach to higher category theory in general) is that you can use "strict" or "evil" constructions, carefully, to more easily talk about the "real" underlying "non-strict" notions.

   It's quite true that quasi-categories are a set-theoretic approach to higher categories. (You can, however, talk about "large quasi-categories" in the size-theoretic sense, without any problems.) However, I don't think the "evil" definitions should be changed; part of the point of quasi-category theory (and of the model categorical approach to higher category theory in general) is that you can use "strict" or "evil" constructions, carefully, to more easily talk about the "real" underlying "non-strict" notions.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownBy the way, all existing definitions of higher category are also "set-theoretic" in this sense. In fact, so are almost all definitions of "category"! To get beyond that we need a "(higher-)categorical" foundation for mathematics.

   By the way, all existing definitions of higher category are also "set-theoretic" in this sense. In fact, so are almost all definitions of "category"! To get beyond that we need a "(higher-)categorical" foundation for mathematics.

8. • CommentRowNumber8.
   • CommentAuthordomenico_fiorenza
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: domenico_fiorenza
   Format: HtmlI know, but it is precisely this "set-theoretic" aspect that at times makes me uneasy with the subject. I mean, in my experience, I've never known exactly what a set is (in any foundational sense). I just worked with the naive idea which sounds like "a set is some collection of things; but never never never say the set of all sets". Much in the same way I always worked with a naive category theory, with the basic rule "never ask how many are the objects, and never say two of them are equal, if not tautologically". so, for instance, I feel confident in saying thinks like "the category of vector spaces", or "a finite dimensional vector space is naturally isomorphic to its bidual", while I really feel uneasy if I have to wonder whether <latex>V_1\otimes(V_2\otimes V_2)</latex> is equal to <latex>(V_1\otimes V_2)\otimes V_3</latex> or not. to me is not that the answer is not, but rather that the question is meaningless. so I have no problems in working with a set-theory based higher category theory, but I will feel of it as a simplicial homotopy theory with another name (there's a post by Urs on this, if I'm not wrong), and will have some psychological difficulties in looking at vector spaces as to an infinity-category, while I'm currently used to, in the extremely naive way sketched above. the fact to be considered, I think, is that with all the naiveness of my feeling on category theory, I'm "the categorist" at my department (this recollects to the "nLab in the eyes of others" thread: how is the feeling about category theory outside the category theory community?). and I feel that a non-naive (higher) category theory would fail in its spreading through maths. that's why I insist so much in sayng that definitios should be at least non evidently evil. I can believe that going deep enough in unwrapping the definitons some evilness will come out anyway, since total unwrapping always calls in the foundations, but I'll always be a big sustainer of the naive approach to higher category theory ("never say two functors are equal :)" )

   I know, but it is precisely this "set-theoretic" aspect that at times makes me uneasy with the subject. I mean, in my experience, I've never known exactly what a set is (in any foundational sense). I just worked with the naive idea which sounds like "a set is some collection of things; but never never never say the set of all sets". Much in the same way I always worked with a naive category theory, with the basic rule "never ask how many are the objects, and never say two of them are equal, if not tautologically". so, for instance, I feel confident in saying thinks like "the category of vector spaces", or "a finite dimensional vector space is naturally isomorphic to its bidual", while I really feel uneasy if I have to wonder whether is equal to or not. to me is not that the answer is not, but rather that the question is meaningless.
   
   so I have no problems in working with a set-theory based higher category theory, but I will feel of it as a simplicial homotopy theory with another name (there's a post by Urs on this, if I'm not wrong), and will have some psychological difficulties in looking at vector spaces as to an infinity-category, while I'm currently used to, in the extremely naive way sketched above.
   
   the fact to be considered, I think, is that with all the naiveness of my feeling on category theory, I'm "the categorist" at my department (this recollects to the "nLab in the eyes of others" thread: how is the feeling about category theory outside the category theory community?). and I feel that a non-naive (higher) category theory would fail in its spreading through maths. that's why I insist so much in sayng that definitios should be at least non evidently evil. I can believe that going deep enough in unwrapping the definitons some evilness will come out anyway, since total unwrapping always calls in the foundations, but I'll always be a big sustainer of the naive approach to higher category theory ("never say two functors are equal :)" )
9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 4th 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownI'm more optimistic about the prospects for HCT spreading through math than that. I would eventually, like for there to be a higher-categorical foundation of mathematics, but today we barely even have a 1-categorical foundation for mathematics! We can't wait until we have the perfect world before doing anything.

   I'm more optimistic about the prospects for HCT spreading through math than that. I would eventually, like for there to be a higher-categorical foundation of mathematics, but today we barely even have a 1-categorical foundation for mathematics! We can't wait until we have the perfect world before doing anything.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeJan 5th 2010
    • PermaLink
    Author: TobyBartels
    Format: Markdown@ Mike #7 >By the way, all existing definitions of higher category are also "set-theoretic" in this sense. Isn't Makkai supposed to have defined ‘multitopic’ ?-categories in FOLDS? I never really looked at his stuff on higher categories (although I should!), so maybe not.

    @ Mike #7

    By the way, all existing definitions of higher category are also "set-theoretic" in this sense.

    Isn't Makkai supposed to have defined ‘multitopic’ ?-categories in FOLDS? I never really looked at his stuff on higher categories (although I should!), so maybe not.

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJan 5th 2010
    • PermaLink
    Author: TobyBartels
    Format: Markdown@ Domenico # 8 >to me is not that the answer is not, but rather that the question is meaningless. I agree, that is the attitude to take. One can look at an implementation of categories within set theory (what I call a [[strict category]]) and ask that question, but not when dealing with categories *in themselves*. If our formal language of mathematics allows us to ask the question anyway, then that is the language's fault.

    @ Domenico # 8

    to me is not that the answer is not, but rather that the question is meaningless.

    I agree, that is the attitude to take. One can look at an implementation of categories within set theory (what I call a strict category) and ask that question, but not when dealing with categories in themselves. If our formal language of mathematics allows us to ask the question anyway, then that is the language's fault.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJan 5th 2010
    • PermaLink
    Author: Mike Shulman
    Format: Markdown> Isn't Makkai supposed to have defined 'multitopic' ?-categories in FOLDS? That may be right. Although it's not clear to me whether there's a good definition of the "category of multitopes/opetopes" (which would specify the dependent-sorts in that FOLDS theory) that doesn't require some set theory.

    Isn't Makkai supposed to have defined 'multitopic' ?-categories in FOLDS?

    That may be right. Although it's not clear to me whether there's a good definition of the "category of multitopes/opetopes" (which would specify the dependent-sorts in that FOLDS theory) that doesn't require some set theory.

13. • CommentRowNumber13.
    • CommentAuthorHarry Gindi
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Harry Gindi
    Format: TextI agree that "evil" is a bad thing in terms of category theory, but I doubt very much that category theory will ever give us a satisfying and intuitive theory of logic like set theory has. People are always ready to throw away sets, but sets are great, and I feel like you're jumping the gun on this whole "redifining logic" thing.

    I agree that "evil" is a bad thing in terms of category theory, but I doubt very much that category theory will ever give us a satisfying and intuitive theory of logic like set theory has. People are always ready to throw away sets, but sets are great, and I feel like you're jumping the gun on this whole "redifining logic" thing.
14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownOn the contrary, category theory has cast considerable light on the structure of logic (e.g., universal and existential quantification are right and left adjoint to substitution or pulling-back operations, Beck-Chevalley conditions, and much more) in a way that "set theory" per se has not, and has considerably expanded the scope of what we even mean by "logic" (cf. enriched category theory as "generalized logic", a la Lawvere's metric space paper). When you say that set theory gives a satisfying and intuitive view of logic, more so than category theory, I assume you are referring to (Tarskian) semantics of first-order languages (interpreting relations as subsets, etc.). I agree that that is perhaps (or arguably) the best pedagogical starting point, but the expansion of semantics to include topos semantics and semantics in even more general structures (e.g., pretoposes, exact and regular categories, or even just categories with products, depending on the logical strength of the language being interpreted) has opened the playing field in a huge way and is of tremendous importance. And not for categorists alone -- for example, oftentimes in interpreting concepts in algebraic geometry, one needs to break free of set-theoretic ways of thinking. So far only category theory has provided an adequate language and methodology for doing so. I don't know of anyone who is ready to "throw away sets", or perhaps I'm not sure what you mean by that. The primitive undefined notion of collection is obviously here to stay. But certainly what is meant by a _set theory_ has been considerably expanded and sharpened over the decades by topos theorists and others who work in categorical logic, and I think this is closer to the heart of the discussion: reformulate set theory structurally, in a way which avoids various problems of evil. Cf. the long thread at the Café on material vs.structural set theories, the discussion of SEAR, etc.

    On the contrary, category theory has cast considerable light on the structure of logic (e.g., universal and existential quantification are right and left adjoint to substitution or pulling-back operations, Beck-Chevalley conditions, and much more) in a way that "set theory" per se has not, and has considerably expanded the scope of what we even mean by "logic" (cf. enriched category theory as "generalized logic", a la Lawvere's metric space paper).

    When you say that set theory gives a satisfying and intuitive view of logic, more so than category theory, I assume you are referring to (Tarskian) semantics of first-order languages (interpreting relations as subsets, etc.). I agree that that is perhaps (or arguably) the best pedagogical starting point, but the expansion of semantics to include topos semantics and semantics in even more general structures (e.g., pretoposes, exact and regular categories, or even just categories with products, depending on the logical strength of the language being interpreted) has opened the playing field in a huge way and is of tremendous importance. And not for categorists alone -- for example, oftentimes in interpreting concepts in algebraic geometry, one needs to break free of set-theoretic ways of thinking. So far only category theory has provided an adequate language and methodology for doing so.

    I don't know of anyone who is ready to "throw away sets", or perhaps I'm not sure what you mean by that. The primitive undefined notion of collection is obviously here to stay. But certainly what is meant by a set theory has been considerably expanded and sharpened over the decades by topos theorists and others who work in categorical logic, and I think this is closer to the heart of the discussion: reformulate set theory structurally, in a way which avoids various problems of evil. Cf. the long thread at the Café on material vs.structural set theories, the discussion of SEAR, etc.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Urs
    Format: MarkdownMaybe parts of what you just said, Todd, or something similar, could usefully be copied into the section "In logic" at [[nPOV]]?

    Maybe parts of what you just said, Todd, or something similar, could usefully be copied into the section "In logic" at nPOV?

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownAn interesting distinction to make is between "throwing away sets" and "throwing away collections." From a certain version of the n-POV, the distinction between a *set* and a *collection* is that a set comes with a notion of *equality*. Intensional type theory and its relationship to higher category theory suggests to me that perhaps while we still need a "primitive undefined notion of collection," the *equality* relations that make such collections into "sets" may be regarded as defined rather than primitive. (Of course this is a long-standing view in constructive mathematics independent of category theory. That category theory comes to it from a completely different standpoint is, I think, additional evidence for its meaningfulness.)

    An interesting distinction to make is between "throwing away sets" and "throwing away collections." From a certain version of the n-POV, the distinction between a set and a collection is that a set comes with a notion of equality. Intensional type theory and its relationship to higher category theory suggests to me that perhaps while we still need a "primitive undefined notion of collection," the equality relations that make such collections into "sets" may be regarded as defined rather than primitive. (Of course this is a long-standing view in constructive mathematics independent of category theory. That category theory comes to it from a completely different standpoint is, I think, additional evidence for its meaningfulness.)

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownAlso, it just occurred to me that the notion of quasicategory can almost certainly be formulated in FOLDS as well. In fact, probably pretty much any completely non-algebraic notion of higher category could be so formulated.

    Also, it just occurred to me that the notion of quasicategory can almost certainly be formulated in FOLDS as well. In fact, probably pretty much any completely non-algebraic notion of higher category could be so formulated.

18. • CommentRowNumber18.
    • CommentAuthorzskoda
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: zskoda
    Format: MarkdownHow about a complementary notion of COEVIL ? I mean when one has some notion in (higher) categorical world non-evil definition will make it maximally flexible-invariant under the appropriate level of equivalences. This is optimal. But if one wants to compare two different kinds of objects, then one wants to organize them in the highest categorical structure possible. Thus unlike the non-evil definitions in which one wants to have invariance under the WEAKEST possible equivalence, the optimal comparison of different notions is the equivalence of the RICHEST (strongest) possible structures. For example, some descent problems lead to the (n,k)-categories of descent data which are not mere (n,1)-categories. Neglecting this refinement is coevil and it happens if one treats the descent problem using non-functorial resolutions; some canonical functorial resolutions enable one to see the full (n,k)-categories.

    How about a complementary notion of COEVIL ? I mean when one has some notion in (higher) categorical world non-evil definition will make it maximally flexible-invariant under the appropriate level of equivalences. This is optimal. But if one wants to compare two different kinds of objects, then one wants to organize them in the highest categorical structure possible. Thus unlike the non-evil definitions in which one wants to have invariance under the WEAKEST possible equivalence, the optimal comparison of different notions is the equivalence of the RICHEST (strongest) possible structures. For example, some descent problems lead to the (n,k)-categories of descent data which are not mere (n,1)-categories. Neglecting this refinement is coevil and it happens if one treats the descent problem using non-functorial resolutions; some canonical functorial resolutions enable one to see the full (n,k)-categories.

19. • CommentRowNumber19.
    • CommentAuthorHarry Gindi
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Harry Gindi
    Format: TextI feel like there are a number of places where a notion of formal equality is useful. If we have no notion of equality, then we can only classify objects in an ordinary category up to isomorphism, which means that when we make statements about the category, it's not really any different than talking about the skeleton, because if A and B are isomorphic, they are now entirely indistinguishable. That is, unless I'm missing a huge point here.

    I feel like there are a number of places where a notion of formal equality is useful. If we have no notion of equality, then we can only classify objects in an ordinary category up to isomorphism, which means that when we make statements about the category, it's not really any different than talking about the skeleton, because if A and B are isomorphic, they are now entirely indistinguishable. That is, unless I'm missing a huge point here.
20. • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Mike Shulman
    Format: Markdown@Harry, that's true. As long as every category has a skeleton (which is, itself, an evil thing to even say), anything non-evil you can say about a category will also be true about its skeleton. So what?

    @Harry, that's true. As long as every category has a skeleton (which is, itself, an evil thing to even say), anything non-evil you can say about a category will also be true about its skeleton. So what?

21. • CommentRowNumber21.
    • CommentAuthorHarry Gindi
    • CommentTimeJan 6th 2010
    • (edited Jan 6th 2010)
    • PermaLink
    Author: Harry Gindi
    Format: TextSo does evil mean that it uses the axiom of choice, or does it mean that it uses primitive equality? I'm willing to give up primitive equality if there's a good argument for it, but I'll never give up the axiom of choice. That's something I like my foundations to have.

    So does evil mean that it uses the axiom of choice, or does it mean that it uses primitive equality? I'm willing to give up primitive equality if there's a good argument for it, but I'll never give up the axiom of choice. That's something I like my foundations to have.
22. • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownWell, there are multiple things that "evil" might mean. "Using equality of objects" is the informal definition. I've never heard anyone suggest that it had anything to do with AC.

    Well, there are multiple things that "evil" might mean. "Using equality of objects" is the informal definition. I've never heard anyone suggest that it had anything to do with AC.

23. • CommentRowNumber23.
    • CommentAuthorHarry Gindi
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: Harry Gindi
    Format: TextWell, the skeleton exists by the axiom of choice, no?

    Well, the skeleton exists by the axiom of choice, no?
24. • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeJan 6th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownEvil means, more or less, using a primitive notion of equality between objects of a given aribtrary category. Evil does *not* mean using the axiom of choice. Both concepts have something to do with formalising the notion of equality, and I do think of them as related, although I'm not sure that I can say anything precise about that. In any case, you can avoid evil while still accepting the full strength of the axiom of choice.

    Evil means, more or less, using a primitive notion of equality between objects of a given aribtrary category. Evil does not mean using the axiom of choice. Both concepts have something to do with formalising the notion of equality, and I do think of them as related, although I'm not sure that I can say anything precise about that. In any case, you can avoid evil while still accepting the full strength of the axiom of choice.

25. • CommentRowNumber25.
    • CommentAuthorHarry Gindi
    • CommentTimeJan 7th 2010
    • PermaLink
    Author: Harry Gindi
    Format: TextHow is taking the skeleton evil, then?

    How is taking the skeleton evil, then?
26. • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownA skeleton is evil because the notion of when a category is skeletal is evil: a category is skeletal if any two isomorphic objects are equal. This involves equality of objects. In a theory that doesn't admit equality of objects, you cannot ask whether a category is skeletal or not, hence you cannot construct a skeleton.

    A skeleton is evil because the notion of when a category is skeletal is evil: a category is skeletal if any two isomorphic objects are equal. This involves equality of objects. In a theory that doesn't admit equality of objects, you cannot ask whether a category is skeletal or not, hence you cannot construct a skeleton.

27. • CommentRowNumber27.
    • CommentAuthorHarry Gindi
    • CommentTimeJan 7th 2010
    • (edited Jan 7th 2010)
    • PermaLink
    Author: Harry Gindi
    Format: TextConsider the following proposed axiom for a skeleton, "f in Arr(C) has an inverse => f is composable with itself". This is an interesting statement and brings us to somewhat of a crossroads. The definition of composability we were discussing on the page is: f is left composable with g if and only if Dom(g)=Cod(f). From this, it's clear that either we allow composability to be defined along arbitrary isomorphisms like Toby suggested, or as you said in the discussion, "Mike Shulman: I’m not convinced by “composing along isomorphisms,” because what does it mean for an isomorphism h to be “between” domg and codf? It means that domh=codf and codh=domg." To be honest, I didn't understand some of the points afterwards regarding type theory. However, we're forced now to make a decision: Either we lose the ability to define composability explicitly, or skeletons are not evil. So that definition of composability must be evil because it implies that we can define skeletons un-evilly.

    Consider the following proposed axiom for a skeleton, "f in Arr(C) has an inverse => f is composable with itself". This is an interesting statement and brings us to somewhat of a crossroads. The definition of composability we were discussing on the page is: f is left composable with g if and only if Dom(g)=Cod(f). From this, it's clear that either we allow composability to be defined along arbitrary isomorphisms like Toby suggested, or as you said in the discussion,
    
    "Mike Shulman: I’m not convinced by “composing along isomorphisms,” because what does it mean for an isomorphism h to be “between” domg and codf? It means that domh=codf and codh=domg."
    
    To be honest, I didn't understand some of the points afterwards regarding type theory. However, we're forced now to make a decision: Either we lose the ability to define composability explicitly, or skeletons are not evil.
    
    So that definition of composability must be evil because it implies that we can define skeletons un-evilly.
28. • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownMy response has to do with the type theory that you didn't understand. (-: In a non-evil framework like FOLDS, composability is a typing assertion rather than a proposition. The domain and codomain of a morphism have to be given before the morphism is talked about. You can't talk about merely "a morphism of the category C," only "a morphism from x to y in the category C" where x and y are previously known to be objects of C. Thus, it makes no sense to say "prove that f and g are composable" or assume an axiom like the one you propose. I guess you could say this is "losing the ability to define composability" but the point is that composability is not properly regarded as a "property" of an "arbitrary" pair of arrows. Rather, two arrows with compatible source/target are composable by virtue of their types, while two arrows with incompatible source/target are not composable by virtue of their types. Consider, by analogy, the group of integers mod 7, with addition, and the group of continuous real-valued functions on the Cantor set, with addition. Is a residue class mod 7 "addable" to a real-valued function on the Cantor set? No, but that's not something that I would think of *proving* or *assuming*---it's just so because of typing. Addition is only defined for things that are elements of the same group. Likewise, composition is only defined for morphisms that have compatible source/target.

    My response has to do with the type theory that you didn't understand. (-: In a non-evil framework like FOLDS, composability is a typing assertion rather than a proposition. The domain and codomain of a morphism have to be given before the morphism is talked about. You can't talk about merely "a morphism of the category C," only "a morphism from x to y in the category C" where x and y are previously known to be objects of C. Thus, it makes no sense to say "prove that f and g are composable" or assume an axiom like the one you propose.

    I guess you could say this is "losing the ability to define composability" but the point is that composability is not properly regarded as a "property" of an "arbitrary" pair of arrows. Rather, two arrows with compatible source/target are composable by virtue of their types, while two arrows with incompatible source/target are not composable by virtue of their types. Consider, by analogy, the group of integers mod 7, with addition, and the group of continuous real-valued functions on the Cantor set, with addition. Is a residue class mod 7 "addable" to a real-valued function on the Cantor set? No, but that's not something that I would think of proving or assuming---it's just so because of typing. Addition is only defined for things that are elements of the same group. Likewise, composition is only defined for morphisms that have compatible source/target.

29. • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexI hereby move the following discussion from [[evil]] to here *** Comment: It seems that at some level you can't avoid equality, at least if you want to completely formalise things (say, in a proof assistant). For example, in the definition of "category" itself (on which the definitions of isomorphism and $\infty$-groupoid seem to depend), we say that $g \circ f$ is defined iff $\dom g = \cod f$. Now if you start your theorem with "let $a,b,c$ be objects of $C$ and let $g : b \to c$,$f: a \to b$ be morphisms", then there's no problem. But what if you need to compose morphisms whose dom/cod aren't definitionally/syntactically equal? I suppose that at this point it depends on which foundations you use. Reply: Yes, it can depend on the foundations. [[FOLDS]] is a foundation specifically designed to avoid evil, and higher category theory has been formulated in it (by [[Michael Makkai]], who invented both FOLDS and a multitopic definition of higher categories to go with it). More generally, the style of terminology that you gave comes naturally to a development of (higher) category theory in a foundation based on dependent [[type theory]]. Even in your first example, the quesion of whether we can compose $g \circ f$, we can avoid evil if we try. Naïvely, we can compose them if and only if $\dom g = \cod f$; composability is a property of the pair ---but an evil property. Less evilly, we make composability a *structure* on the pair; we can compose them along any isomorphism between $\dom g$ and $\cod f$. So as usual in category theory, we don\'t ask whether these objects are equal but instead how they might be isomorphic. Of course, if $f$ and $g$ are given as $g: b \to c$ and $f: a \to b$, then we can compose them along the identity morphism of $b$; this is the usual notion of compoisition in that case. It is only when $f$ and $g$ are not given to us in such a way that we have to talk about composing along an arbitrary (possibly nonexistent, certainly not likely to exist uniquely) isomorphism. Can you say everything that you want to say about (higher) categories while avoiding evil throughout? That will always be an open question, as people think of new things to say about them. But I think that it is a fruiful attitude to take that one should try. ---[[Toby Bartels]] [[Mike Shulman]]: I'm not convinced by "composing along isomorphisms," because what does it mean for an isomorphism $h$ to be "between" $\dom g$ and $\cod f$? It means that $\dom h = \cod f$ and $\cod h = \dom g$. _Toby_: But <del>you</del><ins>the Anonymous Coward</ins> already told us how to phrase things above: "let $a,b,c$ be objects of $C$ and let $g : b \to c$,$f: a \to b$ be morphisms". So now we take a case where $dom g$ and $cod f$ are not definitionally/syntactically equal, as so: > Let $a,b,c,d$ be objects and let $g: c \to d,\; f: a \to b$ be morphisms. Then we can form the composite $g \circ f$ relative to any isomophism $h: b \to c$. (Of course, the notation $g \circ f$ suppresses $h$, so it\'s more proper to write $g \circ_h f$, or just $g \circ h \circ f$ as a normal person would.) Note that the definability of $g \circ f$ is now the set $Iso(b,c)$ rather than the truth value $b = c$. In an $\infty$-category, it would be an $\infty$-groupoid $Iso(b,c)$. [[Mike Shulman]]: That wasn't me above, I don't think. I would consider "let $g : b \to c$ and $f: a \to b$ be morphisms" as implicitly using dependent types if you're considering it to avoid evil. It seems to me that in a non-dependently typed theory, the only thing "let $g : b \to c$ and $f: a \to b$ be morphisms" can mean is "let $g$ and $f$ be morphisms such that $\dom f = a$, $\cod f = b$, $\dom g = b$, and $\cod g=c$," which does involve talking about equality of objects. _Toby_: Right on both counts: that was an [[Anonymous Coward]] in the first comment, and the phrasing that the Coward suggested does implicitly use dependent types (as I alluded to in my original reply). Makkai says 'dependent sorts' (the 'DS' in 'FOLDS') instead for some reason. Can we avoid evil in an independently typed (possibly even untyped) language? I think that this should be possible; we would need rules about when you can and can\'t state equalities; maybe, you can state $\forall f, dom f = x \Rightarrow ...$ and the obvious variations, but no others? [[Mike Shulman]]: In other words, you can secretly make your independent types act like dependent ones? (-: _Toby_: Yeah, a dependent type theory can always be rephrased as an independent type theory, although you have to use equality to do this; this is equivalent to the original dependent type theory if (as is the common practice) that theory also had equality predicates, but otherwise it\'s stonger. Similarly, a typed theory can be rephrased as an untyped theory, although you have to use typing predicates to do this, and again this is stronger. Conversely, we know (well, some people know) how to limit the use of the typing predicates in the untyped theory to make it equivalent to the typed theory. Now I think that there also ought to be rules to limit the use of equality in a simple type theory to make it equivalent to a dependent type theory *without* equality. [[Mike Shulman]]: Amazingly enough, as you said at latest changes, this conversation does seem to be leading in the direction of actual mathematics. It does seem like that should be possible, but I don't have the time to think about it any more deeply now. Aside from pointing out the obvious fact that until we get to $\omega$-categories, we do want to allow equality relations on *some* of the types in the dependent type theory. *** to be continued in the next message

    I hereby move the following discussion from evil to here

    ---

    Comment: It seems that at some level you can’t avoid equality, at least if you want to completely formalise things (say, in a proof assistant). For example, in the definition of “category” itself (on which the definitions of isomorphism and $\infty$-groupoid seem to depend), we say that $g \circ f$ is defined iff $\dom g = \cod f$.

    Now if you start your theorem with “let $a,b,c$ be objects of $C$ and let $g : b \to c$,$f: a \to b$ be morphisms”, then there’s no problem. But what if you need to compose morphisms whose dom/cod aren’t definitionally/syntactically equal? I suppose that at this point it depends on which foundations you use.

    Reply: Yes, it can depend on the foundations. FOLDS is a foundation specifically designed to avoid evil, and higher category theory has been formulated in it (by Michael Makkai, who invented both FOLDS and a multitopic definition of higher categories to go with it). More generally, the style of terminology that you gave comes naturally to a development of (higher) category theory in a foundation based on dependent type theory.

    Even in your first example, the quesion of whether we can compose $g \circ f$, we can avoid evil if we try. Naïvely, we can compose them if and only if $\dom g = \cod f$; composability is a property of the pair —but an evil property. Less evilly, we make composability a structure on the pair; we can compose them along any isomorphism between $\dom g$ and $\cod f$. So as usual in category theory, we don't ask whether these objects are equal but instead how they might be isomorphic.

    Of course, if $f$ and $g$ are given as $g: b \to c$ and $f: a \to b$, then we can compose them along the identity morphism of $b$; this is the usual notion of compoisition in that case. It is only when $f$ and $g$ are not given to us in such a way that we have to talk about composing along an arbitrary (possibly nonexistent, certainly not likely to exist uniquely) isomorphism.

    Can you say everything that you want to say about (higher) categories while avoiding evil throughout? That will always be an open question, as people think of new things to say about them. But I think that it is a fruiful attitude to take that one should try. —Toby Bartels

    Mike Shulman: I’m not convinced by “composing along isomorphisms,” because what does it mean for an isomorphism $h$ to be “between” $\dom g$ and $\cod f$? It means that $\dom h = \cod f$ and $\cod h = \dom g$.

    Toby: But youthe Anonymous Coward already told us how to phrase things above: “let $a,b,c$ be objects of $C$ and let $g : b \to c$,$f: a \to b$ be morphisms”. So now we take a case where $dom g$ and $cod f$ are not definitionally/syntactically equal, as so:

    Let $a,b,c,d$ be objects and let $g: c \to d,\; f: a \to b$ be morphisms. Then we can form the composite $g \circ f$ relative to any isomophism $h: b \to c$. (Of course, the notation $g \circ f$ suppresses $h$, so it's more proper to write $g \circ_h f$, or just $g \circ h \circ f$ as a normal person would.)

    Note that the definability of $g \circ f$ is now the set $Iso(b,c)$ rather than the truth value $b = c$. In an $\infty$-category, it would be an $\infty$-groupoid $Iso(b,c)$.

    Mike Shulman: That wasn’t me above, I don’t think. I would consider “let $g : b \to c$ and $f: a \to b$ be morphisms” as implicitly using dependent types if you’re considering it to avoid evil. It seems to me that in a non-dependently typed theory, the only thing “let $g : b \to c$ and $f: a \to b$ be morphisms” can mean is “let $g$ and $f$ be morphisms such that $\dom f = a$, $\cod f = b$, $\dom g = b$, and $\cod g=c$,” which does involve talking about equality of objects.

    Toby: Right on both counts: that was an Anonymous Coward in the first comment, and the phrasing that the Coward suggested does implicitly use dependent types (as I alluded to in my original reply). Makkai says ’dependent sorts’ (the ’DS’ in ’FOLDS’) instead for some reason. Can we avoid evil in an independently typed (possibly even untyped) language? I think that this should be possible; we would need rules about when you can and can't state equalities; maybe, you can state $\forall f, dom f = x \Rightarrow ...$ and the obvious variations, but no others?

    Mike Shulman: In other words, you can secretly make your independent types act like dependent ones? (-:

    Toby: Yeah, a dependent type theory can always be rephrased as an independent type theory, although you have to use equality to do this; this is equivalent to the original dependent type theory if (as is the common practice) that theory also had equality predicates, but otherwise it's stonger. Similarly, a typed theory can be rephrased as an untyped theory, although you have to use typing predicates to do this, and again this is stronger. Conversely, we know (well, some people know) how to limit the use of the typing predicates in the untyped theory to make it equivalent to the typed theory. Now I think that there also ought to be rules to limit the use of equality in a simple type theory to make it equivalent to a dependent type theory without equality.

    Mike Shulman: Amazingly enough, as you said at latest changes, this conversation does seem to be leading in the direction of actual mathematics. It does seem like that should be possible, but I don’t have the time to think about it any more deeply now. Aside from pointing out the obvious fact that until we get to $\omega$-categories, we do want to allow equality relations on some of the types in the dependent type theory.

    ---

    to be continued in the next message

30. • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexcontinuation of forwarded discussion from the previous message *** _Toby_: I also don\'t have the time to think about it carefully; I feel pretty secure about my intuition, but that is all. But I would see the equality relation between parallel $n$-morphisms in an $n$-category as something extralogical, just as much as the type of $n$-morphisms between parallel $(n-1)$-morphisms. _Harry_: Couldn't we just say: Let $f$ and $g$ be (left? right?)-composable iff $h[dom g]$ is isomorphic to $h[cod f]$ where $h$ is the homotopy category functor (assuming quasicategories, but there should be a good enough way to define this in more generality, no?). This way, $g \circ f$ is only specified up to homotopy (that is, we know that it's in the homotopy class of $h[g] \circ h[f]$. I think there might be a few technicalities to work out with 1-Categories, but applying the homotopy functor immediately collapses it to that case. _Toby_: That seems to bring us back to the idea of composing along an isomorphism between $dom g$ and $cod f$, now generalised to quasicategories. [[Mike Shulman]]: Yes, if you only know that $h[dom g]$ is isomorphic to $h[cod f]$, you still need to *choose* an isomorphism along which to compose $f$ and $g$. Different choices will give you different "composites". _Harry_: Can two wrongs (or evils in this case) make a right? Maybe we can solve the composition problem by passing to the skeleton of the homotopy category? [[Mike Shulman]]: I think the short answer is "no." Choosing a skeleton (together with an equivalence to the category one started with, naturally) involves choosing a bunch of specified isomorphisms between isomorphic objects, so really you aren't doing anything different. [[JCMcKeown]]: Non-sequitur; perhaps it's helpful to try remembering why evil concepts propagate? E.g., "the standard" basis of $\mathbf{k}^n$ doesn't exist as intrinsic to any vector space $\mathbf{k}^n$, but it's implicit in any biproduct diagram for $\mathbf{k}^n$ over $n$ copies of $\mathbf{k}$. That is, sometimes we want to pretend that some anafunctor is actually a functor --- or that a contractible object is literally terminal --- and once we're comfortable dropping this crutch, we try to relax things and see what's still sensible. But surely it's not evil to say that $\id_C(A)=A$? It's not really a statement about *two things*, anyways. Checking the evilness of this would only lead you to ask "¿$\id_C(A)=B$?" for $A,B$ *equivalent* if you *don't know* that we're looking at a diagonal, where we only ask $\id_C(A)=B$ for $A=B$. --JCM _Toby_: In some languages (I am thinking of Coquand-style type theory without identity predicates, but it probably appears elsewhere), it is sometimes necessary to form identity *judgements*. For example, we may need to be able to know that $\pi(a,b)$ and $a$ are the exact same thing (and other identities given by $\beta$-[[beta-rule|rules]]). However, we still don\'t want any identity *propositions*. So given a category $C$ and an object $A$ of $C$, it may well be possible to state, as a judgement of a true fact that we can prove, that $\id_C(A)$ and $A$ are identical; certainly it would be if part of the definition of $\id_C$ is that it acts on objects as $\lambda X. X$ (and we have $\beta$-rule judgements as I suggested above). However, it should never be necessary to treat the statement that they are identical as a proposition, and indeed we would never want (given additionally an object $B$ of $C$) to treat the statement that $\id_C(A)$ and $B$ are identical as a propostion. But in other languages, such as FOLDS, even this sort of thing would never come up. In that language, $\id_C(A)$ is not a term for an object of $C$ at all. The best that you can do is invoke the existential property of the identity anafunctor to know that there is an object $X$ of $A$ such that $X$ is *a* value of $\id_C$ at $A$, then declare that you will denote $X$ by $\id_C(A)$ from now on. (One should be able to formalise this abuse of language so as to make ordinary mathematical vernacular sensible, but I\'m not sure how to do it.) *** end of forwarded discussion

    continuation of forwarded discussion from the previous message

    ---

    Toby: I also don't have the time to think about it carefully; I feel pretty secure about my intuition, but that is all. But I would see the equality relation between parallel $n$-morphisms in an $n$-category as something extralogical, just as much as the type of $n$-morphisms between parallel $(n-1)$-morphisms.

    Harry: Couldn’t we just say: Let $f$ and $g$ be (left? right?)-composable iff $h[dom g]$ is isomorphic to $h[cod f]$ where $h$ is the homotopy category functor (assuming quasicategories, but there should be a good enough way to define this in more generality, no?). This way, $g \circ f$ is only specified up to homotopy (that is, we know that it’s in the homotopy class of $h[g] \circ h[f]$. I think there might be a few technicalities to work out with 1-Categories, but applying the homotopy functor immediately collapses it to that case.

    Toby: That seems to bring us back to the idea of composing along an isomorphism between $dom g$ and $cod f$, now generalised to quasicategories.

    Mike Shulman: Yes, if you only know that $h[dom g]$ is isomorphic to $h[cod f]$, you still need to choose an isomorphism along which to compose $f$ and $g$. Different choices will give you different “composites”.

    Harry: Can two wrongs (or evils in this case) make a right? Maybe we can solve the composition problem by passing to the skeleton of the homotopy category?

    Mike Shulman: I think the short answer is “no.” Choosing a skeleton (together with an equivalence to the category one started with, naturally) involves choosing a bunch of specified isomorphisms between isomorphic objects, so really you aren’t doing anything different.

    JCMcKeown: Non-sequitur; perhaps it’s helpful to try remembering why evil concepts propagate? E.g., “the standard” basis of $\mathbf{k}^n$ doesn’t exist as intrinsic to any vector space $\mathbf{k}^n$, but it’s implicit in any biproduct diagram for $\mathbf{k}^n$ over $n$ copies of $\mathbf{k}$. That is, sometimes we want to pretend that some anafunctor is actually a functor — or that a contractible object is literally terminal — and once we’re comfortable dropping this crutch, we try to relax things and see what’s still sensible. But surely it’s not evil to say that $\id_C(A)=A$? It’s not really a statement about two things, anyways. Checking the evilness of this would only lead you to ask “¿$\id_C(A)=B$?” for $A,B$ equivalent if you don’t know that we’re looking at a diagonal, where we only ask $\id_C(A)=B$ for $A=B$. –JCM

    Toby: In some languages (I am thinking of Coquand-style type theory without identity predicates, but it probably appears elsewhere), it is sometimes necessary to form identity judgements. For example, we may need to be able to know that $\pi(a,b)$ and $a$ are the exact same thing (and other identities given by $\beta$-rules). However, we still don't want any identity propositions. So given a category $C$ and an object $A$ of $C$, it may well be possible to state, as a judgement of a true fact that we can prove, that $\id_C(A)$ and $A$ are identical; certainly it would be if part of the definition of $\id_C$ is that it acts on objects as $\lambda X. X$ (and we have $\beta$-rule judgements as I suggested above). However, it should never be necessary to treat the statement that they are identical as a proposition, and indeed we would never want (given additionally an object $B$ of $C$) to treat the statement that $\id_C(A)$ and $B$ are identical as a propostion.

    But in other languages, such as FOLDS, even this sort of thing would never come up. In that language, $\id_C(A)$ is not a term for an object of $C$ at all. The best that you can do is invoke the existential property of the identity anafunctor to know that there is an object $X$ of $A$ such that $X$ is a value of $\id_C$ at $A$, then declare that you will denote $X$ by $\id_C(A)$ from now on. (One should be able to formalise this abuse of language so as to make ordinary mathematical vernacular sensible, but I'm not sure how to do it.)

    ---

    end of forwarded discussion

31. • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded to [[evil]] a [References](http://ncatlab.org/nlab/show/evil#References) section with a pointer to a talk by Voevodsky

    added to evil a References section with a pointer to a talk by Voevodsky

32. • CommentRowNumber32.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 12th 2011
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Urs - the link to the video seems (for me) to link back to [[evil]]

    @Urs - the link to the video seems (for me) to link back to evil

33. • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexSorry, some copy-and-pasting went wrong. I have fixed it now. The link is [here](http://video.ias.edu/node/68).

    Sorry, some copy-and-pasting went wrong. I have fixed it now.

    The link is here.