Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: our papers

Topic: The derivator of setoids

Mike Shulman (May 19 2021 at 03:09):

My paper "The derivator of setoids" is now on the arxiv: https://arxiv.org/abs/2105.08152.

Here is the abstract:

Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete. We will show that nevertheless, it can be enhanced to a derivator: the formal structure of categories of diagrams related by Kan extension functors. Moreover, this derivator is the free cocompletion of a point in a class of "1-truncated derivators" (which behave like a 1-category rather than a higher category).

In classical mathematics, the free cocompletion of a point relative to all derivators is the homotopy theory of spaces. Thus, if there is a homotopy theory that can be shown to have this universal property constructively, its 1-truncation must contain not only sets, but also setoids. This suggests that either setoids are an unavoidable aspect of constructive homotopy theory, or more radical modifications to the notion of homotopy theory are needed.

Mike Shulman (May 19 2021 at 03:14):

This paper has a funny story.

Mike Shulman (May 19 2021 at 03:14):

One of the projects I'm "supposed" to be working on right now (and which I'm going to talk about at the topos institute next week -- yikes, I should write those slides) is giving an explicit description of the semantics of 1-truncated HoTT in (2,1)-toposes. The point is partly pedagogical, but also preliminary to another project I'm supposed to be working on, of finally making sense of "stack semantics" as a first-order fragment of the internal 1-truncated HoTT of the (2,1)-topos of stacks over an elementary topos.

Mike Shulman (May 19 2021 at 03:17):

But as I was working on this (2,1)-topos semantics, everything seemed so explicit that I thought surely it must be possible to do in constructive mathematics, so I started trying to do it that way. But then I started running into unexpected snags, and so of course instead of giving up and just doing it classically I felt the need to figure out what was going on. (This isn't just stubbornness and curiosity -- elementary topos theory is itself so constructive that it would be disappointing if stack semantics, which is supposed to be an extension of the usual internal logic of a topos, required a classical metatheory.)

Mike Shulman (May 19 2021 at 03:19):

Some of the problems I was encountering seemed like they would go away if I worked with "e-groupoids" instead of ordinary groupoids. Intuitively, an e-category is a "category enriched over setoids". So I had setoids turning over in my head, trying to figure out if there was a good general way to work with e-groupoids and ordinary groupoids in parallel.

Mike Shulman (May 19 2021 at 03:20):

Then about 2 months ago my family was out camping at Joshua Tree National Park, and one night I couldn't sleep. So I lay in my sleeping bag and thought about setoids, and probably about 3am it struck me that setoids must form a derivator.

Mike Shulman (May 19 2021 at 03:25):

Being able to put the words "setoid" and "derivator" in the same sentence was such an exciting thought that when we got home I had to work it out. I'm quite happy with how it came out. True, I still don't really understand what's up with setoids, but at least I have a clearer picture of what I don't understand. And it hasn't really solved my problems with constructive (2,1)-toposes either; but at least I have a clearer idea of what the problems are, and some ideas about how to manage them.

David Michael Roberts (May 19 2021 at 05:49):

You note that "some weak form of the axiom of choice seems to be necessary to prove that the bicategoryof categories and anafunctors is cartesian closed", but it's definitely true that an additional axiom is required, even if interpreting it as a Choice principle is not clear. Simon Henry asked about something relevant on MO for the purposes of his constructive version of model categories. There is an explicit model of ZF, given in the answers, where the hom-groupoid in Gpd_ana from disc(N) to B(Z/2) is not small. One can re-do this entirely in the topos world, too, of course, along the lines of my WISC paper (I had a student learn about topos theory using the topos where this works as an eventual target). It's a really nice and relatively simple example that I hope to write up the proof of one day. It's just not clear where it would go, since it's a tiny result, in the grand scheme of things.

Nathanael Arkor (May 19 2021 at 10:55):

Since Figures 1 and 3 describe a preorder of "free relative cocompletions of a point", it seems likely that these preorders relate in a strong sense to preorders of KZ doctrines on a 2-category, e.g. on the $n$-truncated derivators, though perhaps one must also account for the weakness inherent in the homotopical structure. Do you think something precise can be said in this direction?

Mike Shulman (May 19 2021 at 14:30):

@David Michael Roberts Thanks! I'll mention that in the paper. I presume that in this model $\rm Gpd_{ana}$ is also not complete, e.g. it has no $\mathbb{N}$-fold power of $B(\mathbb{Z}/2)$?

Mike Shulman (May 19 2021 at 14:34):

@Nathanael Arkor I don't quite see what you have in mind. All the derivators in question are cocomplete in the same sense; the difference is in what kind of category they are. What 2-category are you thinking of your lax-idempotent 2-monads living on?

Nathanael Arkor (May 19 2021 at 14:41):

The sort of statement I'm imagining is: "A left derivator $\mathscr I$ is a relative cocompletion of a point if there exists a KZ doctrine $T$ such that $\mathscr I \simeq T(1)$.". The 2-category in question could be the 2-category of left derivators, for instance. Then, since evaluation of KZ doctrines at 1 should preserve their order, Fig. 1 would describe the preorder of KZ doctrines.

Mike Shulman (May 19 2021 at 14:46):

I guess it's possible that locality could be represented by a lax-idempotent 2-monad. Maybe T-local left derivators are even a reflective subcategory? I haven't really thought about it.

David Michael Roberts (May 20 2021 at 00:16):

@Mike Shulman Hmm, I haven't shown that. The topos is externally cocomplete, but it's likely that the universal property the $\mathbb{N}$-fold power fails in the internal language.

The topos in question is the category of continuous $\mathcal{G}$-sets, for $\mathcal{G}$ the $\mathrm{Ord}$-indexed product of copies of $\mathbb{Z}/2$, with the profinite topology. One might instead adapt the proof to the topos of uniformly continuous $\mathcal{G}$-sets, to get a non-cocomplete topos. I just thought of that now, so I'd have to double check.

David Michael Roberts (May 20 2021 at 00:25):

I guess you mean for $\mathrm{Gpd}_{ana}$ to be enriched over $\mathrm{GPD}$, the category of large groupoids... And clearly it's not a priori true that even if the power exists in the internal sense, it's going to be the same as in external sense. Although I'm a bit suspicious that I'm being thick and because of stack semantics magic, they will be the same.

Ulrik Buchholtz (May 20 2021 at 12:07):

I'm a bit confused about what the take-home lessons should be. I'd rather take “radical modifications to the notion of homotopy theory” than conclude that “setoids are an unavoidable aspect of constructive homotopy theory” (but to each their own).
Have I got it right if I summarize the situation as follows:

• When working in constructive set theory, we have to be very careful how we formalize category theory. We need to use ana-functors (and hence maybe WISC?) and ana-derivators. This is essentially because categories live at the level of 1-truncated mathematics, so dealing with them purely in 0-truncated mathematics is a pain. (BTW, it seems that the correct notion of morphisms in the exact completion should then be ana-functions, because then $\mathrm{Set}_{\mathrm{ex}}$ would be equivalent to $\mathrm{Set}$ and we'd have fewer problems. But ana-functions don't appear in the paper.)
• When working in univalent foundations, everything should work without a hitch if we define derivators in the proper $(2,1)$-categorial way, taking (univalent) categories as inputs. (Presumably (Der2) should be changed to concern the core inclusion?) Then the “bad” version of exact completion won't be a derivator, and all is well.

It seems the exercise of going straight from 0-truncated mathematics to spaces is too big a jump; perhaps it would be better to separately study how to do 1-truncated (constructive) mathematics using constructive set theory, and as a separate step jump to $\infty$?

I think the final question in the paper, whether Type gives rise to a derivator that is the free cocompletion of a point, merits some investigation. (Even if it's a bit premature at the moment.) Why would this require AC and not just SC (Sets Cover)? It's not even clear to me that SC would be needed, though it might be needed to show that there is a combinatorial presentation of this derivator.

David Michael Roberts (May 20 2021 at 12:30):

Continuing my train of thought from before: I think that $\mathrm{Gpd}_\mathrm{ana}$ might fail to have the $\mathbb{N}$-power of $\mathbf{B}(\mathbb{Z}/2)$ as soon as countable choice fails in the underlying set theory! This is not working internally, though, just in a classical metatheory with a topos of (classical) sets where a counted product of countable sets can be empty. More precisely, if we have an $\mathbb{N}$-indexed family of 2:1 surjections $Q_n \twoheadrightarrow \mathbb{N}$, then it possible that $\prod_{n\in\mathbb{N}} Q_n\simeq \emptyset$. In such a model of set theory I believe the power under discussion fails to exist. But I should write out the details and send them to you, @Mike Shulman , to see if I'm missing something.

Mike Shulman (May 20 2021 at 14:40):

@David Michael Roberts That would be very interesting to see!

Mike Shulman (May 20 2021 at 14:50):

Ulrik Buchholtz said:

I'm a bit confused about what the take-home lessons should be. I'd rather take “radical modifications to the notion of homotopy theory” than conclude that “setoids are an unavoidable aspect of constructive homotopy theory” (but to each their own).

For me I think it depends on the nature of the modifications. I like HoTT, obviously. It's less clear to me whether using anafunctors and WISC is sufficient to yield a well-behaved category theory in set-based constructive mathematics.
E.g. if as David suggests $\rm Gpd_{ana}$ can fail to have countable powers as soon as countable choice fails, that seems pretty bad to me. For instance, I would like to be able to define stacks of groupoids, but defining the "category of descent data" (not to speak of the stackification) requires taking limits that would in general be infinite.

However, in the paper I tried to stick as much as possible to facts rather than polemic, and let readers make their own decisions. If you have suggestions for how to make it less confusing, I'd be happy to hear them.

(BTW, it seems that the correct notion of morphisms in the exact completion should then be ana-functions, because then $\mathrm{Set}_{\mathrm{ex}}$ would be equivalent to $\mathrm{Set}$ and we'd have fewer problems. But ana-functions don't appear in the paper.)

Well, the exact (ex/lex) completion is determined by a universal property, so it is what it is. Using ana-functions gives a different category, namely the ex/reg completion of Set, which is equivalent to Set because Set is already exact. (By the way, one can imagine working in a foundational system where Set is regular but not exact, such as type theory with propositional truncation but not quotients; in that case one can argue that it's the ex/reg completion of Set that is the good category, just as in type theory without either one has to take the ex/lex completion to get an exact category.)

Mike Shulman (May 20 2021 at 18:32):

Ulrik Buchholtz said:

• When working in univalent foundations, everything should work without a hitch if we define derivators in the proper $(2,1)$-categorial way, taking (univalent) categories as inputs. (Presumably (Der2) should be changed to concern the core inclusion?) Then the “bad” version of exact completion won't be a derivator, and all is well.

Actually I would expect $\rm Set_{ex}$ to still be a derivator in this univalent sense. In fact I would expect roughly the same proof as in set-based mathematics to show that it is a derivator taking all precategories as inputs. In set-based mathematics we can't necessarily go from a $\rm Cat$-indexed derivator to a $\rm Cat_{ana}$-indexed derivator because $\rm Cat_{ana}$ is a non-reflective localization of $\rm Cat$, and so a derivator like $\rm Set_{ex}$ that doesn't invert weak equivalences in $\rm Cat$ doesn't descend to $\rm Cat_{ana}$. But in the univalent world the 2-category of univalent categories is a reflective subcategory of that of precategories, so we can just restrict a precategory-indexed derivator to a univalent-category-indexed one.

This is why I would conjecture that AC and not just SC is required to show that Type is the free cocompletion of a point: in addition to knowing that Type is built out of sets (or at most 1-types), we need to get rid of the exact completions that are still around. I could be wrong in this, but it's my current best guess.

Regarding the need for SC, I would expect that even in UF there's a set-based (or 1-type-based) construction of a derivator that is a free cocompletion of a point, and so if we want this to be equivalent to Type we need sets cover (or at least 1-types cover).

Jacques Carette (May 21 2021 at 15:41):

Quoting from the abstract:
Mike Shulman said:

Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete.

So it seems that what is meant by "the" category of setoids matters quite a bit. Because in "pure" MLTT, one can fully mechanize that Setoids is complete and cocomplete . No need for anything fancy at all.

Reid Barton (May 21 2021 at 16:11):

I think Mike is talking about the actual (not e-) category obtained by quotienting the Hom-setoids down to sets.

Jacques Carette (May 21 2021 at 16:15):

I think so too. Which reinforces my point: it matters quite a bit which version you're talking about. The e-category of setoids is fairly nice - though not as nice as the (classical) Set-category of Sets.

Mike Shulman (May 21 2021 at 17:47):

Right! That's why I said "the category of setoids", not "the e-category of setoids". (-: And why I put that only in a parenthetical, since "the free exact completion of the category of sets" is also unambiguous.

Jacques Carette (May 21 2021 at 18:11):

I find it really fascinating how delicate a lot of this is. Parts of category theory seems very robust (set-enriched 1-categories and E-categories mostly work the same, for hundreds of definitions and theorems), but their interplay is more subtle.

Mike Shulman (May 21 2021 at 18:52):

I think part of that is due to how general and formal a lot of what we think of as "category theory" really is. A huge amount of category theory can be done abstractly in a 2-category with very little additional extra structure.

Mike Shulman (May 21 2021 at 18:56):

It can also be viewed as an instance of the fact that most of category theory generalizes without a hitch to higher category theory, since an E-category can be regarded as a tricategory whose hom-bicategories are weakly discrete.

Mike Shulman (May 21 2021 at 21:36):

Is the E-category of setoids the exact completion of the (E-)category of sets, in the world of E-categories?

Ulrik Buchholtz (May 22 2021 at 11:33):

Mike Shulman said:

For me I think it depends on the nature of the modifications. I like HoTT, obviously. It's less clear to me whether using anafunctors and WISC is sufficient to yield a well-behaved category theory in set-based constructive mathematics.

Maybe we can be more precise about the desiderata. I'd say that we want a development of category theory in a predicative constructive set-theory setting (maybe MLTT+UIP+FunExt+PropExt+QITs+WISC, or some form of CETCS), that is adequate wrt a “standard” interpretation of this theory in terms of 0-truncated objects in HoTT+SC+WISC, in a sense that would have to be made precise, but could include requirements that the basic notions of category theory are definable and mean the right things (as judged by the interpretation) and maybe that categories definable in HoTT be definable up to equivalence, and that the same (co)completeness properties obtain. (One could also imagine a semantic version of adequacy, e.g., in terms of 1-sheaves of categories in 1-localic Grothendieck toposes.)

Maybe E-categories achieve this, I don't know. But maybe it's simply not possible, which would be evidence that category theory is properly 1-dimensional and cannot be adequately captured in 0-truncated mathematics, unless we're in a sufficiently classical setting.

However, in the paper I tried to stick as much as possible to facts rather than polemic, and let readers make their own decisions. If you have suggestions for how to make it less confusing, I'd be happy to hear them.

I didn't yet read it all the way through (I started with the introduction and the conclusion), so it's possible that all confusions will be dispelled upon further reading. :smile:

Well, the exact (ex/lex) completion is determined by a universal property, so it is what it is. Using ana-functions gives a different category, namely the ex/reg completion of Set, which is equivalent to Set because Set is already exact.

Right, but in this setting where Set is already exact (or just regular), the ex/lex completion is arguably an unnatural thing to look at, exactly because it forgets the regular structure, which is why it's non-idempotent and somewhat confusing to think about as a completion. (It's like taking the free group on the underlying set of a group.)

BTW, you mention in Footnote 5 that it's unclear whether $(\mathrm{Set}_{\mathrm{ex}})_{\mathrm{ex}}$ can be made into a derivator. I don't know what to expect, but if all the iterated ex/lex completions of Set are 1-truncated derivators, then again I'd be more inclined to say, so much the worse for derivators, than to conclude that iterated setoids are unavoidable.

Ulrik Buchholtz (May 22 2021 at 11:43):

Mike Shulman said:

It can also be viewed as an instance of the fact that most of category theory generalizes without a hitch to higher category theory, since an E-category can be regarded as a tricategory whose hom-bicategories are weakly discrete.

Whoah! What does weakly discrete mean here? Is this a foundation-neutral statement, i.e., if we formalize (3,3)-categories in HoTT and require that the hom-(2,2)-categories are weakly discrete, we get E-categories? Then shouldn't setoids also appear more naturally from higher category theory – if so, I might change my mind about them.

Jacques Carette (May 22 2021 at 13:28):

Mike Shulman said:

Is the E-category of setoids the exact completion of the (E-)category of sets, in the world of E-categories?

Hmm, I guess a proof (or disproof) in Agda wouldn't really help, would it. It wouldn't quite be about the same things. Though I do think I'll program up the exact completion construction. I can already tell there's going to be level issues.

David Michael Roberts (May 22 2021 at 13:30):

@Mike Shulman I must (hopefully temporarily!) walk back my claim about being able to show the power by $\mathbb{N}$ fails to exist. The approach that I had was not watertight, so I need to think a bit harder.

David Michael Roberts (May 22 2021 at 14:22):

OK, so I believe I have fixed it, and I have to go all the way to the failure of $\mathrm{Gpd}_{ana}$ to be locally essentially small, not just failure of some type of Choice of small instances. It's a lot simpler than I thought, though of course I'm using the failure of a lot weaker choice principle (and proving that consistent is more work!). So I don't have the result if I assume WISC fails, which may not be quite what you want. But I can at least be more confident in my proof (certainly as the proof is much much simpler).

In the first incorrect version, I had used some implicit assumption of choice for pairs, and then thought that later I needed the negation of countable choice for countable sets. But then I realised that the latter wasn't needed, only choice for pairs again, which I needed for the argument. This is why I really wanted to iron out the wrinkles!

Mike Shulman (May 22 2021 at 15:56):

Jacques Carette said:

Hmm, I guess a proof (or disproof) in Agda wouldn't really help, would it. It wouldn't quite be about the same things.

Why not?

Mike Shulman (May 22 2021 at 15:57):

Another question: has anyone written down a construction of sheaves of setoids? I suspect they would work better than sheaves of sets in predicative constructive mathematics -- sheafifying a presheaf of sets seems to require either impredicativity or WISC, but setoids should work without either.

Jacques Carette (May 22 2021 at 17:58):

Because the $\mathsf{Set}$ (aka $\mathsf{Type}$) of Agda isn't really the same as the sets in the original question?

Mike Shulman (May 22 2021 at 20:01):

But it could be. It doesn't have any more properties than the latter.

Jacques Carette (May 22 2021 at 20:06):

That's true. It has less. One more thing to add to the pile of things to work out.

Mike Shulman (May 22 2021 at 20:19):

David Michael Roberts said:

OK, so I believe I have fixed it, and I have to go all the way to the failure of $\mathrm{Gpd}_{ana}$ to be locally essentially small, not just failure of some type of Choice of small instances.

Okay, that makes sense. I certainly expected limits in $\rm Gpd_{ana}$ to fail to exist in that model. But that still leaves open the question of whether WISC or SVC suffices to show that $\rm Gpd_{ana}$ is complete, right?

Mike Shulman (May 22 2021 at 20:30):

Ulrik Buchholtz said:

Maybe we can be more precise about the desiderata.

My current understanding is that E-categories work pretty well for just about everything "intrinsic". The only problems with them that I've found so far are:

• They don't support a very good "strict category theory". For instance, there doesn't seem to be an analogue of the canonical model structure on Cat for E-categories, it's not clear how to interpret type theory in E-groupoids, and the traditional techniques of strict 2-category theory don't work for E-2-categories. (There are probably model categories of a sort for E-categories, but they'll be significantly more complicated than the canonical model structure on Cat.)

• They don't play well when you want or need to use sets rather than setoids. For instance, the category of 0-truncated objects in ECat is $\rm Set_{ex}$, not Set. (As a particular consequence, you lose any impredicativity that you started with in Set.) And if you interpret them semantically in the type theory of a 1-topos, you don't get the "correct" notion of internal categories or indexed categories.

Mike Shulman (May 22 2021 at 20:34):

$\rm Cat_{ana}$ does better on the second point, but also suffers from the first problem. And of course it has the additional problem of not being locally small or complete. WISC suffices for local smallness, but the situation for completeness seems to be currently unclear.

Mike Shulman (May 22 2021 at 20:36):

Finally, ordinary Cat does have a good strict category theory, and is complete and locally small. But its category of 0-truncated objects is $\rm Set_{reg}$, the reg/lex completion of Set. And it fails to be exact in 2-categorical senses, e.g. not every 1-groupoid object in Gpd is effective, and finite (pseudo)limits don't commute with filtered (pseudo)colimits.

Mike Shulman (May 22 2021 at 20:39):

So my current feeling is that if WISC or something "constructively acceptable" like it implies that $\rm Cat_{ana}$ is complete, then that's the closest we can come to a well-behaved category theory in constructive mathematics. But if not, then maybe it's impossible.

Mike Shulman (May 22 2021 at 20:41):

in this setting where Set is already exact (or just regular), the ex/lex completion is arguably an unnatural thing to look at

I mostly agree. I was just saying that it does exist and is determined by a universal property, so we can't talk about "changing the morphisms in the exact completion" -- if we change the morphisms, it's not the (free) exact completion any more.

Mike Shulman (May 22 2021 at 20:42):

if all the iterated ex/lex completions of Set are 1-truncated derivators, then again I'd be more inclined to say, so much the worse for derivators, than to conclude that iterated setoids are unavoidable.

Would you be satisfied with ana-derivators, if they exclude all those exact completions?

Mike Shulman (May 22 2021 at 20:49):

What does weakly discrete mean here?

A bicategory is weakly discrete if it admits a weak biequivalence functor to a discrete bicategory. This means that any two parallel 1-cells are related by a unique 2-cell and any 1-cell is an equivalence.

Is this a foundation-neutral statement, i.e., if we formalize (3,3)-categories in HoTT and require that the hom-(2,2)-categories are weakly discrete, we get E-categories?

It depends on how you formalize (3,3)-categories in HoTT. A "fully univalent" 2-category that is weakly discrete is also strongly discrete, so a fully univalent 3-category with weakly discrete hom-2-categories is equivalent to an ordinary univalent 1-category. But if you relax the univalence conditions, then you get E-categorical things. In fact the E-dimension is closely related to the "univalence" direction in HoTT. I learned this from Peter Lumsdaine's talk at the Palmgren memorial conference, and made some remarks about it at the very end of the paper.

Then shouldn't setoids also appear more naturally from higher category theory – if so, I might change my mind about them.

Are you saying you'd be more convinced by setoids coming from higher category theory than by setoids coming from homotopy theory? Nowadays many people generally consider those two fields to be very closely related, if not identical...

Mike Shulman (May 22 2021 at 21:55):

Here are two things worthy of note:

1. If the localization functor $\rm Cat \to Cat_{ana}$ preserves infinite products, then the axiom of choice holds. To see this, let $(A_i)$ be a family of inhabited sets and consider the corresponding family $(\sharp A_i)$ of indiscrete groupoids. Then the product $\prod_i \sharp A_i$ in Cat is the indiscrete groupoid $\sharp \prod_i A_i$. But since $A_i$ is inhabited, $\sharp A_i$ is equivalent to 1 in $\rm Cat_{ana}$, so the product $\prod_i \sharp A_i$ in $\rm Cat_{ana}$ is also equivalent to 1. Hence, if the localization functor preserves this product, there is an anafunctor $1 \to \sharp \prod_i A_i$, and hence an element of $\prod_i A_i$. Thus, if there is a "constructive" axiom ensuring that $\rm Cat_{ana}$ is complete, its limits cannot be simply induced by those of Cat.

2. In the internal language of a Grothendieck topos, $\rm Cat_{ana}$ is complete. This is because it is equivalent to the reflective sub-bicategory of Cat consisting of the small categories that are stacks for the intrinsic topology of the topos, and by an external argument every internal category has a stack completion that is again an internal category.

This suggests that instead of "projective" axioms like WISC, for completeness we should be looking at "injective" axioms. One obvious such axiom is "every small category has a small stack completion". I don't know if there is a less blatant one.

Mike Shulman (May 23 2021 at 15:20):

I wonder if the axiom of small cardinality selection implies that $\rm Cat_{ana}$ is complete.