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: learning: reading & references

Topic: Formal Category Theory

Brendan Murphy (Oct 12 2023 at 01:30):

I've been trying to think about profunctors recently and have found the notion of a framed bicategory very helpful when doing so. Also, @Patrick Nicodemus has been talking to me a lot about his ideas on formal category theory and about double categories. And it seems like some competency with formal category theory is necessary to understand the foundations of infinity category theory. A lot of the definitions in HTT (eg of correspondences/profunctors) are a direct translation of the 1-categorical notions, when framed in a suitable way; the book also makes extensive use of simplicially enriched categories. Riehl & Verity's book on infinity cosmoi is (to my impression) about formal infinity category theory and it (1) uses enriched category theory heavily as well as (2) uses defintions from ordinary category theory (eg "adjunction") internal to a 2-category (eg Ho(QCat)) and (3) has multiple sections devoted to virtual equipments. So I have plenty of reason to want to learn formal category theory, but I'm not really sure where to start. There are a ton of competing notions for a suitable context in which formal category theory could be done, and it's hard to put together the "big picture" in my head. Is there a textbook, monograph, or other sort of more structured work than the nlab which develops formal category theory from a modern point of view, explains the (dis)advantages of various systems for doing so, and is somewhat self contained? I'm guessing the answer is no, but I'd also appreciate just a list of useful references to look at. I guess my issue is that it's hard to know where the start with this stuff and where to stop, or what's important in a first pass, or so on.

Ryan Wisnesky (Oct 12 2023 at 04:04):

What does "formal" mean here? Are you looking for formal systems for reasoning about categorical constructions, such as the co-end calculus? https://arxiv.org/pdf/1501.02503.pdf

Jean-Baptiste Vienney (Oct 12 2023 at 04:17):

I think it's about proving the kind of stuff you can prove about categories in a generic 2-category resembling $\mathbf{Cat}$ as described on the nlab or in this paper A Formal Logic for Formal Category Theory

Nathanael Arkor (Oct 12 2023 at 07:32):

Is there a textbook, monograph, or other sort of more structured work than the nlab which develops formal category theory from a modern point of view, explains the (dis)advantages of various systems for doing so, and is somewhat self contained?

Unfortunately not yet. There are three main approaches:

• Yoneda structures (cf. Street–Walters' Yoneda structures on 2-categories).
• Proarrow equipments/fibrant double categories/virtual equipments (cf. Wood's Abstract pro arrows I and Proarrows II; Shulman's Framed bicategories and monoidal fibrations; Cruttwell–Shulman's A unified framework for generalized multicategories; Koudenburg's Formal category theory in augmented virtual double categories)
• Lax-idempotent pseudomonads (cf. Bunge–Funke's On a bicomma object condition for KZ-doctrines)

Most recent approaches to formal category theory take the second approach (although the precise formalism varies). The relationship between the approaches, for the most part, is not laid out clearly in the literature, but a basic intuition is:

• Yoneda structures are based on formalising the presheaf construction.
• Proarrow equipments and related structures are based on formalising distributors/profunctors.
• Lax-idempotent pseudomonads are based on formalising the free cocompletion construction.

In nice settings, e.g. enriched category theory for a well-behaved base of enrichment (e.g. satisfying Kelly's assumptions in Basic Concepts of Enriched Category Theory), all three approaches are viable. However, with weaker assumptions, not every approach is viable. For instance, when the base of enrichment is not well-behaved, one no longer has a presheaf construction or free cocompletion, and so Yoneda structures and lax-idempotent pseudomonads are not applicable. Without enough coequalisers in the base, distributors do not compose, and so proarrow equipments and fibrant double categories are not applicable.

The most general settings are those of virtual equipments and augmented virtual equipments. It is possible to formalise presheaves in this setting (as in the work of Koudenburg), thus recovering Yoneda structures; as well as free cocompletions (not yet in the literature), and so these approaches subsume the others. Technically, augmented virtual equipments generalise virtual equipments, but it is not clear to me that there are examples captured by the former that cannot be captured by the latter by making appropriate modifications. If you are interested in learning about formal category theory in the context of higher category theory (e.g. Riehl–Verity), then it is probably most helpful to start by reading about virtual equipments (starting with Cruttwell–Shulman). However, there is still a lot of formal category theory that has not yet been carried out in this generality, so the other papers are also helpful in understanding the kinds of phenomena that may be understood using formal category theory.

John Baez (Oct 12 2023 at 08:05):

What a nice overview!

fosco (Oct 12 2023 at 08:21):

• Avoid reading Wood's original papers, and instead focus on (virtual) double categories / equipments, as Nathanael suggested. Riehl-Verity build a lot on this framework in their "calculus of bimodules," so I believe you come from there.
• The best references to learn Yoneda structures are Street-Walters' original paper, coupled with Weber's "Yoneda structures from 2-toposes"; most importantly, compare the two approaches to understand what is "good" in a good Yoneda structure à la Weber. The existence of a good Yoneda structure on V-Cat is deeply tied to this story (https://arxiv.org/abs/1804.03829), but the second paper, 10 years younger than Weber's, doesn't reference it.
• Most Yoneda structures are of a specifically well-behaved kind, meaning that the presheaf construction has additional nice properties (for example, having an adjoint or interacting well with a duality involution on top of the ambient 2-category – this second condition entails the first because the adjoint to $X\mapsto PX$ is $X\mapsto P(X^{op})^{op}$; these are important and natural examples. I'm afraid there is no specific reference for this phenomenon, apart from this preprint with Ivan Di Liberti (https://arxiv.org/pdf/1901.01594.pdf) and a set of private notes I received from Davide Bernardini. (Two points: first, there are a number of subtle and less subtle mistakes in my paper with Ivan – we were young and didn't really grasp the whole picture of this story – but the intuition that taking the Kleisli bicategory of $P$ gives an equipment is correct – more or less directly, everybody knew it; second, Bernardini was immensely kind sharing his scribbles and giving me the task of reorganizing them into a coherent set of notes. That is the best approximation of a survey of the theory of Yoneda structures that we have today, although unpublished. In January 2020, I was in the process of typesetting them properly, expanding them, and correcting mistakes. Then the publish-or-perish and the pandemic hit...)

• The French school of category theory, embodied by René Guitart, is scattered with remarks about formal category theory. If you understand mathematical French, I warmly recommend you to read the following papers:

  • Qu'est-ce que la logique dans une catégorie? (http://www.numdam.org/article/CTGDC_1982__23_2_115_0.pdf)
  • Monades involutives complémentées (http://www.numdam.org/article/CTGDC_1975__16_1_17_0.pdf)
  • Relations et carrés exacts, and Carrés déductifs; (https://web.archive.org/web/20211018142728/http://rene.guitart.pagesperso-orange.fr/textespublications/rg42.pdf) and (https://web.archive.org/web/20231001204222/http://rene.guitart.pagesperso-orange.fr/textespublications/rg48.pdf)

Brendan Murphy (Oct 12 2023 at 17:31):

Thanks so much @Nathanael Arkor and @fosco! I didn't realize the (augmented, virtual) proarrow equipment approach subsumed the KZ-monad approach. Nathanael, you say this isn't written up in the literature yet, is the case for non-virtual equipments written down somewhere?

Brendan Murphy (Oct 12 2023 at 17:32):

Also I should really try to get comfortable with mathematical French... There have been several papers I wanted to look at but got scared off by the prospect of translating while reading

Nathanael Arkor (Oct 12 2023 at 17:42):

Brendan Murphy said:

Thanks so much Nathanael Arkor and fosco! I didn't realize the (augmented, virtual) proarrow equipment subsumed the KZ-monad approach. Nathanael, you say this isn't written up in the literature yet, is the case for non-virtual equipments written down somewhere?

One can deduce this in a roundabout way: first, Walker shows in Yoneda structures and KZ doctrines that every lax-idempotent pseudomonad induces a Yoneda structure. Then, every Yoneda structure induces an augmented virtual equipment (cf. Theorem 4.24 of Koudenburg's Formal category theory in augmented virtual double categories). This is related to the preprint of @Ivan Di Liberti and @fosco that Fosco mentioned. However, one has to check for oneself that the formal notions in the language of lax-idempotent pseudomonads then correspond to the corresponding formal notions in the language of equipments: this hasn't been written out in the literature, but is perhaps a nice exercise to gain some intuition regarding the relation between the concepts.

Kevin Arlin (Oct 12 2023 at 18:18):

@Brendan Murphy Mathematical French is generally only about 3% as hard as actual French, in my experience. It's worth taking a course on reading French for graduate students if you have the opportunity, but it's really not necessary. Serre is a particularly friendly place to start.

Brendan Murphy (Oct 12 2023 at 18:24):

Yeah, I'm sure it's mostly psychological. I took a year of French in undergrad anyway

fosco (Oct 12 2023 at 21:22):

I have translated into English two of Guitart papers actually. They are hosted at Jon Sterling's "Mathematical translations" web page. Very easy to find them if you Google. I am posting from my smartphone now, but I can add a link tomorrow morning!

Dylan Braithwaite (Oct 12 2023 at 22:49):

fosco said:

They are hosted at Jon Sterling's "Mathematical translations" web page. Very easy to find them if you Google.

It looks like the page (https://www.jonmsterling.com/math-translations/) linked from the GitHub repo is dead now. I'm guessing due to Jon transitioning his website to use the tool he's been developing.

I wonder is there a plan to port it to Forester or to host it somewhere else.. it seems like a cool project

Dylan Braithwaite (Oct 12 2023 at 22:55):

Ah you can still access the rendered site through the GitHub url: http://jonsterling.github.io/math-translations

Tom Hirschowitz (Oct 13 2023 at 06:31):

For papers that are not yet entirely translated, I'd guess there are sufficiently many french-speaking people here for using the place as a virtual translation hotline. I don't want to speak for all of us, but you can at least try me.

David Egolf (Oct 13 2023 at 22:22):

On the topic of translation, I would note that even the free tier of chatGPT can (I think) do a decent job at translating mathematics. (Although it's probably important to have a way to double check its translation, as I'm sure it makes mistakes!)

For example, I'm currently looking at an introduction to abstract homotopy theory written in Brazilian Portugese. I can sort of guess at parts of what's being said (as I speak some Spanish), but not enough to follow what's going on. However, just directly selecting and copy-pasting from a PDF into chatGPT is yielding a translation that seems to make sense (at least so far!). It even does a good job at noticing when diagrams are present (they copy-paste terribly) and ignores them. In addition, it can also typset symbols using latex.

As an example...
here is a screenshot of an original paragraph:
original text

here is what I copy-paste to chatGPT:
"• se um ponto z ∈ X está na intersecção Bx ∩ By entre vizinhanças
básicas de x e de y, então este possui uma vizinhança Bz ∈ τ (z)
ali inteiramente contida. Isto significa, em particular, que qualquer
ponto x ∈ X admite vizinhanças arbitrariamente pequenas: para
quaisquer Bx, B′
x ∈ τ (x) existe uma vizinhança menor B′′
x ∈ τ (x)
contida em Bx ∩ B′
x."
(notice how the formatting above is not great)

And here is what the free tier of chatGPT outputs:
translation

Patrick Nicodemus (Oct 13 2023 at 23:34):

I think these LLM's have been very successful with translation, scoring very high on several metrics. It is one of their strong points.
However, I certainly don't know how to judge the translation quality of a language I cannot read and do not speak. So it is difficult to say on what grounds we are assessing its quality or fitness here. I personally choose not to do this for this reason.
Perhaps for math it does not matter because it is on the reader to check the correctness of the proof.
But mathematical communication is still primarily trust based in my experience. If a paper tells me a theorem is true, I will believe them and cite the paper.