On the occasion of the discussion about "evil" I want to point out an example where speaking about equality of objects seems to be indispensible. If P : XX -> BB is a functor and one wants to say that it is a fibration then one is inclined to formulate this as follows if u : J -> I is a map in BB and PX = I then there exists a morphism \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ... I don't see how to avoid reference to equality of objects in this formulation. This already happens if XX and BB are groupoids where P : XX -> BB is a fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X with P\phi = u. Ironically the category of groupoids and fibrations of groupoids as families of types was the first example of a model of type theory where equality may be interpreted as being isomorphic. So my conclusion is that equality of objects is sometimes absolutely necessary. Avoiding reference to equality is also not a question of using dependent types as some people implicitly seem to say. Even in intensional type theory there is a notion of equality. But it is sometimes inconvenient to use. As pointed out by Ahrens one can and should use extensional type theory whenever convenient. Intensional type theory allows one to interpret equality as being isomorphic, a kind of reward for the inconvenience of using intensional identity types. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
The usual notion of (Grothendieck) fibration is indeed non-kosher, but there is a variant due to Ross Street which is not. This variant is reproduced at http://ncatlab.org/nlab/show/Grothendieck+fibration#StreetFibration As remarked there, almost any fibration which arises in practice indeed satisfies the stronger non-kosher condition, and a functor is a Street fibration iff it factors as an equivalence of categories followed by a Grothendieck fibration. However, when working internally to a bicategory where the non-kosher version doesn't even make sense, Street's version is essential. Regarding groupoids, it's easy to see that every functor between groupoids is a Street fibration. Grothendieck fibrations between groupoids can be identified with "isofibrations," which are the fibrations in the canonical model structure on Gpd. It seems to me that the use of groupoid fibrations in the groupoid model of type theory is really an artifact of the desire to describe that model treating Gpd as a 1-category, rather than a 2-category. If one defined the identity types and pullbacks using limits in Gpd in the kosher 2-categorical sense, then it seems to me that one should be able to define an equivalent model using arbitrary functors between groupoids to represent the dependent types, rather than merely the fibrations. Similarly, in homotopical models of type theory where the dependent types are represented by the fibrations in some model structure, it seems that one should equivalently be able to work with the oo-category presented by that model structure and use arbitrary maps, but with all the structure defined using kosher oo-categorical limits. The non-kosher version using a model structure on a 1-category and fibrations may certainly be *easier* to describe and work with, and there is no reason not to do so in practice -- but just as is usually the case in homotopy theory, it seems to me that one should regard this as merely a convenient way to "present" the "real" underlying structure, which is higher-categorical and kosher. Mike On Wed, Sep 15, 2010 at 4:43 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
On the occasion of the discussion about "evil" I want to point out an example where speaking about equality of objects seems to be indispensible. If P : XX -> BB is a functor and one wants to say that it is a fibration then one is inclined to formulate this as follows
if u : J -> I is a map in BB and PX = I then there exists a morphism \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ...
I don't see how to avoid reference to equality of objects in this formulation.
This already happens if XX and BB are groupoids where P : XX -> BB is a fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X with P\phi = u.
Ironically the category of groupoids and fibrations of groupoids as families of types was the first example of a model of type theory where equality may be interpreted as being isomorphic.
So my conclusion is that equality of objects is sometimes absolutely necessary. Avoiding reference to equality is also not a question of using dependent types as some people implicitly seem to say. Even in intensional type theory there is a notion of equality. But it is sometimes inconvenient to use. As pointed out by Ahrens one can and should use extensional type theory whenever convenient. Intensional type theory allows one to interpret equality as being isomorphic, a kind of reward for the inconvenience of using intensional identity types.
Thomas
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 15 Sep 2010, at 08:43, Thomas Streicher wrote:
On the occasion of the discussion about "evil" I want to point out an example where speaking about equality of objects seems to be indispensible. If P : XX -> BB is a functor and one wants to say that it is a fibration then one is inclined to formulate this as follows
if u : J -> I is a map in BB and PX = I then there exists a morphism \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ...
I don't see how to avoid reference to equality of objects in this formulation.
If one tries to define fibrationhood as a property of functors, "P : XX --> BB is a fibration", then indeed talking about equality of objects seems unavoidable. The problem is exactly turning the object part F : ob XX ---> ob BB into a function ob BB ---> Sets. But if instead we define a set of "fibrations over BB", then we can do it: a fibration over BB is a function ob BB ---> Sets, together with etc. etc. (I gave more details in a post on June 2, answering a similar question.) Now, in classical foundations, this is (1-)equivalent to the usual definition. Within a dependent type theory foundation, they are only rather more weakly equivalent; and in that case I'd hazard that something along these lines is a more natural/fruitful definition. Digressing a little further, a similar situation arises for many other classes of maps that are viewed as "fibrations" or some sort: in a dependently-typed foundation, it's often more natural to consider a type of "fibrations over B", which then have "total spaces" that are maps into B, rather than defining "f is a fibration" as a property of maps. The most fundamental case is just in Sets, with (classically) "all maps are fibrations": in a dependent system, a "fibration over B" is a function B --> Sets, which may not be quite the same as a map E --> B. -p. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Michael, Street's notion of fibration is a weakening not a strengthening of Grothendieck fibrations. For such a thing the key intuitions are lost as far as I can see (even if I and J are isomorphic the fibre over I may be inhabited whereas the fibre over J is inhabited). I doubt that category theory over a base (topos) can be deloped this way. At least it would be very cumbersome. Has the generalised notion of fibration been used for something? I agree with you that Kan fibrations in simplicial sets are an alternative and certainly the right thing if one want's to get "weak". After all that's what I suggested in 2006 in a talk in Uppsala. I personally am interested in the possibility of having type theories where equality coincides with being isomorphic or even weakly equivalent (as recently suggested by Voevodsky). But this is an extremal point of view which shouldn't be taken absolute since otherwise important parts of category theory get lost. I suspect that when doing fibered categories in a type theory validating Voevodsky's equivalence axiom one comes up with something like Street's generalisation of fibrations. But that doesn't mean that we arrive at something easy to work with. What Martin Hofmann and I thought when bringing up the idea was that use of intensional Id-types amounts to imposing a brutal bureaucracy which FORCES you to check all the coherence conditions often swept under the carpet. I think when interpreting type theory in the topos SSet of simplicial sets one can have both extensional Id-types and the intensional ones. In the first case a family of types is simply a map of SSet, in the second case it is a Kan fibration. Luckily both system of display maps are closed under \Sigma and \Pi. Thus the intensional model sits within the extensional one. It is the restriction to "kosher" types, i.e. Kan complexes. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Theorem. Equality if and only if the diagonal. Corollary. P(equality) <--> P(contraction) (where the predicate P may be "Evil", "Nonlinear", "Sophomoric", etc) In this context (as opposed to metric spaces, materials, and maternity wards) contraction is the logical rule predicated on the idea that two things with the same name are actually one. See Kripke and others on the topic of Naming and Necessity. Were Rosa Parks still around she would surely not judge equality evil. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thomas Streicher wrote in small part (in a post about fibrations):
Even in intensional type theory there is a notion of equality.
Elsewhere in the same thread, Vaughan Pratt wrote:
Theorem. Equality if and only if the diagonal.
and concluded that equality is no more or less evil than contraction. This depends on what kind of type theory you are using! In the intentional type theory of Martin-Loef, for example, there is a notion of equality (or identity) at each type. Heck, there's even a notion of identity of types! However, one can certainly consider type theory without identity types. I would suggest the internal language of a Heyting 2-pretopos (although that depends on what one takes this language to be). Logic should be the servant of intuition, not the master. If some category theorists have the intuition (and we do) that it is meaningless to speak of equality of objects, then it's the job of the logician to find a formal language which expresses only what these category theorists find meaningful. If they haven't done so, then this is something to work on, not an argument that the motivating intuitions are invalid. There is something else that logic can do, however: it can show that identity follows from something else. Vaughn's theorem (cited above) purports to do this, but it is based on the assumption that every operation between types (in this case, the diagonal Delta_X: X -> X x X) has (as "image" or "range") a predicate on the target type (in this case, the identity predicate on X x X). So if our intuition suggests that operations have ranges, then we must accept that we have identity predicates too (assuming that we can construct the diagonal operation using contraction). But my intution suggests no such thing for arbitrary types (such as might be suitable as the type of objects of a category); naively, given an operation f: X -> Y, the range predicate (ran f) on Y would hold at those objects of Y with the form f(a) for some object a of X. But given an object b of Y, how do you determine if it has this form? If we already had an identity predicate =_Y on Y, then we could do this: (ran f)(b) if and only if (for some x: A) (b =_Y f(a)). But in general, I don't see any meaning for the range of an operation. In fact, since I'm happy to use contraction in general mathematics, I would phrase Vaughn's theorem as follows:
Theorem. Equality if and only if ranges.
and conclude that equality is no more or less evil than ranges. But I don't believe in either of these, in general; that is, I believe in the usefulness of types that lack these. (Quiz: Given two arbitrary sets, say the set of natural numbers and the set of positive integers, how do you decide if they are equal? Similarly, given a set and an arbitrary operation on sets, say the set of rational numbers and the operation of cartesian square, how do you decide if the set belongs to the range of the operation? Or more relevantly, given the diagonal operation on sets, how do you decide if a pair of sets belongs to its range?) --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
It's no problem to come up with logics without equality predicates. Just omit the equality predicate and its associated axioms. For ideological reasons most logic texts give equality a distinguished status for historical reasons. In case of extensional theories it suffices to have equality on base type and lift it `a la logical relations. But then there might be operations which don't respect this kind of equality. In other words identity types are not necessary for doing constructive mathematics. Intensional Id-types arise from putting the idea to an extreme that all logical concepts are "inductively defined", i.e. are given by constructors and eliminators. The notion of equality of types you refer to is a different one. Namely judgemental equality which cannot be used as an ingredient for forming propositions. It seems to me t that the point simply is that use of equality in premisses can be avoided by declaring varibales appropriately. That trick goes a long way in basic category theory. Using Id-types is a different thing. Extensional Id-types together with sums correspond to "cartesian logic" which suffices for declaring a lot of categorical concepts. Intensional Id-types might be convenient for providing a logic where equality gets identified with isomorphism or even weak equivalence. But that's not avoiding equality it's rather `liberal'ising it. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thanks Thomas for bringing up the intensional type theory perspective. Here equality of objects in categories is a serious problem already for sets, or rather for their type theoretic counterpart, setoids (types with equivalence classes). The so-called identity types give a minimal equality on each type A: Id(A,a,b) are the proofs that a and b are equal in A. But the fact that these proofs are in general not unique and induces a groupoid structure makes it difficult to apply when e.g. A is a universe of types. Some remarks are contained in in this preprint http://www.mittag-leffler.se/preprints/files/IML-0910f-36.pdf If one tries to use the Id-types to define equality on (small) setoids one ends up with a groupoid of objects rather than a setoid objects. I think the situation can be described as follows for a general category K, which we think of as a category without equality of objects. We now want to induce an equality of objects on (a part of) K. Take a groupoid G and a functor F:G -> K. We define the groupoids of objects C_0, arrows C_1 and composable arrows C_2 in a natural way. C_0 is G and C_1 has for objects triples (a,b,f) where a,b in G and f:F(a) -> F(b), and a morphism (a,b,f) -> (a',b',f') is a pair of G morphisms r:a -> a' and s:b -> b' with F(s) f = f' F(r). C_2 has for objects pairs of morphisms composable with an mediating map m from G, i.e. ((a,b,f),(c,d,g),m). The composition is g F(m)f. The morphisms of C_2 are then pairs of C_1 morphisms ((r,s), (t,u)): ((a,b,f),(c,d,g),m) -> ((a',b',f'),(c',d',g'),m') with m's= t m. When G is a discrete groupoid this becomes a standard category. When G is a groupoid it becomes almost a category. Notions of limits can be formulated in a natural fashion. At least when K=Setoids, C inherits limits from K. Perhaps some general results are known about this construction of C from functor F:G -> K on a groupoid G? Erik
It's no problem to come up with logics without equality predicates. Just omit the equality predicate and its associated axioms. For ideological reasons most logic texts give equality a distinguished status for historical reasons. In case of extensional theories it suffices to have equality on base type and lift it `a la logical relations. But then there might be operations which don't respect this kind of equality. In other words identity types are not necessary for doing constructive mathematics. Intensional Id-types arise from putting the idea to an extreme that all logical concepts are "inductively defined", i.e. are given by constructors and eliminators. The notion of equality of types you refer to is a different one. Namely judgemental equality which cannot be used as an ingredient for forming propositions.
...... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Intensional Id-types might be convenient for providing a logic where equality gets identified with isomorphism or even weak equivalence. But that's not avoiding equality it's rather `liberal'ising it.
Vladimir Voevodsky just posted a draft manuscript about these issues: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Bas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Toby Bartels <toby+categories@ugcs.caltech.edu> wrote in part:
The point is that one can recognise that two syntactic expressions, such as x and x, are the same, ...
Sorry, Toby, when I see "such as x and x" I have to struggle to treat the expression between "as" and "and" as anything other than different from the expression following the "and" -- for, if they were really the same, there would be but one expression, not two, it would be in one of those positions only, not both (I'm put in mind of the good old "Cheech and Chong"-ism, "How can you be in two places at once, if you're not anywhere at all?"), and you'd have used not the plural verb form "are" but the singular "is". An illustration from another realm: each time the clerk behind the deli counter finishes with one customer and shouts "Next!" so as to bring up another one, the expression the clerk shouts refers to an entirely different customer than it did the time just before.
... or even that one reduces to another, such as fst(x,y) and x (where fst: A x B -> A is the usual projection),
Again I'm puzzled: what can fst(x,y) (where fst: A x B -> A is as you say) possibly have to do with x (as in A x B, presumably -- or did you mean as in fst(x,y), which could be problematic for void B)? Sorry to be so obtuse, but ...; cheers, -- Fred [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Let BB be a (base) topos. Then split fibrations over BB correspond to categories internal to Psh(BB). (Well, in Psh(BB) = Set^{BB^op} one has to choose Set big enough!). Thus in Psh(B) one can speak about split fibrations over BB as categories internal to Psh(BB). To which extent can this be extended to arbitrary fibrations P : XX -> BB typically not split. In a recent paper by Mike Shulman this has been exercised for the fundamental fibration P_BB : BB^2 -> BB. (Well, he was even exploiting that P_BB is a stack w.r.t. the regular topology on BB). But it works for every fibration P. One can speak about P in a first order dependently typed language L(P) without equality of objects. Generalized elements of sort "object" at stage I are objects of the fibre P(I) and similarly for morphisms. Now this language can be given a Kripke-Joyal interpretation in BB. If P is a JJ-stack then one thinks of BB as endowed with the topology JJ and incorporates this into the Kripke-Joyal interpretation. The key trick is that implicitly one quantifies over all possible reindexings. First I was quite enthusiastic about this because I thought that it augments the usual fibrational foundations of category theory over an arbitrary base topos with a linguistic framework entending that of the internal language of the base (or rather (pre)sheaves over it). But when trying to test the viability of this approach I came across the following problem. It is not enough to quantify over objects but one also has to quantify over families of objects indexed objects of BB. This leads one to consider also the family fibration Fam(P) over BB together with the cartesian functor FFam(P) from Fam(P) to P_BB. One can now easily cook up a language speaking about P, Fam(P) and the cartesian functor FFam(P). The first thing one wants to show is that the proposition "Fam(P) is a fibration" holds under the Kripke-Joyal interpretation. But when writing this down one sees that one cannot escape equality of objects which has been dropped to make the whole thing possible. Thus it might be easier to replace P by an equivalent split fibration Sp(P) and reason about this in Psh(BB). Nothing seems to be lost when one considers everything up to isomorphism. The question rather is whether this excessive prevention of "evil" is appropriate. I have some doubts since it prevents us from speaking about fibrations in a natural way. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Yes, fibrations in the original sense of Grothendieck are "evil" (sorry, Jean!), as is shown by the fact that an equivalence of categories is not in general a fibration. There is a weaker notion of fibration in which one replaces the equality "P\phi = u" by a (specified) isomorphism PY -> J making the obvious triangle commute. But every fibration in this sense factors as an equivalence followed by a fibration in Grothendieck's sense, so it's not such an important notion. Peter Johnstone On Wed, 15 Sep 2010, Thomas Streicher wrote:
On the occasion of the discussion about "evil" I want to point out an example where speaking about equality of objects seems to be indispensible. If P : XX -> BB is a functor and one wants to say that it is a fibration then one is inclined to formulate this as follows
if u : J -> I is a map in BB and PX = I then there exists a morphism \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ...
I don't see how to avoid reference to equality of objects in this formulation.
This already happens if XX and BB are groupoids where P : XX -> BB is a fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X with P\phi = u.
Ironically the category of groupoids and fibrations of groupoids as families of types was the first example of a model of type theory where equality may be interpreted as being isomorphic.
So my conclusion is that equality of objects is sometimes absolutely necessary. Avoiding reference to equality is also not a question of using dependent types as some people implicitly seem to say. Even in intensional type theory there is a notion of equality. But it is sometimes inconvenient to use. As pointed out by Ahrens one can and should use extensional type theory whenever convenient. Intensional type theory allows one to interpret equality as being isomorphic, a kind of reward for the inconvenience of using intensional identity types.
Thomas
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Sure, they are "evil" but it seems to be beneficial to be "evil" sometimes. If the equivalence closed version would have been the original one I doubt that it would have been recognized how useful they are for category theory over fairly general bases. Or, rather, people would have quickly shifted to the "evil" version. BTW under a regime which identifies equality with being isomorphic (or weakly equivalent) it looks tempting to use functors from B^\op to Cat. These should capture the pseudo-functors since equality and isomorphism are identified. But writing down functoriality in type theory using \Sigma for existence amounts to choosing a lot of not at all canonical "canonical isomorphisms". Actually, one would get something even more general than pseudo-functors because one wouldn't write down the coherence conditions (actually one couldn't even since there is no honest for good equality!). Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Mike wrote:
If one defined the identity types and pullbacks using limits in Gpd in the kosher 2-categorical sense, then it seems to me that one should be able to define an equivalent model using arbitrary functors between groupoids to represent the dependent types, rather than merely the fibrations.
This seems (to me) to be analogous to extending one's notion of covering space to allow for empty fibres - indeed, the characterisation of covering spaces as representations of Pi_1 needs this. David PS +1 for using 'kosher' :) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thomas wrote, of fibrations: Sure, they are "evil" but it seems to be beneficial to be "evil" sometimes.
Of course! Anybody who thinks that concepts should be avoided merely because they're "evil" in the technical sense must also think that odd numbers are peculiar and perfect groups are the best groups to study. I'm finding it quite amusing how people are getting worked up over the concept just because its name has moral overtones. An excellent example of an evil but useful concept is the concept of "skeletal category". Every category is equivalent to a skeletal one (assuming choice), but not every category is skeletal. So, this concept is evil. But it's sometimes nice to prove a theorem for all categories by proving it for skeletal categories. We can formalize this a bit. Remember, a property P of objects in an n-category is "evil" if there's an object with that property that is equivalent to an object without that property. It's "non-evil" if whenever x has property P and x is equivalent to y, y also has that property. (I'm using classical logic here. If we're using intuitionistic logic, the really useful concept is the concept that I'm calling "non-evil". We should probably call it "good": evil is just the absence of good. But "non-evil" is less likely to cause confusion.) Every property P can be made non-evil by defining a new property P' that means "equivalent to something with property P". Sometimes it's more convenient to work with objects with property P than objects with property P'. And note: if the property Q is non-evil, the theorem all objects with property P have property Q automatically implies all objects with property P' have property Q So, for example, if Q is a non-evil property of categories, to prove Q holds for all categories it suffices to prove it for skeletal categories. Or - with a bit more work to fill in the details - if Q is a non-evil property of functors, to prove Q holds for all Street fibrations it suffices to prove it for fibrations. Best, jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Thomas Streicher wrote at last:
BTW under a regime which identifies equality with being isomorphic (or weakly equivalent) it looks tempting to use functors from B^\op to Cat. These should capture the pseudo-functors since equality and isomorphism are identified. But writing down functoriality in type theory using \Sigma for existence amounts to choosing a lot of not at all canonical "canonical isomorphisms". Actually, one would get something even more general than pseudo-functors because one wouldn't write down the coherence conditions (actually one couldn't even since there is no honest for good equality!).
Yes, you can write the coherence conditions down (although I agree that it would be easy to forget them). What you need is that a functor (pseudofunctor) P: B^\op -> Cat is not just the following data: * for each object x of B, a category P_x, * for each object x, object y, and morphism f: x -> y, a functor P_f: P_x -> P_y, * functoriality structure (and maybe coherence conditions); but in fact the following data: * for each object x of B, a category P_x, * for each object x, object y, and morphism f: x -> y, a functor P_f: P_y -> P_x, * for each object x, object y, and equal morphisms f = g: x -> y, a natural isomorphism P_{f=g}: P_f => P_g, * functoriality structure and coherence conditions. For example, given f: w -> x, g: x -> y, and h: y -> z in B, we want to compare (P_f . P_g) . P_h with P_f . (P_g . P_h). In a "kosher" treatment of category theory, these aren't equal (that would be meaningless), but there is an associator between them. As a coherence condition, we want to demand that this associator is equal (and this does have meaning) to a natural isomorphism built out of the functoriality structure isomorphisms and their inverses. As we do this, we need to compare P_{(f;g);h} and P_{f;(g;h)}. Again, it's not meaningful (much less true) that these are equal, but P_{(f;g);h = f;(g;h)} is a natural isomorphism between them. So we can write down this coherence condition after all. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
We seem to agree that paying attention to the non-kosher concept is at least very convenient. But what I do not see is a correspondence between kosher and non-kosher versions. If you start with a collection CC of 1-cells in a 2-cat like Cat and close it under equivalences thus obtaining CC' I don't see any way of reconstructing CC from CC' in a canonical way. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear John, A property is "evil" in your sense if it is not invariant under equivalences. Invariance under equivalence is a well established mathematical notion. I prefer to say that something is not invariant under equivalence than to say that it is "evil". There is no need to introduce a new terminology. Best, André [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Andre: Brevity is the usual reason for introducing new terminology. And, ultimately there is a need, as mathematics would grind to a halt if one had to write out a phrase giving the content of each concept whenever one wanted to talk about it. One may object to the jocular use of a word with a moral denotation as the name for a mathematical concept, but four characters beats 28 characters (or 31 if one counts spaces). It certainly seems desirable to have a brief name for either "invariant under equivalence" or "not invariant under equivalence". Best Thoughts, David Y. On 18 Sep 2010, at 08:50, Joyal, André wrote:
Dear John,
A property is "evil" in your sense if it is not invariant under equivalences. Invariance under equivalence is a well established mathematical notion. I prefer to say that something is not invariant under equivalence than to say that it is "evil". There is no need to introduce a new terminology.
Best, André
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear David, I appreciate your view. I would love to have the dictatorial power to reform the mathematical vocabulary. I dream of kicking out long words like diffeomorphism and homeomorphism. I guess that if they have persisted in mathematics, it is because everybody understand them. It is very difficult to impose a new terminology. There is a social aspect to the problem. Even if small group of peoples agree in using a new terminology, this may have little influence on the larger community. The new word may become a tag for identifying the members of a group. It may enclose its user into a sub-culture. Best, andré -------- Message d'origine-------- De: David Yetter [mailto:dyetter@math.ksu.edu] Date: dim. 19/09/2010 10:57 À: Joyal, André Cc: John Baez; categories Objet : Re: categories: Re: are fibrations evil? Dear Andre: Brevity is the usual reason for introducing new terminology. And, ultimately there is a need, as mathematics would grind to a halt if one had to write out a phrase giving the content of each concept whenever one wanted to talk about it. One may object to the jocular use of a word with a moral denotation as the name for a mathematical concept, but four characters beats 28 characters (or 31 if one counts spaces). It certainly seems desirable to have a brief name for either "invariant under equivalence" or "not invariant under equivalence". Best Thoughts, David Y. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
I completely agree with Andre. I add: Furthermore, the introduction of new terminology (specially if this terminology refers directly to a meaning in everyday life) with no real need and/or to change established terminology, is an habit that harm the credibility of any school of research. In the present case we are discussing a particular single word "x" to replace the compound "not invariant under equivalence". This seems justified by its frequent use, but its frequent use is due precisely because we are discussing its use !!!. In the practice of category theory or mathematics, its use is not frequent enough to justify the introduction of new (simpler) terminology. What happens with readers which see "x" and do not belong to our group ?. Well, most will be upset , and specially if "x is evil" (ja !). Joyal wrote:
Dear John,
A property is "evil" in your sense if it is not invariant under equivalences. Invariance under equivalence is a well established mathematical notion. I prefer to say that something is not invariant under equivalence than to say that it is "evil". There is no need to introduce a new terminology.
Best, André
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Andre is very polite, I call such a subculture "ghetto", and Benabou calls it "Category land". Joyal wrote:
Dear David,
I appreciate your view. I would love to have the dictatorial power to reform the mathematical vocabulary. I dream of kicking out long words like diffeomorphism and homeomorphism. I guess that if they have persisted in mathematics, it is because everybody understand them.
It is very difficult to impose a new terminology. There is a social aspect to the problem. Even if small group of peoples agree in using a new terminology, this may have little influence on the larger community. The new word may become a tag for identifying the members of a group. It may enclose its user into a sub-culture.
Best, andré
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
To partially answer a question posed by Eduardo (in the case "x = evil") :
What happens with readers which see "x" and do not belong to our group ?.Well, most will be upset , and specially if "x is evil" (ja !).
They go to the nLab and read about "x": http://ncatlab.org/nlab/show/evil Best, Alex [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Eduardo J. Dubuc wrote:
Furthermore, the introduction of new terminology (specially if this terminology refers directly to a meaning in everyday life) with no real need and/or to change established terminology, is an habit that harm the credibility of any school of research.
Shall we stop saying "natural" and say "invariant under composition"? Or is that term allowed under the grandfather clause, since it was being used imprecisely before category theory defined it? If I can find a citation where John Baez used the term "evil" before he knew how to define it, will that make it OK? Or is that irrelevant because John was already working in the ghetto?
In the present case we are discussing a particular single word "x" to replace the compound "not invariant under equivalence". This seems justified by its frequent use, but its frequent use is due precisely because we are discussing its use !!!.
As a proud citizen of the Ghetto of Category Land, I've used that term in other contexts than this discussion. If you do not wish to join us, what does that matter? You may continue to write down strict definitions, and we will continue to weaken them as we need. Different styles of mathematics are not at war. I understand that "evil" is grating; other terms have been suggested. But no, *any* short term to replace "not invariant under equivalence" is forbidden by your decree: it relegates us to the ghetto. Well, that is your interpretation, but it doesn't affect my mathematics. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (15)
-
Alex Hoffnung -
Bas Spitters -
David Roberts -
David Yetter -
Eduardo J. Dubuc -
Erik Palmgren -
Fred E.J. Linton -
John Baez -
Joyal, André -
Michael Shulman -
Peter LeFanu Lumsdaine -
Prof. Peter Johnstone -
Thomas Streicher -
Toby Bartels -
Vaughan Pratt