Dear Andre,

The test: Can we define a notion of category internal to a symmetric monoidal category without using a coalgebra structure on the object of objects?

the quickest reference I can find is the very incomplete page http://ncatlab.org/nlab/show/internal+category+in+a+monoidal+category but more importantly, the thesis referenced there. As I remark at the above page, Ross Street would know something about this. As to the other idea, someone (Toby Bartels perhaps) once said that explicitly equipping 'sets' with a notion of when elements are equal goes back to Cantor. I find thinking of the undergraduate (or high school) definition of equality of functions |R --> |R as a pale shadow of the idea of preset. Consider the collection of expressions denoting functions (even restricting to polynomials), this is a preset with the equality relation given by when one algebraic expression gives the same function as another algebraic expression. Best, David Roberts 2010/1/13 Joyal, André <joyal.andre@uqam.ca>:

Dear All,

I cannot imagine a category without an equality relation between the objects of this category. Ok, I may have been brainwashed by my training in mathematics at an early age. But more seriously, I think that the equality relation is inseparable from the idea of a set. I do not understand what a preset is:

http://ncatlab.org/nlab/show/preset

Two things are equal if they are the same, if they coincide (whatever that mean!). Without this notion, an element of a set has no identity, no individuality. Of course, a set is often constructed from other sets, as in arithmetic with congruence classes. I am fully aware that the equality relation between the objects of a category is not preserved by equivalences in general. But the art of category theory consists partly in knowing which construction on the objects and arrows of a category is invariant under equivalences.

I would like to propose a test for verifying if the notion of category can be freed from the equality relation on its set of objects. The equality relation on an ordinary set S is defined by the diagonal S-->S times S. The objects of a symmetric monoidal category have no diagonal in general, ie no coalgebra structure.

The test: Can we define a notion of category internal to a symmetric monoidal category without using a coalgebra structure on the object of objects?

Best, André

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Dear André, I do not understand the point of your "test". What Bob Paré said, and which I agree with, is that equality is "okay" for small categories. And as Paul Taylor wrote, by "small" what one really means is "internal". So, of course, it makes sense that V-internal categories (where V is a not-necessarily-braided monoidal category with distributive coreflexive equalisers) should have a comonoid of objects. But this in no way contradicts the assertion that _large_ categories should not have an equality relation between objects---internal categories are tautologously small! Not being as familiar with indexed categories/fibrations as I ought to be, I tend to think of large categories in terms of enriched category theory. Here, we see very clearly that the collection of objects has nothing whatsoever to do with the enriching category V, and this is as it should be. In fact, I suppose that it probably would make sense to generalise enriched categories by taking a (large) groupoid of objects (and _canonical_ isos, in the spirit of Paré and Schumacher) instead of a mere class. I don't know if this has ever been done. My main point is that you are right in asserting that a set without an equality relation is not a set. But the exact meaning of large category is one whose objects do not necessarily form a set! Morally speaking, "set" does mean "collection that has an equality predicate", but this leaves open the possibility that there are collections which do not have such a predicate, and which are therefore not sets. These suffice for the purpose of large category theory---for example, they suffice for the purpose of enriched categories; moreover, FOLDS is explicitly based on these principles. Cheers, Jeff. ----- Original Message ----

From: "Joyal, André" <joyal.andre@uqam.ca> To: categories@mta.ca Sent: Tue, January 12, 2010 4:24:39 PM Subject: categories: A challenge to all

Dear All,

I cannot imagine a category without an equality relation between the objects of this category. Ok, I may have been brainwashed by my training in mathematics at an early age. But more seriously, I think that the equality relation is inseparable from the idea of a set. I do not understand what a preset is:

http://ncatlab.org/nlab/show/preset

Two things are equal if they are the same, if they coincide (whatever that mean!). Without this notion, an element of a set has no identity, no individuality. Of course, a set is often constructed from other sets, as in arithmetic with congruence classes. I am fully aware that the equality relation between the objects of a category is not preserved by equivalences in general. But the art of category theory consists partly in knowing which construction on the objects and arrows of a category is invariant under equivalences.

I would like to propose a test for verifying if the notion of category can be freed from the equality relation on its set of objects. The equality relation on an ordinary set S is defined by the diagonal S-->S times S. The objects of a symmetric monoidal category have no diagonal in general, ie no coalgebra structure.

The test: Can we define a notion of category internal to a symmetric monoidal category without using a coalgebra structure on the object of objects?

Best, André

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

hi. several people suggest dependent type theory as a foundation to formalize categories. maybe it is worth mentioning that per martin- loef (the originatory of dependent types) worked this out, prolly in the 70s. that was one of his early examples. many people who implemented basic category theory in the 80s (burstall-rydeheard, NuPRL team etc) followed this design. i am sure that there are people on the list who know much more about this than i do. while martin-loef's construction is quite natural and easy to reconstruct, one idea that still seems to be missing here, and leads to some confusion: the distinction between the extensional equality, ie term conversion, and the intentional equality, ie equality types. without going into any details, let me suggest that this formalization may clarify some confusion. in martin loef's formalization, the composition operation does not involve equality: no equality expressions occur in the expression Hom(A,B) # Hom(B,C) ---> Hom(A,C). what does occur are two copies of B. but ***being able to copy B is not the same thing as being able to decide the equality predicate***. mapping things along the diagonal is not the same thing as being able to decide whether something lies in the image or not. in practice, if i give you an object (say a group B) you will have no problem to make two identical copies of that group, in whichever form it may be given. but if i give you two big complicated groups, and you want to know whether they are equal on the nose, then you need to see how they are represented. in other words, you need to open the black boxes, and see what exactly are the elements of these groups etc. and this is not very categorical. as we all know, the whole point of eg the universal properties is that you describe things without opening any black boxes. one more thing, also apparent from any formalization: the reason why the object equality is no problem for small (internal) categories is that their objects can be viewed as arrows of the base category (and the arrows are, of course, in the business of being equal or not). -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

[[sorry about the delay with replying: i am travelling.]] On Jan 14, 2010, at 6:23 AM, Colin McLarty wrote:

...

several people suggest dependent type theory as a foundation to formalize categories. maybe it is worth mentioning that per martin- loef (the originatory of dependent types) worked this out, prolly in the 70s.

Is there a published account of this, preferably on the web?

i am not aware of any of martin-loef's writings on the web. i was talking from memory (as i am not near my filing cabinet with the paper copies). martin-loef's category theory example could be in his bibliopolis book, or in one of his Logic Colloquium contributions. -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

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/ ]

Just to respond to one aspect of this: Joyal wrote:

I am also reluctant to base category theory on type theory because constructive mathematics tends to be much more complicated than ordinary mathematics.

I can't speak for others, but I did not intend, in making the suggestion to base category theory without equality for objects on type theory, that constructive mathematics be necessarily also adopted. While many of the adherents of type theory have a constructive point of view, and type theory is a natural home for constructive mathematics, type theory with classical logic is also a perfectly well-defined notion. Its type-theoretic properties are not as good as those of the constructive version, but that's irrelevant for the purposes I had in mind: it can be used as a language just like the ordinary classical first-order logic in which classical set theories such as ZFC are formulated. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]