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.
I have two suggestions about strict category. (I guess this is mostly directed at Toby, but anyone else should feel free to chime in.)
First: the first paragraph in the highlighted box at the top seems overly cautious to me. The reference to “FOLDS, SEAR+ε, the type theories of Martin-Löf and Thierry Coquand, and preset theories” as contexts in which non-strict categories can be defined seems certainly true to me, and I’m not sure what claims are referred to that would require not-yet-proven consistency/independence results.
We could perhaps be more precise about the type theory in question. I don’t think non-strict categories are possible in extensional type theory with identity types (are they?). In type theory without identity types, you have to talk about setoids in order to get any notion of “equality” at all, so you could get non-strict categories by taking the objects to be a type and the homs to be setoids. And if you treat intensional identity types homotopically, then it would be natural to require, in defining a 1-category, that the type of objects be 1-truncated and the homs 0-truncated, obtaining something like a 1-truncated complete Segal space — I think that would qualify as a non-strict 1-category. (I’ve added some comments along these lines to type-theoretic definition of category.)
Second: I’d like to expand on the second paragraph in the highlighted box and add it to the main entry. Specifically, I’d like to say that while in set-theoretic foundations, every category is strict, when a page on the nLab links to strict category it means that there is a category which we want to treat strictly, i.e. make use of an equality predicate on its objects somehow. I think this is a useful thing to be able to signify, even in set-theoretic foundations. (I’d also like to go through the links to “strict category” and make sure they are consistent about this.)
I was deliberately being cautious, and you may remove any extra caution if you wish. I’m happy with your other proposals too.
One clarification: even in fully extensional type theory, unless you have quotient types, there’s still a difference between weak and strict categories. More generally, if you have access to a notion of types or presets that don’t form a pretopos, so that you want to pass to a pretopos of setoids as your formalisation of $Set$, then there’s a difference between weak categories (whose objects form presets) and strict categories (whose objects form sets).
It may be that every weak category is naturally a strict category (in a free way) but that still not every strict category so arises. Then there is still a difference between them.
I thought that I had put at strict category a precise definition of the $1$-category $Str Cat$ in terms of the $2$-category $Cat$ (and some of its standard structure), but It wasn’t there. I must have only written it down elsewhere, perhaps in the discussion of $\mathcal{M}$-categories. Anyway, I put it there just now, perhaps in excessive detail.
even in fully extensional type theory, unless you have quotient types, there’s still a difference between weak and strict categories
Is that really the same difference? I thought “strict category” just meant that we have a notion of equality for the objects, and we do have that in extensional type theory even for categories with only a preset of objects. Whether the thing-with-equality that is the objects belongs to a collection of things that admit quotients seems to me to be a separate question.
The way I understand it, a strict category is a category with extra structure (per the definition now at the article). In normal set theory, not only is every category automatically a strict category, but furthermore every strict category (up to isomorphism, of course) arises in this way (ignoring size issues), at least if full choice holds. In extensional type theory with identity types but without quotient types, every category is still automatically a strict category, but not every strict category arises in this way. (In fact, not even every discrete strict category arises in this way.) The problem is that the automatic notion of equality may be finer than the correct notion of equality for the strict category in question. Thus there continues to be a difference between categories and strict categories, much as there is a difference between types (completely presented sets) and setoids (sets).
For example, take the discrete category on the set of real numbers. Of course this depends on specifics, but typically, there is no type of real numbers per se but only a type of Cauchy (pre)sequences of rational numbers. To get the set of real numbers, we must consider this type together with a certain equivalence relation, a setoid. The discrete category on the set of real numbers is essentially the exact same construction, now with a note that parallel morphisms are always defined to be equal. The automatic notion of equality on the objects of this category is equality of Cauchy (pre)sequences, but the desired notion of equality for this discrete category as a strict category is isomorphism, which is equality of real numbers. So while this category is automatically a strict category, it is a strict category in the wrong way.
I’ve put the last paragraph above in a discussion at strict category.
Okay. That’s not what I originally understood “strict category” to mean, but I think I get what you mean now.
It’s sort of a matter of categories-as-strict-categories vs categories-as-some-strict-categories.
If this is the intended meaning, then I think it would be more correct (or, at least, more precise) to state the Idea as “a strict category is a category with the structure of a set on its collection of objects” than “a strict category is a category with a notion of equality of its objects”. What do you think?
I must be too entrenched in thinking extensionally, but how is the notion of “category with a notion of equality of its objects” so different from a category with special isomorphisms, or a category with a special congruence relation?
Do you have precise definitions of the latter two concepts in mind?
Well, as far as I can tell, a strict category should turn out to be the same thing as a category with at most one chosen/special isomorphism between any pair of isomorphic objects, and this chosen isomorphism witnesses the “equality” of the two objects. (Of course, the composite of two such special isomorphisms is another special isomorphism, and the identity automorphism is always special.) A strict functor is just a functor that preserves these witnesses.
Alternatively, if we think of a category as being a collection of arrows with a partial composition operation, then choosing such a class of special isomorphisms generates a congruence relation on the class of arrows. I haven’t thought about how to axiomatise the congruence relations that arise in this fashion though. (Note that these are necessarily more general than the kind discussed in e.g. CWM Ch. II §8.)
Zhen Lin: I agree with your definition, which is already in the article: an $\mathcal{M}$-category (category with special morphisms) such that the tight (special) morphisms form a discrete category.
@Mike: I see two purposes for the notion of strict category. One purpose is ideological: to have a concept that one can insist that most large categories in mathematical practice do not meet. The other purpose is mathematical: to have a concept that many categories in mathematical practice do meet. Peter May’s example of the category of cosets is a good one, and to make it work, we need to use the set of cosets, regardless of whether our foundation gives this to us directly (in addition to giving it as a setoid, as it must to be a useful foundation of mathematics). Thus we need a precise, general, foundation-independent definition.
@Toby 14: I think I agree, now that I understand better what you were getting at. Was that intended as a response to my #9?
Not so much a specific response to #9 as just continuing the conversation from ##4–9.
This discussion made me check what the $n$Lab has on “setoid”. I have now added to that entry the line
Equivalently, a setoid is a groupoid that is 0-truncated.
That page, equivalence relation, needed some organising, so I did it.
I did a bunch of reorganizing of strict category along the lines of comment #9, with separate discussion of different kinds of foundations. There were a couple of remarks which I didn’t understand/agree with. First, even in set-theoretic foundations with AC, I don’t see why every strict category should be isomorphic (as opposed to equivalent) to a canonical one. Second, I don’t understand this paragraph:
just because there is a notion of equality of objects, we might not really have a strict category unless this notion behaves as equality ought. In particular, if $a$ and $b$ are equal objects, then they ought to be isomorphic as well. (In terms of the formal definition of strict category, this goes into the action of the functor $cl$ on morphisms.) In set theory and extensional type theory, we have this; the identity morphism $\id_a\colon a \to a$ is isomorphism $\id_a\colon a \to b$, since after all $a = b$. But in intensional type theory (even with identity types), we are not necessarily allowed to switch the type of $\id_a$ from $a \to a$ to $a \to b$ like this.
What sort of type theory are you thinking of here? I haven’t encountered any notion of “identity type” which doesn’t allow substitution, which seems to be all that is needed to show that $a\cong a$ implies $a\cong b$.
First, even in set-theoretic foundations with AC, I don’t see why every strict category should be isomorphic (as opposed to equivalent) to a canonical one.
I guess that I don’t see why either. You already fixed this.
Second, I don’t understand this paragraph: […] What sort of type theory are you thinking of here? I haven’t encountered any notion of “identity type” which doesn’t allow substitution, which seems to be all that is needed to show that $a\cong a$ implies $a\cong b$.
One might allow substitution only for sufficiently small types, making this break down for categories that aren’t locally small. But that gets caught up with size issues and so morally isn’t what we’re discussing here. I’ve taken it out. (I wanted to show that categories might not naturally be strict in type theory with intensional identity types, as opposed to type theory with extensional types, where they are strict. But there is no need for that; the real point is that one variety of such type theory, HoTT, really wants a more careful definition of category, and that’s already covered later down.)
Great, thank you!
Thank you!
I just came across another notion of strict category, in Bénabou’s 1985 paper “Fibered categories and the foundations of naive category theory”. There he takes the view that a category is a certain kind of fibred category satisfying certain “definability” properties, and it turns out that equality of objects is “definable” in such a “category” if and only if the fibration is split. This seems like another way (non-)strict “categories” might show up in ordinary mathematics.
Zhen, that is a nice observation! Would you like to add something along those lines to strict category?
Yes, Benabou’s thoughts on foundations and equality using fibrations are interesting, and to me seem like an analogue of distributors for ordinary category theory (as opposed to homotopy theory aka (oo,1)-category theory)
@Mike: I added a couple of paragraphs.
Rereading the paper, I realised Bénabou seems to define the structure of “equality of objects” to be a split fibration without too much justification, and it appears that the “definability” of “equality of objects” is an even stricter condition on the fibration! He doesn’t explicitly state what it means for “equality of objects” to be “definable”, but I suspect it goes something like this: given a fibration $p : \mathbf{E} \to \mathbf{B}$, two objects $X$ and $X'$ in the fibre $p^{-1} (I)$, we define a sieve $\mathcal{E} (X, X')$ on $I$ by saying $u : J \to I$ is in $\mathcal{E} (X, X')$ if and only if there are arrows $f : Y \to X$, $f : Y' \to X'$ cartesian over $u$ such that $Y \cong Y'$ (and this isomorphism is cartesian over $id : J \to J$); equality of objects is definable precisely when the sieve $\mathcal{E} (X, X')$ (regarded as a subfunctor of $\mathbf{B}(-, I)$) is representable for every such pair $(X, X')$. But maybe not. (The acid test is whether this gives the right conclusion for theorem 10.4.3 in Bénabou’s paper.)
Thanks! I would have assumed that definability of equality of objects (in a split fibration) would mean that given $X$ and $X'$ in $p^{-1}(I)$, the subfunctor of $\mathbf{B}(-,I)$ consisting of those $u\colon J\to I$ such that $u^*X = u^* X'$ (where $u^*$ denotes the functor induced by the splitting) is representable. Your definition sounds like “definability of being isomorphic”. (Aside: every isomorphism is cartesian.)
Ah, that makes much more sense! I was struggling to see how to use the data of the splitting.
This fits quite well with Bénabou’s example… but it’s not a perfect fit. Let $\mathbf{F}$ and $\mathbf{B}$ be non-empty categories, and set $\mathbf{E} = \mathbf{B} \times \mathbf{F}$. The canonical projection $p : \mathbf{E} \to \mathbf{B}$ is a split fibration: for each $u : J \to I$ set $u^*(I, x) = (J, x)$. Thus $u^* X = u^* Y$ if and only if $X = Y$, so the sieve is either the maximal sieve or the empty sieve. The maximal sieve is certainly representable, but the empty sieve is never representable (since $B$ is non-empty!). So the only way for equality of objects to be definable for $p : \mathbf{E} \to \mathbf{B}$ is if $\mathbf{F}$ is isomorphic (in the evil sense!) to a one-object category. But Bénabou says that equality of objects is definable if and only if $\mathbf{F}$ is isomorphic to the terminal category…
Hmm, curious. Perhaps Bénabou is implicitly assuming that “definability of equality of objects” includes definability of equality of morphisms?
Doesn’t it? Two morphisms are equal if their domains are equal, their codomains are equal and they are equal in the (now proven equal) hom-set.
Formally, in a category with the structure of a strict category (which I will think of as a kind of $\mathcal{M}$-category so that I can use language with only safe connotations), $f\colon a \to b$ and $g\colon c \to d$ are equal if there are (necessarily unique) tight morphisms $p\colon a \to c$ and $q\colon b \to d$ such that the resulting square from $a$ to $d$ commutes.
@Toby - that is a very nice characterisation, and to me it seems it gets around the issue of people getting confused about being able to compare arbitrary arrows for equality when thinking about categories in this sort of foundations (usu. something like type theory), because we are allowed to say that diagrams commute, and we are given specified ’equality’ arrows between domain and codomain.
In the context of definability in indexed categories, making sense of “they are equal in the hom-set” is exactly what it means to know that “equality of morphisms is definable”.
If that’s all that you meant by equality of morphisms, OK. That should exist in a category regardless of whether we have equality of objects. Do we need to add something to Bénabou’s version of internal category (which I’m not following completely) to get this?
It should exist in a category, but it doesn’t necessarily exist in an indexed category. Which means that S-indexed categories are somewhat too general to be a good notion of “large category relative to S” for some purposes (although for many purposes, it doesn’t matter).
1 to 34 of 34