Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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!
Oh goody! When I read his post this morning I was sorely tempted to send a reply saying "Put this on the nLab!".
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.
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.
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.
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.
@ 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.
@ 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.
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.
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.
Maybe parts of what you just said, Todd, or something similar, could usefully be copied into the section "In logic" at nPOV?
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.)
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.
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.
@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?
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.
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.
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.
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.
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
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
added to evil a References section with a pointer to a talk by Voevodsky
@Urs - the link to the video seems (for me) to link back to evil
Sorry, some copy-and-pasting went wrong. I have fixed it now.
The link is here.
1 to 33 of 33