Dear All, Many people have expressed their view on the problem posed by the equality relation. I warmly thank everyone for that. I would like to make some general observations. I apologise for not answering individually. First, I have a litte story to tell. [A tale of giants, small and large. I remember when I first encountered the big sets obtained from the set of natural numbers by iterating the power set operation a finite number of times. I was scared and amazed by their size but I was reassured by my teacher who told me they were good. I often thought about them because I was studying real numbers and analysis. We eventually became close friends and I was happy to accept the whole family in my mathematical house. But once living in my house, they received the visit of their relatives, first the brothers, then the cousins, and later some higher degree cousins. The relatives were bigger, stokier, but they were all very kind. I had no objection in making them a place in my house if they wanted to live with me. But eventually, the relatives were arriving endlessy and I began to worry that my house may collapse. I could not find a fair rule to bar the newcomers from my house. I was apparently losing control. This is why I felt some relief when I learned from a high priest that my home giants were actually dwarfs compared to a race of mega-giants, the larges. The giants were so much bigger than me and bigger than anything I could see directly. But the priest, a distant relative of Bertrand Russel, also told me that I should be very wary of the mega-giants, because "the equality relation may not be well defined on a large set". The truth is that I could not perceive a real difference between the large giants and the biggests among the small giants. There was only a vague difference of scale, not really of shape. After taking some vacation in which I did some meditation, I decided to be fair with all creatures, small and large, and behave as if they were all good. I ignored the advice of the priest and welcomed the large giants in my house. My house did not collapse and I am enjoying mathematics even more.] The notion of equality is raising a lot of questions, running from the theory of classes to constructive mathematics, from categorical logic to higher category theory and homotopy theory. It has also ramifications in philosophy. I will only discuss a limited numbers of aspects. The main character in the arena of constructive mathematics is represented by Martin-Lof intensional types theory. Let me give a few references, since category theorists are not always familiar with type theory: http://en.wikipedia.org/wiki/Intuitionistic_type_theory [B. Nordstöm, K. Petersson, and J. M. Smith Martin-Löf s Type Theory Handbook of Logic in Computer Science, Vol. 5 Oxford University Press, 2001] For an introduction to dependant type theory, see http://www.math.unipa.it/~ngambino/dtt.html A salient feature of the system is the formation rule which associates to two terms a and b of type A another type Id_A(a,b). A term c of type Id_A(a,b) is a proof of the equality a=b. It can also be interpreted as an isomorphism c:a-->b. A semantic using isomorphisms and groupoids was proposed by Curien in 1993 and constructed by Hoffman and Streicher in 1994: [Hofmann, M. and Streicher, T. (1994) A groupoid model refutes uniqueness of identity proofs. Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, France] A semantic based on paths and spaces was later proposed by Steve Awodey and Michael Warren in 2007: http://arxiv.org/abs/0709.0248 A semantic based on weak omega-groupoids was proposed by Beno van den Berg and Richard Garner in 2008, and also by Lumsdaine: http://arxiv.org/abs/0812.0298 http://arxiv.org/abs/0812.0409 In these models, a dependant type type A(x), with x a variable of type B, is interpreted as a fibration A(x)--->B. Nicola Gambino and Richard Garner have introduced a notion of fibration in the classifying category of type theory: http://arxiv.org/abs/0803.4349 These developements illustrate the fact that there is a tantalising connection between type theory, higher category theory and homotopy theory (see the paper of Awodey and Warren above). Classical first order intuitionistic logic has a natural semantic in toposes. It is natural to conjecture that intensional type theory has a natural semantic in infty-toposes. One problem is that an infty-topos is not an ordinary category, it is an (infty,1)-category. There are many *brands* of (infty,1)-categories and they are all equivalent: http://arxiv.org/abs/math/0610239 http://arxiv.org/abs/math/0504334 http://arxiv.org/abs/math/0607820 It is not clear which *brand* of (infty,1)-categories is best for the semantic of type theory. At first, the simplicial category *brand* appears to be the simplest because a simplicial category is just a category enriched over simplicial sets. But homotopy theoretic constructions in simplicial categories are notoriously complex. For example, we have to use homotopy coherent diagrams instead of plain commutative diagrams, http://www.ams.org/tran/1997-349-01/S0002-9947-97-01752-2/home.html The corresponding constructions in quasi-categories are much simpler. This is why Jacob Lurie is using quasi-categories instead of simplicial categories (his thesis on infinity-toposes was originally written with categories enriched over spaces). http://arxiv.org/abs/math/0610239 This leads to the general problem of representing (infty,1)-categories by various kind of categorical structures. One can use *homotopical categories* for that http://www.ams.org/bookpages/surv-113/ A homotopical category is a category C equipped with a class W of "weak equivalences". Every homotopical category (C,W) has a *quasi-localisation* C[W(-1)] which is a quasi-category. The simplicial set C[W(-1)] is obtained from the nerve of C by freely gluing a homotopy inverse to each arrow in W, and then, by adding simplicies to turn it into a quasi-category (this last step is called a fibrant completion). The quasi-category C[W(-1)] is equivalent to the Dwyer-Kan localisation of C with respect to W, via the equivalence between quasi-categories and simplicial categories, http://arxiv.org/abs/0910.0814 http://arxiv.org/abs/0911.0469 Conversely, every quasi-category is equivalent to the quasi-localisation of a homotopical category. This gives a representation of all (infty,1)-categories in terms of homotopical categories. It follows that many aspects of the theory of (infty,1)-categories can be expressed in terms of category theory. When the homotopical category (C,W) is obtained from a Quillen model structure (by forgetting the cofibrations and the fibrations) the quasi-category C[W^(-1)] has finite limits and colimits. Conversely, I conjecture that every quasi-category with finite limits and colimits is equivalent to the quasi-localisation of a model category. In fact, every locally presentable quasi-category is a quasi-localisation of a combinatorial model by a result of Lurie. More can be said: the underlying category can taken to be a category of presheaves by a result of Daniel Dugger. http://arxiv.org/abs/math/0007070 Denis-Charles Cisinski has studied the model structures on a Grothendieck toposes in which the cofibrations are the monomorphisms. [Théorie Homotopique dans les topos, JPAA, Vol 174 (2002), pp 43-82] It should be very interesting to know which combinatorial model structures on a Grothendick topos are giving rise to infty-toposes after quasi-localisation. These "model topos" could possibly serve as a semantic for intensional type theory. This leads to the more general problem of "modelling" higher categories. All higher categories can be represented as fibrant objects in a model category. Charles Rezk has recently proposed a model structure for n-quasi-category: http://arxiv.org/abs/0901.3602 Finally, let me return to the equality problem. I agree that the meaning of the equality relation between the objects of a large category is unclear. The is because the set theoretic incarnation or representation of a mathematical structure depends on arbitrary choices. For example, the real euclidian space could be construct as (R times R) times R or as R times (R times R). where R is the real line. They are different sets, but as far as geometry goes, it does not matter. I like to use it in a course for an example of a monoidal category which is not strict. Not every monoidal category is strict, since the the category of sets is not! I am reluctant to accept the notion of preset, a set without an equality, because I do not understand what it means. I am also reluctant to base category theory on type theory because constructive mathematics tends to be much more complicated than ordinary mathematics. I doubt that constructive mathematics will be adopted by the mathematical community any time soon, probably not before the collapse of human civilisation due to climate warming! (I hope it will not collapse, but we should be wary). But type theory could become important in computer science in the short term: [B. Nordström, K. Petersson, and J. M. Smith Programming in Martin-Löf s Type Theory Oxford University Press, 1990] Classical set theory is our best friend. It should not be throwned away because of philosophical doubts about the equality relation. It should be used (and perfected) until we have a better alternative or until it breaks. The theory of sets is axiomatic and we may choose the axioms quite freely for their simplicity, beauty and practical values. This is why I am ready to use large sets whenever possible when they seem useful. Category theory based on classical set theory works very well. The category of large sets is a pretopos equipped with a notion of small maps (algebraic set theory). It has many other properties that should be investigated. For example, I suspect that its category of internal categories has a natural Quillen model structure. I conjecture that this is true also for many other categories of internal structures. For example, there should be a model structure for internal n-quasi-categories for any n. I believe that the encoding of higher category theory in terms of ordinary category theory and set theory is not artificial. It depends on deep mathematical structures and ideas. It is using Quillen model structures and combinatorics. Many people have suggested using indexed categories and stacks to handle large categories. The notion of stack is extending that of sheaf. The category of all sheaves on a site is a Grothendieck topos and the category of all stacks may be called a Grothendieck cosmoi (I apologise to Ross Street for perverting his terminology). The quasi-category of Rezk categories internal to a 1-topos is an another example of cosmoi, but not every cosmoi is of this form. The theory of cosmoi can be developed by using model structures. Best, André PS: My "challenge to all" was met with a deafening silence as far as producing a counter-example is concerned. Ross Street and Brian Day have a notion of quantum category, but as Ross pointed out, its object of objects has a coalgebra structure. [Quantum categories, star autonomy, and quantum groupoids, in "Galois Theory, Hopf Algebras, and Semiabelian Categories", Fields Institute Communications 43 (American Math. Soc. 2004) 187-226] Ross wrote:
Take V to be the monoidal category of vector spaces (say). Write Comod(V) for the monoidal bicategory whose objects are comonoids C in V and whose morphisms C --> D are left C-, right D-comodules; composition of these morphisms involves an equalizer. Actually Comod(V) is an autonomous monoidal bicategory with the dual C^o of C obtained by following the diagonal by a switch (symmetry or braiding would do for more general V). Notice that C^o (tensor) C becomes a pseudomonoid in Comod(V). A quantum category in V consists of a comonoid C in V together with a monoidal comonad on C^o(tensor) C.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]