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.
Reed Mullanix (May 25 2021 at 19:24):Recently, a paper[1] has been making the rounds that shows the existence of an adjoint quintuple of the form implies that must be equivalent to . This surprised me, and got me thinking about what might happen in an enriched context. Specifically, does this only work for enriched categories? I haven't thought too much about total categories, and even less about total categories in an enriched setting, so I'm a bit stumped here.
[1]: https://www.ams.org/journals/proc/1994-122-02/S0002-9939-1994-1216823-2/home.html
Nathanael Arkor (May 25 2021 at 19:35):I don't think it's obvious to what extent this result generalises. The proof in that paper makes use of some arguments that aren't available in a more general setting, at least not directly. I don't even think Lemma 2 is provable constructively, for instance. Note that the argument that Set is involved in an adjoint chain of length 5 is straightforward: the difficult part is the converse implication.
Mike Shulman (May 25 2021 at 19:41):Right, the last step of Lemma 2 invokes Freyd's theorem that a complete small category is a preorder. But this is not true constructively, and it's not even entirely clear what it would mean in an enriched context.