Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added a little bit of content to (0,1)-category. Just a little bit. (0,1)-content, so to say.
Added to (0,1)-category the observation that a (0,1)-category with the property of whose each morphism is iso (that is, a -groupoid) is a setoid. Are there constructive aspects which I should take notice of?
Also updated this description to equivalence relation in the section on setoids.
A -category in which every -morphism is invertible is precisely a -category, which is the same as a -category (because the first and second number are the same) and the same as a -groupoid (because the second number is zero).
More generally, we don’t talk about (n,r)-groupoids because they are the same as n-groupoids, the only difference between n and r being invertibility.
Is an -groupoid any different from an -groupoid? It seems that the extra condition that every -cell is invertible when isn’t an extra condition at all, if we already are in an -groupoid or -groupoid where every arrow is invertible to begin with.
(I had the tab open without refreshing for some time, which explains why I didn’t see Mike’s reply before posting. The soccer game’s on.)
A further comment, at 0-category, a 0-category is defined as a set. I mentioned that this is the case only up to equivalence and changed the actual definition to setoid, to be consistent with (0,1)-category.
You’re the one who said that a 0-category is a setoid. I don’t think that’s quite accurate, even if at the level of literal data it’s technically true (although even that depends on a particular definition of 0-category) — generally one treats setoids differently than 0-categories. When 0-categories are treated categorically, they really are no different than sets.
Colin, I’m not clear on what the real difficulty is supposed to be. Let me try to rephrase what I think Mike might be saying:
generally one treats setoids differently than 0-categories
I think this means there is a category of setoids and setoid maps (those which preserve the equivalence relation). This is quite different from (it’s not a topos for instance). But from the POV of higher category theory, it’s what we might call a naive truncation of the -category of 0-categories, where we simply discard -cells for .
When 0-categories are treated categorically, they really are no different than sets.
If we more reasonably form the “homotopy category” consisting of setoids/0-categories and functors between them modulo natural isomorphism, then we get a category equivalent to . (For the moment “equivalence” means weak equivalence: the evident functor is fully faithful and essentially surjective.) A better way of saying it might be that if we regard the 1-category as an -category, then we have an -equivalence .
I would rather say that a -category is a setoid up to isomorphism and a set up to equivalence. And of course, up to equivalence is better.
Actually, even speaking of what things are up to isomorphism is a bit arbitrary, since what you get depends on where you start, but this way of saying it reflects what is probably a common starting point for people first coming to higher category theory: ordinary category theory.
To be honest, it is a bit dicey even to say that a -category is a setoid up to isomorphism, but the issue there has to do with the term ‘setoid’. Although it was me who started saying things like ‘A setoid is a set equipped with an equivalence relation.’, the people who use setoids are people who start with an impoverished notion of set (specifically a notion that cannot handle quotient sets) and introduce setoids to fix this. And the category that they use (possibly implicitly) is not the naïve category of setoids that Todd refers to but the homotopy category that he refers to next.
I essentially “rolled back” the first sentence of the definition section at 0-category so as not to mention setoid, and then tried to summarize some of the discussion above into remarks, specifically the second remark, where setoids are mentioned. Perhaps those who were in this discussion could read this over (it feels heavy to me, but it may be useful for those who feel some puzzlement as they hop from one nLab page to another).
I moved the remark about setoids to equivalence relation, where it is really needed.
If we more reasonably form the “homotopy category” consisting of setoids/0-categories and functors between them modulo natural isomorphism, then we get a category equivalent to . (For the moment “equivalence” means weak equivalence: the evident functor is fully faithful and essentially surjective.)
Your parenthetical suggests you are not assuming AC, but I think this is only true if you do assume AC. E.g. if is a surjection without a section, then is a map of setoids inducing an isomorphism in , but it’s not an isomorphism in that homotopy category of setoids (and more generally, I don’t think will be isomorphic to any set in that homotopy category). To make it an equivalence without AC I think you have to include “anafunctors” between 0-groupoids, which setoid-theorists rarely do.
It’s also not clear to me that people who use setoids are actually working in this homotopy category. Sometimes it seems like they are, but I think often they actually do use given representatives of the morphisms.
Thanks for the note, Mike. (Noted, but I don’t think anything I wrote into the entry needs to be changed.)
Edit: actually, yes, I was assuming AC without saying so. Sorry if the phrasing was confusing.
To make it an equivalence without AC I think you have to include “anafunctors” between 0-groupoids, which setoid-theorists rarely do.
It's not exactly clear what the users of setoids (I wouldn't want to say ‘setoid-theorists’) are really doing, since they're usually using a notion of ‘set’ that doesn't really match ours. (That means, of course, that they're not going to agree that the category of setoids is equivalent to the category of sets no matter how we set things up … that's why they use setoids, because the category of their sets is not enough to support mathematics, while the category of setoids is.)
But often setoid-users assume the axiom of choice in the sense that all of the sets that they accept as ‘sets’ are projective (being ‘completely presented’) and therefore the homotopy category that Todd describes does work. And on the other hand, some people (well, at least one person1, since FOLDS is the only foundation that I can think of now that does this, although it doesn't use this terminology) would use functional, entire, equivalence-respecting relations as morphisms between setoids, where ‘functional’ is defined using the given equivalence rather than equality, and these (which are in fact saturated anafunctors) also give the correct category.
It is probably no coincidence that this is also the person who invented anafunctors! ↩
I guess that’s right.
The definition of a “(-1)-truncated ∞-groupoid” used in defining a (0, 1)-category is not valid in constructive mathematics.
have now hyperlinked the word “hence” to a new entry, which is meant to be the place where this relation is explained coherently:
coming back here in order to see how to link to the new entry relation between preorders and (0,1)-categories, I ended up largely rewriting the Idea-section, merging it into what was labeled “Definition”, and then re-organizing a little more still.
1 to 22 of 22