* the definition of "evil" @ 2010-01-03 7:23 Peter Selinger 2010-01-03 17:10 ` Claudio Hermida ` (4 more replies) 0 siblings, 5 replies; 28+ messages in thread From: Peter Selinger @ 2010-01-03 7:23 UTC (permalink / raw) To: Categories List Dear all, sorry for sending yet another message on the topic of "evil" structures on categories. After some interesting private replies, as well as Dusko's latest message (which should have appeared on the list by the time you read this), I noticed that not everyone is agreeing on the technical meaning of the term "evil". I will therefore attempt to state a more precise technical definition of the term as I have used it. Perhaps 2-category theorists already have another name for this. The information definition I had used is that a structure is "evil" if it does not "transport along equivalences of categories". I thought it was reasonably obvious what was meant by "transport along", but there is actually a lot of variation in what people understand this phrase to mean. John Baez gave a pointer to a website containing a technical definition of "evil": http://ncatlab.org/nlab/show/evil. Unfortunately, this site only speaks of properties, not structures. It is easy to state what it means for a property of categories to be transported along equivalences: namely, if C has the property, and C and C' are equivalent, then C' has the property. Structures are more tricky. Certainly, it should not just mean that if C admits such a structure, and C' is a category equivalent to C, then C' admits such a structure. (Then "admitting a structure" would merely be a property). This seems to be the definition Dusko has used. If we used this definition, there would be almost no evil structures; in particular, the original (strict) notion of dagger category is not evil in this sense. Dagger structure is reflected by full and faithful functors, and therefore by one half of an equivalence. The point is that the other half won't respect it. At least to me, "transported" suggests that the given equivalence respects the structure in some sense. So here is my attempt at a definition. DEFINITION. Let X be some structure on categories. By this, I mean that there is a given 2-category called X-Cat, whose objects are called X-categories, whose morphisms are called X-functors, and whose 2-cells are called X-transformations, and for which there is a given 2-functor U to Cat, called the forgetful functor. We say that X is "transported along equivalences of categories" if the following holds. Given an X-category D', with underlying category D = U(D'), and a category C, and an equivalence (F,G,e,h) of categories D and C, where F: D -> C, G: C -> D, and e: FG -> id_C, h: GF -> id_D, it is then possible to find: (1) an X-category C' whose underlying category U(C') is isomorphic [not equivalent!] to C. Let c : U(C') -> C be the isomorphism (i.e., an invertible functor in Cat) with inverse c': C -> U(C'); (2) an X-equivalence of X-categories (F',G',e',h'), where F': D' -> C', G': C' -> D', e': F'G' -> id_C', and h': G'F' -> id_D' [the concept of equivalence makes sense in any 2-category]; such that (3) (U(F'), U(G'), U(e'), U(h')) = (cF, Gc', cec', h). Here, cF and Gc' denotes composition of functors, and cec' denotes whiskering. The structure X is called "evil" iff it is not transported along equivalences of categories. This finishes the definition. More informally, "transported along equivalences" therefore means that if D and C are equivalent, and D has an X-structure, then there is a way to equip C with an X-structure and to lift the original equivalence to an X-equivalence. There was a need for the isomorphism c in the definition, because the forgetful functor U : X-Cat -> Cat may not be strictly speaking surjective onto 0-cells in some real-life examples (and in any case, this forgetful functor may sometimes only be well-defined up to isomorphism). It is important that c is an isomorphism, rather than an equivalence, because else the definition becomes vacuous (and we are precisely interested in notions that are not well-defined up to equivalence). Also note that I didn't require the data (C',F',G',e',h') to be unique, not even up to equivalence in X-Cat. Although in practice, it will often be unique in this sense. So my definition allows for a given structure to be transported "in essentially more than one way" along a given equivalence. I am open to strengthening the definition to forbid this. It is clear that the definition generalizes to any 2-category instead of Cat, so one might for example speak of structures on monoidal categories, or on categories-with-a-distinguished-subcategory, or even on dagger categories, as being evil or not. Here are some examples of structures: * monoidal structure on categories is non-evil (for concreteness, taken with strong monoidal functors and monoidal natural transformations). * strict monoidal structure is evil, when taken with strict monoidal functors. With strong monoidal functors, I think it is still evil, but I am not sure at this late hour. * dagger structure is evil. More generally, any structure X with which one can equip FHilb (the category of finite dimensional Hilbert spaces), and which allows a definition of unitary map that includes all identities and that coincides with the usual one on FHilb, and for which the full and faithful X-functors preserve and reflect unitary maps, is evil. Here is the technical argument again, as it seems to have been misunderstood. The forgetful functor F : FHilb -> FVect induces an equivalence, whose other half G : FVect -> FHilb requires a choice of inner product on each finite dimensional vector space. Define such a G in some way. Fix some X-structure on FVect. Let V be some non-trivial vector space, and let i and j be two different inner products on V. Then (V,i) and (V,j) are Hilbert spaces, so different objects of FHilb. Consider the morphism (in FHilb) f:(V,i) -> (V,j) given by f(v) = v. It is evidently not unitary. However, we have F(f) = id_V: V -> V, which is unitary, no matter the X structure that was chosen on FVect. So F does not reflect unitary maps. QED. Note that it is F, not G, that is causing problems. As remarked above, since G is full and faithful, it is possible to successfully reflect the dagger structure along G to FVect. This amounts to arbitrarily choosing some inner product on each vector space. But it won't be compatible with F. Also note that this argument is independent of the definition of the 2-cells of X-Cat. So it is even valid for some weaker definitions of "evil", for example, if one only requires F and G to lift to X-functors, rather than to an X-equivalence. I will argue that any structure X that claims to be a "weak" version of dagger structure should at least satisfy the conditions I listed as preconditions for the argument above. This is the basis for my claim that no construction such as Toby's or Dusko's can succeed in producing a non-evil equivalent of dagger structure. * the structure of "being equipped with a chosen Frobenius structure on each object" is evil, relative to monoidal categories. * the structure of "being equipped with an identity-on-objects covariant functor" is evil. * more generally, the structure of "being equipped with a chosen subcategory" is evil, unless the subcategory is required, as part of the structure, to contain all isomorphisms (in which case it is not evil). * poset-enrichment (with composition f o g monotone in f and g) is non-evil. * The following structure is evil: equip a category with a partial order on each hom-set, so that composition f o g is monotone in g, but not necessarily in f. Proof: Given such a structure on any category, define g:A->B to be "monotone" if (X,g) : (X,A) -> (X,B) is monotone for all X. Consider the category whose objects are partially-ordered sets, and whose morphisms are *all* functions (thanks to Fred Linton for this example). It can be equipped with the aforementioned structure, by giving the pointwise ordering to the functions in each hom-set. As a category, it is equivalent to Set. The rest of the argument proceeds as above for Hilbert spaces, with "monotone" instead of "unitary": take some non-trivial set with two different partial orders, then the identity is non-monotone, etc. The last example is almost an enrichment in Poset, but instead of the usual cartesian product on Poset, we have used another bifunctor on Poset, given by cartesian product P x Q of the underlying sets, with the non-standard order defined by (p,q) <= (p',q') iff p=p' and q<=q'. This operation is bifunctorial and associative, but not quite monoidal, because it lacks a right unit. More generally, taking "enrichments" in such almost-monoidal categories often yields evil structures. An analogous example works for the category of finite abelian groups and all set-theoretic functions. Happy new year to all, -- Peter [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* re: the definition of "evil" 2010-01-03 7:23 the definition of "evil" Peter Selinger @ 2010-01-03 17:10 ` Claudio Hermida 2010-01-03 17:53 ` John Baez ` (3 subsequent siblings) 4 siblings, 0 replies; 28+ messages in thread From: Claudio Hermida @ 2010-01-03 17:10 UTC (permalink / raw) To: categories Peter Selinger wrote: DEFINITION. Let X be some structure on categories. By this, I mean that there is a given 2-category called X-Cat, whose objects are called X-categories, whose morphisms are called X-functors, and whose 2-cells are called X-transformations, and for which there is a given 2-functor U to Cat, called the forgetful functor. We say that X is "transported along equivalences of categories" if the following holds. Given an X-category D', with underlying category D = U(D'), and a category C, and an equivalence (F,G,e,h) of categories D and C, where F: D -> C, G: C -> D, and e: FG -> id_C, h: GF -> id_D, it is then possible to find: (1) an X-category C' whose underlying category U(C') is isomorphic [not equivalent!] to C. Let c : U(C') -> C be the isomorphism (i.e., an invertible functor in Cat) with inverse c': C -> U(C'); (2) an X-equivalence of X-categories (F',G',e',h'), where F': D' -> C', G': C' -> D', e': F'G' -> id_C', and h': G'F' -> id_D' [the concept of equivalence makes sense in any 2-category]; such that (3) (U(F'), U(G'), U(e'), U(h')) = (cF, Gc', cec', h). Here, cF and Gc' denotes composition of functors, and cec' denotes whiskering. The structure X is called "evil" iff it is not transported along equivalences of categories. This finishes the definition. More informally, "transported along equivalences" therefore means that if D and C are equivalent, and D has an X-structure, then there is a way to equip C with an X-structure and to lift the original equivalence to an X-equivalence. There was a need for the isomorphism c in the definition, because the forgetful functor U : X-Cat -> Cat may not be strictly speaking surjective onto 0-cells in some real-life examples (and in any case, this forgetful functor may sometimes only be well-defined up to isomorphism). It is important that c is an isomorphism, rather than an equivalence, because else the definition becomes vacuous (and we are precisely interested in notions that are not well-defined up to equivalence). Also note that I didn't require the data (C',F',G',e',h') to be unique, not even up to equivalence in X-Cat. Although in practice, it will often be unique in this sense. So my definition allows for a given structure to be transported "in essentially more than one way" along a given equivalence. I am open to strengthening the definition to forbid this. Dear all, A quick pointer to a variation on this matter, which has already been around (I presented it at CT07). The nature of 2-categorical structures that transport along equivalences is nicely captured by the notion of Equ-iso-fibration: DEFINITION A 2-functor F:E → B is an Equ-iso-fibration if: - it admits cartesian liftings of (adjoint) equivalences and - every hom F(X,Y):E(X,Y) → B(FX,FY) admits cartesian lifitings of isomorphism 2-cells, and such liftings are preserved by precomposition (pointwise). Notice that a cartesian lifting of an adjoint equivalence is another such. The notions of cartesian liftings used here are those for 2-fibrations (as in the references below); they involve the expected 2-dimensional property for 1-cells. The liftings are strict. The most interesting example of such a structure is the forgetful functor of a 2-cateogory of pseudo-algebras V: Ps-T-Alg → K, for a 2-monad T on a 2-category K (or a pseudo-monad on a bicategory). They include all the known interesting examples of pseudo-structures, the classical such being monoidal categories. The morphisms in Ps-T-Alg are strong ones, preserving structure up to coherent isomorphism. The observation that pseudo-algebras do transport along equivalences is credited to Max Kelly in Power´s article below. I used this notion to capture the following universality of coherence: coherence for such pseudo-algebras (meaning that we can strictify every pseudo-algebra into a equivalent strict T-algebra) is equivalent to the statement THM: The inclusion 2-functor J: T-alg → Ps-T-alg makes V: Ps-T-alg → K the FREE Equ-iso-fibration over U:T-alg → K In other words, the passage from strict algebras (with their strict morphisms) to pseudo-algebras (and strong morphisms) is the universal way of achieving transportability along equivalences. Claudio References - C.Hermida, Some properties of Fib as a fibred 2-category, JPAA, *134 (1), 83-109, 1999* - C.Hermida, Descent on 2-fibrations and 2-regular 2-categories, Applied Cat Str, *12(5-6), 427--459, 2004* - A.J.Power, A general coherence result, [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* re: the definition of "evil" 2010-01-03 7:23 the definition of "evil" Peter Selinger 2010-01-03 17:10 ` Claudio Hermida @ 2010-01-03 17:53 ` John Baez 2010-01-04 17:14 ` Michael Shulman 2010-01-04 9:24 ` Urs Schreiber ` (2 subsequent siblings) 4 siblings, 1 reply; 28+ messages in thread From: John Baez @ 2010-01-03 17:53 UTC (permalink / raw) To: categories Dear Categorists - I'm glad Peter is trying to formulate a definition of structures that can be transported along equivalences, and I like the spirit of his definition, namely in terms of a "lifting property" where one has a 2-functor U: XCat -> Cat and one is trying to lift equivalences from Cat to XCat. But it makes me nervous when he says "isomorphic [not equivalent!]". Just as evil in category theory typically arises from definitions that impose equations between objects instead of specifying isomorphisms, evil in 2-category theory typically arises when we specify isomorphisms between objects instead of specifying equivalences. It would be sad, or at least intriguing, if the definition of "evil" was itself evil. Best, jb DEFINITION. Let X be some structure on categories. By this, I mean > that there is a given 2-category called X-Cat, whose objects are > called X-categories, whose morphisms are called X-functors, and whose > 2-cells are called X-transformations, and for which there is a given > 2-functor U to Cat, called the forgetful functor. > > We say that X is "transported along equivalences of categories" if the > following holds. Given an X-category D', with underlying category D = > U(D'), and a category C, and an equivalence (F,G,e,h) of categories D > and C, where F: D -> C, G: C -> D, and e: FG -> id_C, h: GF -> id_D, > it is then possible to find: > > (1) an X-category C' whose underlying category U(C') is isomorphic > [not equivalent!] to C. Let c : U(C') -> C be the isomorphism > (i.e., an invertible functor in Cat) with inverse c': C -> U(C'); > > (2) an X-equivalence of X-categories (F',G',e',h'), where > F': D' -> C', G': C' -> D', e': F'G' -> id_C', and h': G'F' -> id_D' > [the concept of equivalence makes sense in any 2-category]; > > such that > > (3) (U(F'), U(G'), U(e'), U(h')) = (cF, Gc', cec', h). > > Here, cF and Gc' denotes composition of functors, and cec' denotes > whiskering. > > The structure X is called "evil" iff it is not transported along > equivalences of categories. > > This finishes the definition. > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* re: the definition of "evil" 2010-01-03 17:53 ` John Baez @ 2010-01-04 17:14 ` Michael Shulman 0 siblings, 0 replies; 28+ messages in thread From: Michael Shulman @ 2010-01-04 17:14 UTC (permalink / raw) To: John Baez It looks to me like there are (at least) two different ideas of "evil" floating around. 1. A property or structure (on objects of a 2-category) is "non-evil" if it can be transported along equivalences. This is clearly a property of a forgetful 2-functor, which I agree that it makes the most sense to formulated as a lifting property for entire (adjoint) equivalences, including both functors and the unit and counit. (I'm surprised that Peter didn't require (F,G,e,h) and (F',G',e',h') to be *adjoint* equivalences in his definition; that seems to me likely to be the more correct notion.) Thus, whether a given structure is "evil" in this sense depends on what you are forgetting down to. Dagger structure is evil as structure on a category, but it is not evil as structure on a "category equipped with a distinguished subgroupoid." (Of course, a distinguished subgroupoid is evil as structure on a category.) I also think that this notion must necessarily be "2-evil" in the way that makes John sad, for anything at all is always "transportable along an equivalence up to equivalence"! In other words, if we are serious about avoiding evil, even at a higher-categorical level, then we shouldn't even be talking about evil in the first place. (-: (Of course, that also suggests that we probably can't construct, by purely non-2-evil (e.g. bicategorical) means, the 2-category of dagger categories from the 2-category of categories. But we can construct something pretty close, e.g. if we weaken "distinguished subgroupoid" to "faithful functor with groupoidal domain.") 2. A categorical structure is "evil" if it involves talking about equality of objects. For this sense, one has to be careful, because lots of notions in category theory involve equality of objects. In order to compose two morphisms f:A-->B and g:B-->C one has to know that the target of f is *equal* to the source of g. Likewise, to say that f:A-->B is an isomorphism, one has to say that there is an inverse g:B-->A whose source and target are *equal* to the target and source of f, respectively. However, as Toby says, there is a precise way to say that something is "not evil" in this sense while still admitting all of these "natural" constructions. Namely, we work in a dependent type theory with a type Ob of objects, and for each pair of objects x,y a dependent type Hom(x,y) of arrows, and stipulate that our theory contains an equality predicate only for the types Hom(x,y) and not for Ob. (Makkai's FOLDS, which Toby mentioned, is a generalization of this appropriate for higher-categorical structures.) The point is that specifying the source and target of an arrow should not be thought of as "talking about equality of objects," but rather as a *typing assertion*. What is forbidden is rather asking whether two already *given* objects are equal, not introducing an arrow whose source and target are ("equal to") some pair of already given objects. The notion of "dagger category" can be formulated in this dependently-typed language, as Toby has said, so it is *not* evil in this sense. This is related to the observation that dagger-categories are still "implementation-independent" relative to membership-based set theory, e.g. for the dagger-structure on Hilb it doesn't matter whether you define the real numbers as Cauchy sequences or Dedekind cuts. The relationship between these two notions is not immediately obvious to me. Clearly evil (1) does not imply evil (2), because of the example of dagger-categories. Does evil (2) imply evil (1)? Best, Mike John Baez wrote: > Dear Categorists - > > I'm glad Peter is trying to formulate a definition of structures that can be > transported along equivalences, and I like the spirit of his definition, > namely in terms of a "lifting property" where one has a 2-functor > > U: XCat -> Cat > > and one is trying to lift equivalences from Cat to XCat. > > But it makes me nervous when he says "isomorphic [not equivalent!]". Just > as evil in category theory typically arises from definitions that impose > equations between objects instead of specifying isomorphisms, evil in > 2-category theory typically arises when we specify isomorphisms between > objects instead of specifying equivalences. > > It would be sad, or at least intriguing, if the definition of "evil" was > itself evil. > > Best, > jb > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: the definition of "evil" 2010-01-03 7:23 the definition of "evil" Peter Selinger 2010-01-03 17:10 ` Claudio Hermida 2010-01-03 17:53 ` John Baez @ 2010-01-04 9:24 ` Urs Schreiber 2010-01-05 20:04 ` dagger not evil Joyal, André [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F565E@CAHIER.gst.uqam.ca> 4 siblings, 0 replies; 28+ messages in thread From: Urs Schreiber @ 2010-01-04 9:24 UTC (permalink / raw) To: Peter Selinger On Sun, Jan 3, 2010 at 8:23 AM, Peter Selinger <selinger@mathstat.dal.ca> wrote: > John Baez gave a pointer to a website containing a technical > definition of "evil": http://ncatlab.org/nlab/show/evil. > Unfortunately, this site only speaks of properties, > not structures. Fortunately, though, everybody can and is invited add to this site! So eventually it may speak also of structures -- and much more. This site was created for exactly the kind of situation we have here: we have an intersting technical discussion on a mailing list or similar forum. After a while it will end and a bunch of scattered messages will remain in the archives of the mailing list. The important insight gained or exhibited in the discussion will be non-trivial to find and deduce from the archived discussion threads. It'll be a shame if all the valuable insight of various participants, all the energy they invested into composing these messages, find no more focused and polished incarnation than that. The above site is meant to provide a place where results of such discussion is collected in a more useful form. I am hoping that eventually the upshot of the discussion on "evil" had here on the list will eventually find a nice incarnation on that site. Everyone can help to make that come true. Just hit the "edit" button at the bottom of the page: http://ncatlab.org/nlab/edit/evil Best, Urs [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* dagger not evil 2010-01-03 7:23 the definition of "evil" Peter Selinger ` (2 preceding siblings ...) 2010-01-04 9:24 ` Urs Schreiber @ 2010-01-05 20:04 ` Joyal, André 2010-01-06 8:40 ` Toby Bartels [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5672@CAHIER.gst.uqam.ca> [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F565E@CAHIER.gst.uqam.ca> 4 siblings, 2 replies; 28+ messages in thread From: Joyal, André @ 2010-01-05 20:04 UTC (permalink / raw) To: Peter Selinger, categories Dear Peter and all, I cannot resist adding my grain of salt to the ongoing discussion on dagger categories. I will take the point of view of a homotopy theorist. Recall that the category of small categories Cat admits a "natural" model structure (called the "folk" model structure for the wrong reason by the folks). The category of small dagger categories DCat also admits a "natural" model structure. A dagger functor f:A-->B is a weak equivalence iff it is fully faithful and unitary surjective (this last condition means that every object of B is unitary isomorphic to an object in the image of the functor f). The cofibrations and the trivial fibrations are as in Cat. A fibrations is a unitary isofibration (a map having the lifting property for unitary isomorphisms). The forgetful functor DCat ---> Cat is a right adjoint but it is not a right Quillen functor with respect to the natural model structures on these categories. In other words the forgetful functor DCat ---> Cat is wrong. This may explains why a dagger category cannot be regarded as a category equipped a homotopy invariant structure. But I claim that the notion of dagger category is perfectly reasonable from an homotopy theoretic point of view. This is because the model category DCat is combinatorial. It follows, by a general result, that the notion of of dagger category is homotopy essentially algebraic There a homotopy limit sketch whose category of models (in spaces) is Quillen equivalent to the model category DCat. This is true also for the model category Cat. There should be a notion of dagger quasi-category. A dagger simplicial set can be defined to be a simplicial set X equipped with an involutive isomorphism dag:X-->X^o which is the identity on 0-cells. The category of dagger simplicial sets (and dagger preserving maps) is the category of presheaves on the category whose objects are the ordinals [n] but where the maps [m]-->[n] are order reversing or preserving. Finally, the (homotopy) trace of a category (resp. quasi-category) has the structure of a cyclic set in the sense of Connes. I conjecture that the (homotopy) trace of a dagger category (resp. dagger quasi-category) has the structure of a dihedral set in the sense of Fiedorowicz and Loday. Happy New Year to all! andré PS: I will be quiet during the next few weeks. -------- Message d'origine-------- De: categories@mta.ca de la part de Peter Selinger Date: dim. 03/01/2010 02:23 À: Categories List Objet : categories: the definition of "evil" Dear all, sorry for sending yet another message on the topic of "evil" structures on categories. After some interesting private replies, as well as Dusko's latest message (which should have appeared on the list by the time you read this), I noticed that not everyone is agreeing on the technical meaning of the term "evil". I will therefore attempt to state a more precise technical definition of the term as I have used it. Perhaps 2-category theorists already have another name for this. The information definition I had used is that a structure is "evil" if it does not "transport along equivalences of categories". I thought it was reasonably obvious what was meant by "transport along", but there is actually a lot of variation in what people understand this phrase to mean. John Baez gave a pointer to a website containing a technical definition of "evil": http://ncatlab.org/nlab/show/evil. Unfortunately, this site only speaks of properties, not structures. It is easy to state what it means for a property of categories to be transported along equivalences: namely, if C has the property, and C and C' are equivalent, then C' has the property. Structures are more tricky. .... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: dagger not evil 2010-01-05 20:04 ` dagger not evil Joyal, André @ 2010-01-06 8:40 ` Toby Bartels 2010-01-07 5:50 ` Peter Selinger 2010-01-08 0:45 ` Joyal, André [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5672@CAHIER.gst.uqam.ca> 1 sibling, 2 replies; 28+ messages in thread From: Toby Bartels @ 2010-01-06 8:40 UTC (permalink / raw) To: categories André Joyal wrote in small part: >In other words the forgetful functor DCat ---> Cat is wrong. This reminds me of the fact that the obvious forgetful functor Ban -> Set or Hilb -> Set (where now Hilb is just a category, with short linear maps as morphisms, not a dagger category) is wrong. That is, the wrong forgetful functor takes the set of points, whereas the right one takes the set of points in the closed unit ball. (Of course, both functors exist, but the right one is representable.) While the obvious forgetful functor DCat -> Cat is wrong, is there a right one? In particular, we have a functor Cat -> Grpd that takes the lluf subcategory (LS) of invertible morphisms and the functor DCat -> Grpd that takes the LS of unitary morphisms; is there a functor DCat -> Cat that completes a commutative triangle? Less rigorously but more concretely, can we start with Hilb+ (the dagger category with all bounded linear maps as morphisms) and systematically derive the class of short linear maps, much as we can systematically derive the class of unitary maps? Offhand, I don't see how to do this. (Note: "short" = "Lipschitz with Lipschitz constant at most 1", so "short linear" = "bounded linear with norm at most 1".) --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: dagger not evil 2010-01-06 8:40 ` Toby Bartels @ 2010-01-07 5:50 ` Peter Selinger 2010-01-08 0:45 ` Joyal, André 1 sibling, 0 replies; 28+ messages in thread From: Peter Selinger @ 2010-01-07 5:50 UTC (permalink / raw) To: toby+categories Toby Bartels wrote: > > Andr=E9 Joyal wrote in small part: > > >In other words the forgetful functor DCat ---> Cat is wrong. > > This reminds me of the fact that the obvious forgetful functor > Ban -> Set or Hilb -> Set (where now Hilb is just a category, > with short linear maps as morphisms, not a dagger category) is wrong. > That is, the wrong forgetful functor takes the set of points, > whereas the right one takes the set of points in the closed unit ball. > (Of course, both functors exist, but the right one is representable.) > > While the obvious forgetful functor DCat -> Cat is wrong, > is there a right one? In particular, we have a functor > Cat -> Grpd that takes the lluf subcategory (LS) of invertible morphisms > and the functor DCat -> Grpd that takes the LS of unitary morphisms; > is there a functor DCat -> Cat that completes a commutative triangle? There is, because Cat -> Grpd is right invertible, but that is probably not the functor you had in mind. > Less rigorously but more concretely, can we start with Hilb+ > (the dagger category with all bounded linear maps as morphisms) > and systematically derive the class of short linear maps, > much as we can systematically derive the class of unitary maps? > Offhand, I don't see how to do this. > > (Note: "short" = "Lipschitz with Lipschitz constant at most 1", > so "short linear" = "bounded linear with norm at most 1".) > > --Toby As far as I know, you can't do this with a dagger structure alone; however, if you regard Hilb+ as a dagger category with dagger biproducts, then the short linear maps are definable as those maps f: A -> B satisfying (1) there exists some g: A -> C such that (f^dagger o f) + (g^dagger o g) = id, or equivalently, (2) there exists some h: D -> B such that (f o f^dagger) + (h o h^dagger) = id. In Hilb+, conditions (1) and (2) are equivalent for a given f. In a general dagger category with dagger biproducts, they are not equivalent (as the example Rel shows), and one should in general define a "short linear" morphism to be an f that satisfies both (1) and (2). The always form a dagger subcategory. In general, invertible + short linear, in this sense, does not imply unitary. A counterexample is chosen-basis vector spaces over Z_2 (with dot product as inner product), where all maps are short linear, but not all invertible maps are unitary. However, if one further assumes that the category satisfies the following strictness condition: (3) 1 + (g o g^dagger) = 1 implies g = 0, then invertible + short linear implies unitary. So something like your "right" forgetful functor DCat' -> Cat can be defined, where DCat' is DCat equipped with these additional hypotheses. I don't know whether there is a more organic definition that works in greater generality. -- Peter [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: dagger not evil 2010-01-06 8:40 ` Toby Bartels 2010-01-07 5:50 ` Peter Selinger @ 2010-01-08 0:45 ` Joyal, André 1 sibling, 0 replies; 28+ messages in thread From: Joyal, André @ 2010-01-08 0:45 UTC (permalink / raw) To: Toby Bartels, categories Dear Toby You wrote: >While the obvious forgetful functor DCat -> Cat is wrong, >is there a right one? In particular, we have a functor >Cat -> Grpd that takes the lluf subcategory (LS) of invertible morphisms >and the functor DCat -> Grpd that takes the LS of unitary morphisms; >is there a functor DCat -> Cat that completes a commutative triangle? I will try answer your question, but my answer is wonkish. First, a category can be regarded as a (simplicial) diagram of groupoids. More precisely, every category C has a "Rezk nerve" RN(C) which is a simplicial object in the category of groupoids. By definition, we have RN(C)_n=IsoNat([n],C) for every non-negative integer n, where IsoNat([n],C) denotes the groupoid of natural isomorphisms in the category of functors [n]-->C. The nerve RN(C) was first introduced by Charles Rezk in http://arxiv.org/abs/math/9811037 The functor RN has very nice properties. It embeds the category Cat in the category of simplicial groupoids Simp(Grpd). The embedding respects (ie preserves and reflects) the equivalences defined on both sides, where a map of simplicial groupoids f:X-->Y is defined to be an equivalence if it is an equivalence levelwise. It can be proved that RN is a right Quillen functor with respect to the natural model structure on Cat and with respect to the Reedy model structure on Simp(Grpd). A dagger category can also be regarded as a (dagger simplicial) diagram of groupoids. More precisely, every dagger category C has a "unitary nerve" UN(C) which is a dagger simplicial object in the category of groupoids. By definition, we have UN(C)_n=UIsoNat([n],C) for every non-negative integer n, where UIsoNat([n],C) denotes the groupoid of unitary natural isomorphisms in the category of functors [n]-->C. The functor UN embeds the category DCat in the category of dagger simplicial groupoids DSimp(Grpd). The embedding respects the equivalences defined on both sides, where a map of dagger simplicial groupoids f:X-->Y is defined to be an equivalence if it is an equivalence levelwise. You wrote: >Less rigorously but more concretely, can we start with Hilb+ >(the dagger category with all bounded linear maps as morphisms) >and systematically derive the class of short linear maps, >much as we can systematically derive the class of unitary maps? >Offhand, I don't see how to do this. I am afraid I dont have an answer to this question. But I will think about the problem. Best, André [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F5672@CAHIER.gst.uqam.ca>]
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F5673@CAHIER.gst.uqam.ca>]
* equality is beautiful [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5673@CAHIER.gst.uqam.ca> @ 2010-01-09 3:29 ` Joyal, André 2010-01-10 17:17 ` Steve Vickers ` (3 more replies) 0 siblings, 4 replies; 28+ messages in thread From: Joyal, André @ 2010-01-09 3:29 UTC (permalink / raw) To: categories Dear All Many people seem to distrust the equality relation between the objects of a (large) category. Is this a philosophical conundrum or a mathematical problem? Can we define a notion of (large) category without supposing that its (large) set of objects has a diagonal? Best, André [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality is beautiful 2010-01-09 3:29 ` equality is beautiful Joyal, André @ 2010-01-10 17:17 ` Steve Vickers [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5677@CAHIER.gst.uqam.ca> 2010-01-10 19:54 ` equality is beautiful Vaughan Pratt ` (2 subsequent siblings) 3 siblings, 1 reply; 28+ messages in thread From: Steve Vickers @ 2010-01-10 17:17 UTC (permalink / raw) To: Joyal, André, categories On 9 Jan 2010, at 03:29, Joyal, André wrote: > Dear All > > Many people seem to distrust the equality > relation between the objects of a (large) category. > Is this a philosophical conundrum or a mathematical problem? > > Can we define a notion of (large) category without supposing > that its (large) set of objects has a diagonal Dear Andre, Can I explore this with regard to topologies? Suppose we compare FinSet with Set, defining FinSet very small with N for its object space. The object diagonal N -> NxN is an open inclusion. Now look at Set. The natural topology on the class of sets, as the Ind-completion of FinSet, is the one whose sheaves are given by the object classifier. Thus continuous maps from it are functorial and preserve filtered colimits (the categorical analogue of Scott continuity). (This introduces a confusing issue. Functors from the category Set are already determined by their object maps. But it is a special category in which the morphism space is the comma object got from two copies of the identity map on the object space - we are using the fact that the category of spaces is actually a 2-category, using the specialization morphisms. FinSet was certainly not of this kind.) Now the object diagonal is not even an inclusion, since it is not full. I would speculate, by analogy with what I know for ideal completions, that it is essential but not locally connected. I don't really know what to make of this, but it does seem that there are topological distinctions to be made between the two categories based on object equality. Now let me wonder about classifying toposes. I love using them (as I did above), but they always seem slightly fuzzy because they are really defined only up to equivalence. So I certainly would distrust the object equality. I think the discussion becomes slightly sharper in terms of arithmetic universes (as mentioned by Paul Taylor) instead of toposes. Given a base AU A0, there are two obvious places to look for an object classifier (representing the class of sets) a la Grothendieck topos theory. First, there is A0[U], the AU freely generated over A0 by an object U. This can be constructed by universal algebra, and then is a classifying A0-AU (for the theory with one sort and no predicates, functions or axioms) characterized up to isomorphism with respect to strict A0-AU homomorphisms. However, its object equality depends rather delicately on the precise structure used to characterized AUs. For example, I suspect it will differ according as AUs are taken to have canonical pullbacks or canonical binary products and equalizers. On the other hand, sheaf theory would suggest using the category Presh (FinSet^op) of internal diagrams over the internal FinSet in A0. I conjecture that this (is an AU and) is equivalent but not isomorphic to A0[U]. Hence there are issues of object equality when one compares them. (Milly Maietti and I are looking at "subspaces" in this AU setting, and again are having to be rather careful about equality and the distinction between strict and non-strict AU homomorphisms.) A further issue, seen in AUs but not toposes, is that A0[U] can be internalized in A0, as the internal AU in A0 freely generated by one object. The comparison with the external A0[U] will presumably raise truth v. proof issues similar to those that you have already investigated for the initial AU and Goedel's Theorem. To summarize: (1) Granted the existence of the object diagonals, they may still have different topological characteristics for different kinds of categories. (2) A universal characterization (such as for classifying toposes) that is only up to equivalence will make it difficult to rely on object equality. (3) In arithmetic universes we can perhaps (allowing for the fact that the theory is not fully developed yet) see situations where the object equality definitely exists, but is sensitive to inessential differences. Best regards, Steve Vickers. [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F5677@CAHIER.gst.uqam.ca>]
* Re: A challenge to all [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5677@CAHIER.gst.uqam.ca> @ 2010-01-12 10:25 ` Steve Vickers 2010-01-12 16:24 ` Joyal, André 1 sibling, 0 replies; 28+ messages in thread From: Steve Vickers @ 2010-01-12 10:25 UTC (permalink / raw) To: Joyal André, categories Dear Andre, How would you deal with composition? The standard account of composability - defined by equality between a domain and a codomain - does seem to presuppose a notion of object equality. Normally for categories internal in C one therefore takes C to have pullbacks. Are there obvious ways to generalize that to monoidal C? Or are you thinking you might want to relax that standard account, perhaps even losing the well defined domain and codomain? I'm getting a picture of things like "categories" of smooth curves, where two curves are composable only if the end of one has an open overlap with the start of the other. But then "objects" are more nebulous. Regards, Steve Vickers. Joyal wrote: > ... > I cannot imagine a category without an equality relation between the objects. > ... > > 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 a set S is > defined by the diagonal map S-->S times S. > The diagonal gives a set the structure of a cocommutative coalgebra, > where the tensor product is the cartesian product. > The objects of a general symmetric monoidal category have no > coalgebra structure in general. > > The test: Is it possible to define a notion of category internal to > a symmetric monoidal category without using a coalgebra structure > on the object of objects? [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* A challenge to all [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5677@CAHIER.gst.uqam.ca> 2010-01-12 10:25 ` A challenge to all Steve Vickers @ 2010-01-12 16:24 ` Joyal, André 2010-01-13 0:03 ` David Roberts ` (5 more replies) 1 sibling, 6 replies; 28+ messages in thread From: Joyal, André @ 2010-01-12 16:24 UTC (permalink / raw) To: categories 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-12 16:24 ` Joyal, André @ 2010-01-13 0:03 ` David Roberts 2010-01-13 0:47 ` burroni ` (4 subsequent siblings) 5 siblings, 0 replies; 28+ messages in thread From: David Roberts @ 2010-01-13 0:03 UTC (permalink / raw) To: Joyal, André, categories 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-12 16:24 ` Joyal, André 2010-01-13 0:03 ` David Roberts @ 2010-01-13 0:47 ` burroni [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5688@CAHIER.gst.uqam.ca> 2010-01-13 1:02 ` Jeff Egger ` (3 subsequent siblings) 5 siblings, 1 reply; 28+ messages in thread From: burroni @ 2010-01-13 0:47 UTC (permalink / raw) To: Joyal, André; +Cc: categories Dear André, > 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? This is possible with this conception : A "monoid" in a monoidal category is what Benabou call *monad* in his paper on bicatégories. The more general notion of "category", in the same vein, is the notion of *polyad* (in the same paper of Benabou --- apologize me : I have not the reference whith me): the objets are given externally. I don't know if my remark you satisfie, I think not (you have had certainly yourself this idea), but, for me, the moral of this fact seems to say that the equality of objets have something of intrinsically very different of morphisms. (This meets perhaps the ideas of Bob Paré on index categories) I am convided of this (If I have the occasion, I will explain this). Best, Albert "Joyal, André" <joyal.andre@uqam.ca> a écrit : > 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. ... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F5688@CAHIER.gst.uqam.ca>]
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F568B@CAHIER.gst.uqam.ca>]
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F568D@CAHIER.gst.uqam.ca>]
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F568F@CAHIER.gst.uqam.ca>]
* Re: A challenge to all [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F568F@CAHIER.gst.uqam.ca> @ 2010-01-15 19:33 ` Joyal, André 2010-01-20 5:52 ` Michael Shulman 0 siblings, 1 reply; 28+ messages in thread From: Joyal, André @ 2010-01-15 19:33 UTC (permalink / raw) To: categories 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-15 19:33 ` Joyal, André @ 2010-01-20 5:52 ` Michael Shulman 0 siblings, 0 replies; 28+ messages in thread From: Michael Shulman @ 2010-01-20 5:52 UTC (permalink / raw) To: joyal.andre, categories 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-12 16:24 ` Joyal, André 2010-01-13 0:03 ` David Roberts 2010-01-13 0:47 ` burroni @ 2010-01-13 1:02 ` Jeff Egger 2010-01-13 2:28 ` Michael Shulman ` (2 subsequent siblings) 5 siblings, 0 replies; 28+ messages in thread From: Jeff Egger @ 2010-01-13 1:02 UTC (permalink / raw) To: Joyal, André, categories 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-12 16:24 ` Joyal, André ` (2 preceding siblings ...) 2010-01-13 1:02 ` Jeff Egger @ 2010-01-13 2:28 ` Michael Shulman 2010-01-13 20:53 ` equality Dusko Pavlovic 2010-01-13 23:43 ` A challenge to all Peter LeFanu Lumsdaine 2010-01-15 19:40 ` Thomas Streicher 5 siblings, 1 reply; 28+ messages in thread From: Michael Shulman @ 2010-01-13 2:28 UTC (permalink / raw) To: joyal.andre, categories Dear Andre, You are absolutely right that the equality relation is inseparable from the idea of a set. What is being proposed, however, is that a category doesn't need to have a *set* of objects. In fact, the objects of a category don't need to form an object of any category at all, so I think your proposed test is misguided. The formulation of category theory in dependent type theory which Richard, Toby, I, and others are proposing makes perfect sense without any equality predicate for the objects. Best, Mike Joyal wrote: > 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality 2010-01-13 2:28 ` Michael Shulman @ 2010-01-13 20:53 ` Dusko Pavlovic 2010-01-14 14:23 ` equality Colin McLarty 0 siblings, 1 reply; 28+ messages in thread From: Dusko Pavlovic @ 2010-01-13 20:53 UTC (permalink / raw) To: Categories 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/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality 2010-01-13 20:53 ` equality Dusko Pavlovic @ 2010-01-14 14:23 ` Colin McLarty 0 siblings, 0 replies; 28+ messages in thread From: Colin McLarty @ 2010-01-14 14:23 UTC (permalink / raw) To: Categories 2010/1/13 Dusko Pavlovic <dusko@kestrel.edu>: > 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. Is there a published account of this, preferably on the web? Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-12 16:24 ` Joyal, André ` (3 preceding siblings ...) 2010-01-13 2:28 ` Michael Shulman @ 2010-01-13 23:43 ` Peter LeFanu Lumsdaine 2010-01-15 19:40 ` Thomas Streicher 5 siblings, 0 replies; 28+ messages in thread From: Peter LeFanu Lumsdaine @ 2010-01-13 23:43 UTC (permalink / raw) To: categories [-- Warning: decoded text below may be mangled, UTF-8 assumed --] [-- Attachment #1: Type: text/plain, Size: 1861 bytes --] On 12 Jan 2010, at 11:24, André Joyal wrote: > > 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. Your test is addressed in more detail in other replies, but to pull out one idea that comes up in several: --- the diagonal embedding is not always the equality relation. I don't think I've seen anyone propose how to define a notion of category in the absence of some kind of diagonal embedding, but Francois Larmarche and others nicely describe various situations (topological spaces, higher categories, intensional type theories...) where the diagonal embedding isn't a well-behaved equality relation, and certainly isn't the one we want. For example, one such situation is explored by Gambino and Garner in "The identity type weak factorisation system". Roughly: you can have logical categories where a predicate S ---> A on an object means not a monic, but rather a _fibration_, for some wfs (or similar structure). The diagonal embedding A >--> AxA may fail to be a fibration; then the equality predicate E comes from the factorisation of this map as a left map (think "cofibrant weak equivalence") followed by a fibration: A >--> E ---> AxA. The groupoid case is a nice example of this situation, as described in that paper. So the notions of "diagonal embedding" and "equality relation" can certainly diverge (even in situations where both exist); and I think the insight of Mike Shulman and co. here is that "diagonal embedding" is the one which (if either) is wanted in the definition of a category. -p. -- Peter LeFanu Lumsdaine Carnegie Mellon University [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: A challenge to all 2010-01-12 16:24 ` Joyal, André ` (4 preceding siblings ...) 2010-01-13 23:43 ` A challenge to all Peter LeFanu Lumsdaine @ 2010-01-15 19:40 ` Thomas Streicher 5 siblings, 0 replies; 28+ messages in thread From: Thomas Streicher @ 2010-01-15 19:40 UTC (permalink / raw) To: categories It is, of course, not impossible that big categories come with an equality of objects, e.g. if one works relative to a base category Set which is a model of ZFC with sufficiently many Grothendieck universes. A very strong such extension is by the axiom that every set appears as element of some Grothendieck universe. For most purposes 2 or 3 nested Grothendieck universes suffice. This may seem strong but is weaker than some of the large cardinal axioms considered by set theorists. As I understand big categories without equality show up necessarily when one works relative to bases much weaker then Set like elementary toposes or "predicative" versions thereof. The reason is that when fibring the base BB over itself via the fundamental (or codomain) fibration P_BB : BP^2 -> BB this fibration is not split. A possibility is to extend BB to the category Idl(BB) (as done in work on Algebraic Set Theory by Awodey et.al. following an advice of Joyal) which provides a model for an intuitionistic theory of classes. One may describe Idl(BB) as the full subcategory of Sh(BB) (sheaves over BB w.r.t. the finite cover topology) such that equality is definable in the sense of Benabou. Of course, not all split fibrations over BB can be obtained as externalisations of categories internal to Idl(BB). But P_BB is equivalent to such a fibration. Of course, this approach just mimicks the classical set theoretic approach which many people dislike. Type theory was mentioned as a possible alternative because via dependent types one can formulate the structure of a category in a most natural way. But if one works in extensional type theory (i.e. "judgemental" and "propositional" equality identified) there is also no problem with equality. Actually extensional type theory with a cumulative sequence of universes is an attractive alternative for those who dislike a set like approach. The current official version of type theory is intensional type theory with a weak "judgemental" equality and a stronger "propositional" equality. The distinguishing feature of intensional type theory is that type checking is decidable (which is not the case for extensional type theory). Living with two equalities doesn't really make one's life easier but it's a price to be paid for having the nice (and practically most useful) property of decidable type checking. But there is a way of turning this defect into an advantage. This was observed in the mid 90s by Martin Hofmann and myself when we considered the model where types are groupoids and families of types are (split) fibrations of groupoids. Of course, the diagonal on a groupoid will be a fibration if and only if the groupoid is discrete. Therefore, we interpreted the equality on a groupoid A as the fibration corresponding to Hom_A(-,-), i.e. equality as being isomorphic. Thus there are different ways of being equal because there are in general different ways of being isomorphic. (Finding models of type theory where there are different ways of being propositionally equal was our main concern in this paper). We also discussed in this paper (Sect.5.4) that one might add axioms claiming for elements of some universe that being equal is equivalent to being isomorphic. In Sect.5.5 of this paper we sketched how to exploit such an extended type theory for formalizing category theory in such a way that equality of objects is equivalent to them being isomorphic. There are 2 defects of the groupoid model, namely that it is 2-dimensional and that it is strong and not weak. In his PhD Thesis Michael Warren has shown that strict \omega-groupoids do form a model of intensional type theory. In a talk some time ago (2006) I suggested to model intensional type theory in the topos SSet of simplicial sets interpreting types as Kan complexes and families of types as Kan fibrations. Recently, in Nov. 2009 V.Voevodsky gave a talk in Munich on "Homotopical Lambda Calculus" where he presented such a setting as a model for type theory where equality can be understood as being isomorphic. The latter was precisely his motivation for doing it. He said he will write up this work in the near future. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality is beautiful 2010-01-09 3:29 ` equality is beautiful Joyal, André 2010-01-10 17:17 ` Steve Vickers @ 2010-01-10 19:54 ` Vaughan Pratt 2010-01-11 2:26 ` Richard Garner 2010-01-13 11:53 ` lamarche 3 siblings, 0 replies; 28+ messages in thread From: Vaughan Pratt @ 2010-01-10 19:54 UTC (permalink / raw) To: categories Joyal wrote: > Many people seem to distrust the equality > relation between the objects of a (large) category. > Is this a philosophical conundrum or a mathematical problem? I don't even trust it for the *-autonomous category with two objects and three morphisms. This is the basis for the classical notion of truth as normally understood when not trying to parse the sentences of constructive mathematicians. Some dark night someone could sneak into the basement where the foundations of mathematics are stored and switch true and false around, and in the morning we'd all wake up talking Doublespeak without even realizing it. Are you suggesting we should trust the equality relation between the objects of that category? Useful categories don't come much smaller. It can't be a question of size because the free Heyting algebra on one generator is infinite yet it doesn't have this structural ambiguity of classical logic: we can trust its equality relation because we can tell which element is the generator even if the arrows are accidentally flipped---it's a sort of error-detection feature of that Heyting algebra not possessed by any Boolean algebra. This is a reason to prefer intuitionistic logic over classical (not one I'd use myself mind you). Best, Vaughan [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality is beautiful 2010-01-09 3:29 ` equality is beautiful Joyal, André 2010-01-10 17:17 ` Steve Vickers 2010-01-10 19:54 ` equality is beautiful Vaughan Pratt @ 2010-01-11 2:26 ` Richard Garner 2010-01-13 11:53 ` lamarche 3 siblings, 0 replies; 28+ messages in thread From: Richard Garner @ 2010-01-11 2:26 UTC (permalink / raw) To: Joyal, André; +Cc: categories Dear André > Many people seem to distrust the equality > relation between the objects of a (large) category. > Is this a philosophical conundrum or a mathematical problem? > > Can we define a notion of (large) category without supposing > that its (large) set of objects has a diagonal? Yes, this is precisely what one does in formalising category theory in an (intensional) dependent type theory. (Mike Shulman has alluded to this in a previous message to this list.) Since in such a type theory one does not have quotients of equivalence relations, one typically works not with raw types but with setoids (=types equipped with an equivalence relation in the internal logic). The category of such setoids is well behaved---at least an LCC pretopos---but the notion of internal category in this pretopos is generally not what one is interested in. Instead one takes a category internal to the type theory to be given by a type of objects O, together with an OxO indexed family of hom-setoids O(x,y), composition and identities which are maps of setoids, and associativity and unitality witnessed by elements of the hom-setoid equality. In this setting, we may not talk of equality of objects (since O is not a setoid but only a type) but may talk of the equality of any pair of parallel arrows. This notion is due to Peter Aczel and there is a fairly extensive development of it in the proof assistant Coq by Gérard Huet and Amokrane Saïbi. Some consequences of the definition are, e.g., that the collection of all small categories does no longer forms a category, but only a bicategory (since one cannot speak of equality of functors, since this would require equality of objects in the codomain). Some work on this has been done by Olov Wilander. Since the category of sets is a model of extensional, and so also intensional, type theory, one may interpret what the above means in this context to obtain, within a classical (or at least impredicative) metatheory, a notion of category meeting your requirements. In fact such non-standard categories may be seen as special kinds of tricategory (in the usual sense). Indeed, in the set-based model of type theory, a setoid is given by a set X; for each pair of elements x,y in X, a further set X(x,y); and arrows of composition X(y,z) x X(x,y)-->X(x,z), inverse X(x,y)-->X(y,x) and identity 1-->X(x,x) subject to no axioms. But this is precisely to give a bigroupoid which is locally chaotic, in the sense that between any two parallel 1-cells, there is a unique 2-cell. [From a constructive perspective, not every such bigroupoid would be "OK". The constructively valid ones would be the cofibrant ones, since these may be inductively generated.] From this it follows without difficulty that a category in the constructive sense is precisely a tricategory (in the sense of Gordon-Power-Street) whose every hom-bicategory is a locally chaotic bigroupoid. The use of these non-standard categories is pertinent with regard to Bill Lawvere's comments on the distinction between presentations and the things (theories) that they present. There is a model structure on the category FPCat of small categories with chosen finite products and strict product-preserving maps whose cofibrant objects are, up to retracts, the (many-sorted) Lawvere theories. One may define, in a similar way, a category FPCat' whose objects are non-standard categories with finite products, and whose morphisms are strict structure-preserving maps: and on this there is a model structure (or at least the cofibration-trivial fibration half of a model structure) whose cofibrant objects are "equational presentations of Lawvere theories": one has not only the sorts, and the generating operations, but also the generating equalities between composite operations. There is an adjunction between FPCat and FPCat' which is the left-hand of the two adjunctions described by Bill. Richard [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality is beautiful 2010-01-09 3:29 ` equality is beautiful Joyal, André ` (2 preceding siblings ...) 2010-01-11 2:26 ` Richard Garner @ 2010-01-13 11:53 ` lamarche 2010-01-13 21:29 ` Michael Shulman 3 siblings, 1 reply; 28+ messages in thread From: lamarche @ 2010-01-13 11:53 UTC (permalink / raw) To: André, categories I have been thinking on how to get this post right for a few days, taking my time, but André's recent post > Can we define a notion of (large) category without supposing > that its (large) set of objects has a diagonal? prompted me to send this... perhaps prematurely. One can do a lot of mathematics without using the equality predicate. The necessary technology (dependent types) has been around for a long time, and the foundations of category theory is a natural domain of application for it. Richard Gardner has already said something to that effect, but I want to stress that point and try to sell it to the less syntactically inclined among us. In dependent types you still need a very limited form of equality, to be able to compare syntactic objects. After all, if you make a complex syntactic construction A, you have to be able to make copies of it and reuse it elsewhere at several places, and you want your theory to take account of this. And, more importantly, if you start with A and elaborate on it twice, getting two syntactic objects S(A), T(A), it is natural to be able to assert that the two results are equal, because some times they will. The standard example of this is beta- reduction in the lambda calculus. But as I said this is a very limited form of equality, since a true equality predicate would allow you to assert if two *arbitrary* objects are equal. The syntax of dependent types is rather heavy, but once you know how to interpret it in a category C it is very intuitive. To get started all you need is a class of maps in C which is stable under pullbacks. and then you interpret such a special map A: \bar A ----> X as a dependent type x: X |- A(x) I.e., if types in say, simple lamda calculus can be interpreted as sets (or spaces), then dependent types can be interpreted as an indexed family of sets, depending on another set. The operation of pullback is substitution of a term in a type. That is, if an aribtrary map B ----> A in C is thought of as a term, in the usual Lawvere-Lambek sense b:B |- f(b) then the pullbakck of A by f represents the type b:B |- A(f(b)) Most of the people on this list are already very familiar with this *intuition*, which has been used countless times since the mid-fifties starting in algebraic topology, then algebraic geometry, then categorical foundations (I mention in particular the idea of using such a class of pullback-stable maps in a topos-like category as a notion of smallness, introduced (i think) by Bénabou and used extensively by Joyal-Moerdijk in a monograph, and lots of other people who are reading this list. But the point of this post is that I think there is still the need to stress that there is a *formal syntax* which corresponds to this intuition, although many people on this list are already aware of this. We have learned to "reason intuititionisticallty" in a topos, and intuitionistic predicate theory was a real help in doing so... the same goes here: we can learn to reason in situations where the equality predicate is limited to special types, the *discrete* ones. And this point it is easy to illustrate. Let us go back to our category C. People have known for a long time that all you need to do to define internal categories in C is to require that C have pullbacks. But actually the natural requirements are even weaker: all you need is that C have a special class of maps closed under pullbacks (and that includes all isos). For simplicity today I will also require a terminal object. As I already said you think of these maps as indexed families. So suppose X is chosen to be the object of objects of an internal category. You want a family of morphisms. I.e., given the usual span d_0 : X <----- H -----> X d_1 it is now required that X ---> 1 be one of these special maps (so that "X is an independent type") and both H ----> X are required to be special maps too. It is easy to see then that <d_0, d_1> : H ----- > X x X is also a special map. We can now say that these two maps define an indexed family: x: X, y: X |- Hom(x,y) Now look at how composition is presented: x,y,z : X , h: Hom(x,y), k: Hom(y,z) |- k o h : Hom(x,z) This is intepreted in C via very mechanical constructions, which will give the interpretation of composition as the usual map, with the usual pullback as source and which obeys the usual commutation requirements. Notice that the syntax we used *does not need an equality predicate to assert that dom(k) = cod(h)* The same goes with the identity map x: X |- Id(x) : Hom(x,x) But now look at associativity: x,y,z,w: X, h: Hom(x,y), k: Hom(y,z), g: Hom(z,w) |- g o (k o h) = (g o k ) o h Here you need a real equality predicate. That means that the sets in the indexed family (Hom(x,y))_x,y are required to be *discrete sets*, i.e., that the diagonal is required to be a predicate. There is some leeway on how to define predicates, but a natural way to do it is to say that predicates are (represented by) special maps that are monos. Thus, to be back to the "small is beautiful" track, a first approximation of Large/Small goes (very roughly) space/discrete space. Several years ago i circulated a manuscript where I was trying to formalize foundations of category theory by specializing the space/ discrete space duality above to groupoid/discrete groupoid. I was using fibrations of groupoids over a base category (potentially a topos) as a reference model. In other words, I was trying to find the kind of elementary toposes you would get if you subsituted fibrations (and stacks) of groupoids for presheaves (and sheaves). I made some very interesting observations, but one problem I hit was that these categories are only bi-cartesian closed, not cartesian closed, and that really stretched the available syntactic technology. It seems that you can't avoid going in higher dimension whenever you tackle such issues. I was using groupoid-enriched categories as the basic language of my axiomatization. In other words, a class comes *indissociably equipped* with a notion of isomorphism between its objects, and only discrete classes have the true equality predicate. The point is that the classes that you first meet in real life are classes of sets-with-structure, and that *if you have properly defined a structure, you should know what the isomorphisms are*. Moreover, whatever you do to a mathematical object, you should be able to transport along an isomorphism. Naturally I got the idea from André's theory of combinatorial species. This is perfectly in accordance with dependent type theory: you don't have to know when two structures are equal; what really matters is having an iso between them, because then they are interchangeable. So I was working on the principle that all the constructions usually done on sets should be lifted to groupoids, which then always allow you to use transport on whatever you've constructed. But another problem I hit was that the powerset construction is very much weakened, because given a groupoid X, the only natural notion of PX is the (discrete) class of all subgroupoids that are isomorphism-closed ("replete"). This weakens the logic very much and you cannot use higher-order logic to do things like constructing sums, as in elementary toposes. But you sitll can interpret a form of predicate logic in there. Naturally a predicate in general is interpreted as a replete subobject, which is quite natural. A property only makes sense only if it is invariant under iso. The use of subobjects as predicates show that his approach is more aligned with Church-style intuitionism than Martin-Löf-style constructive foundations. One of these interesting observation that I made is that there is a special version of the axiom of choice in that context, which is perfectly suited for category theory, but does not clash with constructivism. And it is valid in fibrations and stacks. Presented in ordinary categorical language, it goes: given a class/groupoid G and a family of classes that depend on it (a fibration of groupoids over G in the ordinary sense) such that every class/fiber of the family is inhabited (which is surjective as a fibration) and such that all theses fibers are *equivalent to discrete sets* (in other words such that hom-sets are never bigger than singletons, Bénabou has a name for these) then the fibration has a splitting. This is the axiom of choice that categorists use all the time: universal constructions give rise to exactly such fibrations---existence up to uniqueisomorphism---and they are the cases when the axiom of choice is needed. Richard mentions some foundational work that I was not aware of, where the higher-order categories go all the way up to tri. It seems that this particular case of dimension-climbing is a formal consequence of the base axiomatics, while mine came from semantics. But I think we should seize the bull by the horns and base foundations on higher- dimension groupoids (i know that other people on this list agree, and I should mention Makkai's opetopes). Because naturally after you've consider classes of sets-with structure, you cannot avoid getting (meta?)classes of classes-with-structure, where isomorphism has become equivalence, und so weiter. To go back to André's original question: you can build foundational universes whose inhabitants are groupoids and ordinary not sets/ classes in general. The diagonal in these will exist *but it will not be a predicate*. Hope this isn't too ponderous, François [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
* Re: equality is beautiful 2010-01-13 11:53 ` lamarche @ 2010-01-13 21:29 ` Michael Shulman 0 siblings, 0 replies; 28+ messages in thread From: Michael Shulman @ 2010-01-13 21:29 UTC (permalink / raw) To: lamarche, categories This whole discussion has been very instructive to me, especially by showing that the same fundamental ideas have occurred to many people over and over again, but seemingly never quite made it out into the general mathematical consciousness. (Either that, or else I've completely missed them.) lamarche wrote: > Several years ago i circulated a manuscript where I was trying to > formalize foundations of category theory by specializing the > space/discrete space duality above to groupoid/discrete groupoid. I was > using fibrations of groupoids over a base category (potentially a topos) > as a reference model. In other words, I was trying to find the kind of > elementary toposes you would get if you subsituted fibrations (and > stacks) of groupoids for presheaves (and sheaves). I made some very > interesting observations, but one problem I hit was that these > categories are only bi-cartesian closed, not cartesian closed, and that > really stretched the available syntactic technology. I would be interested in seeing this manuscript, because it sounds like exactly the same direction that some people have recently been trying to work on "higher-dimensional type theory" and 2-topos theory. For instance, Richard Garner's paper on "two-dimensional type theory" (http://www.dpmms.cam.ac.uk/~rhgg2/2-LCCC/2-LCCC.html) sounds almost exactly like the type theory you are describing, with categories for which Hom(x,y) is a "discrete set", i.e. has a diagonal that "is a predicate" (i.e. is "extensional"). He also deals with an "intermediately weak" form of cartesian closure for 2-categories. A number of people have also recently been thinking about 2-dimensional analogues of elementary toposes. On the one hand, there is Mark Weber's work on "2-toposes" which of course uses "strict" cartesian closure. I have been thinking from a different direction, starting from Street's characterization of "Grothendieck 2-toposes" with Giraud-like exactness axioms, using those exactness axioms to describe an internal logic/type theory for a "2-pretopos" which contains "hom-objects" that are "discrete"---whereas not every object is discrete. (A very preliminary version of this can be found here: http://ncatlab.org/michaelshulman/show/2-categorical+logic .) It generally seems to me that most "first-order" properties of elementary toposes generalize quite well, whereas those that use power objects are touchier. > One of these interesting observation that I made is that there is a > special version of the axiom of choice in that context, which is > perfectly suited for category theory, but does not clash with > constructivism. And it is valid in fibrations and stacks. Presented in > ordinary categorical language, it goes: given a class/groupoid G and a > family of classes that depend on it (a fibration of groupoids over G in > the ordinary sense) such that every class/fiber of the family is > inhabited (which is surjective as a fibration) and such that all theses > fibers are *equivalent to discrete sets* (in other words such that > hom-sets are never bigger than singletons, Bénabou has a name for these) > then the fibration has a splitting. This is the axiom of choice that > categorists use all the time: universal constructions give rise to > exactly such fibrations---existence up to uniqueisomorphism---and they > are the cases when the axiom of choice is needed. I agree entirely. In fact, I would argue that this is not really a version of the axiom of choice at all, but rather a principle of *functor comprehension*. In ordinary set theory, the axiom of choice is not necessary in order to make choices that are uniquely determined. This is sometimes called the "axiom of unique choice" or "axiom of non-choice" or the "function comprehension principle." In categorical language, it corresponds to the fact that any morphism which is both monic and strong epic must be an isomorphism (in a pretopos, of course every epic is strong). This makes the most sense to think about in a regular category, which has stable (strong epi, mono) factorizations, and the function comprehension principle is true in the internal logic of any such category. Likewise, in category theory, the axiom of choice "should" not be necessary in order to make choices that are uniquely determined up to unique specified isomorphism. The fact that an axiom of choice *is* required for such "choices" in standard set-theoretic foundations of category theory I would regard as merely a defect of those foundations. (This defect can, however, be worked around by using "anafunctors" instead of ordinary functors.) Another way of stating the "functor comprehension principle" is that any fully faithful functor (between groupoids, or even between categories) which is surjective on objects must have a section, or equivalently that any functor which is fully faithful and essentially surjective must be a (strong) equivalence. In 2-categorical language, this corresponds again to saying that any map which is both "monic" and "strong epic" must be an equivalence. Here we define a morphism in a 2-category (or bicategory) to be "monic" if it is "fully faithful" in the representable sense (perhaps this should be called "1-monic" for disambiguation with morphisms that are merely "faithful"), and "strong epic" (or "strong 1-epic") if it is left orthogonal to monics (in the bicategorical sense). In Cat, the monics are the fully faithful functors, and the strong epics are those that are essentially surjective on objects. In his paper "A characterization of bicategories of stacks," Street observed that Cat is a regular 2-category, i.e. it has good stable (strong epi, mono) factorizations. The functor comprehension principle is of course true, for the same tautologous reasons, in the "internal logic" of any regular 2-category, suitably defined. However, the fact that Cat is a regular 2-category (and in fact, the characterization of strong epics in Cat as e.s.o. functors) depends on the axiom of choice. But surely AC "should" not be necessary for Cat to be a regular 2-category, just as AC is not necessary for Set to be a regular category. This can be remedied with anafunctors: the bicategory of categories and anafunctors is always regular, whether or not we assume AC. Alternately, however, we could assume in our foundational axioms "Cat is a regular 2-category" or better a "2-topos," instead of a set-theoretic axiom system about Set, and get the functor comprehension principle automatically (and without implying any form of AC). Best, Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F565E@CAHIER.gst.uqam.ca>]
* dagger not evil (2) [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F565E@CAHIER.gst.uqam.ca> @ 2010-01-06 15:44 ` Joyal, André 0 siblings, 0 replies; 28+ messages in thread From: Joyal, André @ 2010-01-06 15:44 UTC (permalink / raw) To: Peter Selinger, Categories List Dear Peter and all, In my last message, I wrote that the forgetful functor DCat ---> Cat is wrong because it is not a right Quillen functor. The argument is not good enough. I believe that a forgetful functor XStruc--->Cat should reflect weak equivalences in addition to preserving them. The forgetful functor DCat ---> Cat preserves weak equivalences but it does not reflect them. Because two objects in a dagger category can be isomorphic without been unitary isomorphic. Best, aj -------- Message d'origine-------- De: Joyal, André Date: mar. 05/01/2010 15:04 À: Peter Selinger; Categories List Objet : dagger not evil Dear Peter and all, I cannot resist adding my grain of salt to the ongoing discussion on dagger categories. I will take the point of view of a homotopy theorist. Recall that the category of small categories Cat admits a "natural" model structure (called the "folk" model structure for the wrong reason by the folks). The category of small dagger categories DCat also admits a "natural" model structure. A dagger functor f:A-->B is a weak equivalence iff it is fully faithful and unitary surjective (this last condition means that every object of B is unitary isomorphic to an object in the image of the functor f). The cofibrations and the trivial fibrations are as in Cat. A fibrations is a unitary isofibration (a map having the lifting property for unitary isomorphisms). .... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 28+ messages in thread
end of thread, other threads:[~2010-01-20 5:52 UTC | newest] Thread overview: 28+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2010-01-03 7:23 the definition of "evil" Peter Selinger 2010-01-03 17:10 ` Claudio Hermida 2010-01-03 17:53 ` John Baez 2010-01-04 17:14 ` Michael Shulman 2010-01-04 9:24 ` Urs Schreiber 2010-01-05 20:04 ` dagger not evil Joyal, André 2010-01-06 8:40 ` Toby Bartels 2010-01-07 5:50 ` Peter Selinger 2010-01-08 0:45 ` Joyal, André [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5672@CAHIER.gst.uqam.ca> [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5673@CAHIER.gst.uqam.ca> 2010-01-09 3:29 ` equality is beautiful Joyal, André 2010-01-10 17:17 ` Steve Vickers [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5677@CAHIER.gst.uqam.ca> 2010-01-12 10:25 ` A challenge to all Steve Vickers 2010-01-12 16:24 ` Joyal, André 2010-01-13 0:03 ` David Roberts 2010-01-13 0:47 ` burroni [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5688@CAHIER.gst.uqam.ca> [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F568B@CAHIER.gst.uqam.ca> [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F568D@CAHIER.gst.uqam.ca> [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F568F@CAHIER.gst.uqam.ca> 2010-01-15 19:33 ` Joyal, André 2010-01-20 5:52 ` Michael Shulman 2010-01-13 1:02 ` Jeff Egger 2010-01-13 2:28 ` Michael Shulman 2010-01-13 20:53 ` equality Dusko Pavlovic 2010-01-14 14:23 ` equality Colin McLarty 2010-01-13 23:43 ` A challenge to all Peter LeFanu Lumsdaine 2010-01-15 19:40 ` Thomas Streicher 2010-01-10 19:54 ` equality is beautiful Vaughan Pratt 2010-01-11 2:26 ` Richard Garner 2010-01-13 11:53 ` lamarche 2010-01-13 21:29 ` Michael Shulman [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F565E@CAHIER.gst.uqam.ca> 2010-01-06 15:44 ` dagger not evil (2) Joyal, André
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).