The n-Category Café

Thanks, Tom. People can get a very good idea of the book’s contents from the last 4 entries at the PhilSci Archive (in the order 7, 8, 9, 6, though these have been considerably reworked and augmented).

With any reasonable background in category theory/type theory, there’s not much mathematics for the reader to learn, but hopefully there’s interest in seeing what philosophical topics are touched by familiar constructions.

Probably the harder work is the explicit task of winning over philosophers with little or no category theory/type theory background. I think a couple of long threads from 6 years ago (I and II) show that I have my work cut out getting people to budge from minor variations on the first-order logic and set theory framework.

Thanks! There really could be a bright future in which philosophy, mathematics, computer science, linguistics and others converge.

I see from your site

I’m generally interested in what it means to be a thing…

it’s easy to see how an applied type theory has to address such matters.

Two things come to mind: graded modalities and aufhebung.

So presumably constructions from the graded monad literature should carry through to the homotopic case.

If you haven’t seen it, there are general results on modalities in homotopy theory in A Generalized Blakers-Massey Theorem.

modalities (by which I mean: factorization systems on $\infty$-categories with base-change-stable left class – I’m not 100% this is the sense the term is being used in the present context).

Yes, that’s correct, modulo internalization. A modality in the internal homotopy type theory of a locally cartesian closed $\infty$-category corresponds externally to a pullback-stable factorization system; this is discussed in the appendix of RSS.

I don’t know where you picked up the word “modality” for a stable factorization system, but the only usages of it in $\infty$-category theory that I’ve seen (e.g. ABFJ) are actually imports from the HoTT terminology by way of this correspondence.

But there are no nontrivial left exact localizations of the $\infty$-topos of spaces!

Are you aware of the results of CORS that any reflective subuniverse (e.g. localization at a set of primes) together with its reflective subuniverse of separated types together behave very much like a left exact modality?

there is a bijection between nullifications … and modalities on the $\infty$-topos of spaces. … I suspect it’s really the modalities one ought to be thinking about.

Yes, I believe that’s correct. Except that when working in the internal HoTT of an arbitrary $\infty$-topos, the bijection is recovered: internal nullifications again correspond bijectively to stable factorization systems. This is also in RSS.

Is there a good “calculus of interrelated modalities” out there?

This is very much a topic of current research in HoTT, but CORS is an excellent start. From any reflective subuniverse $L$ they construct another reflective subuniverse $L'$ such that the $L'$-modal types are the $L$-separated types, i.e. those whose identity types ($\infty$-categorically, their diagonal) are $L$-modal. Iterating this you get a tower of subuniverses $L^{(n)}$, which specializes to the tower of $n$-truncations if you start from the $(-2)$-truncation (the trivial reflective subuniverse containing only the terminal object).

ABFJ have also studied other operations on modalities, such as the join, and I believe have a relative notion of “Postnikov tower”. And Rijke and Wellen have recently been studying notions of “modal descent” and a construction of a new factorization system of “etale maps” corresponding to any modality. I’m certain there’s a whole zoo of structure on the collection of modalities waiting to be explored.

Thanks, David and Mike, that’s helpful! I think I first encountered the term “modality” in ABFJ and was aware it had some sort of significance in HoTT; terminologically I was mostly unsure of how this might map into a book on philosophy.

I think one key term I’ve been missing is “separated types” with respect to a modality. I guess I’ve been putting off reading the type-theoretical literature on modalities, when I should really be diving on in!

To see how modalities turn up in my book you could take a look at the article discussed on a previous post, which is little altered as Chap. 4.

To provide a quick connection, modalities in philosophy often refer to invariance under variation (as in necessity meaning true in all possible worlds). Small wonder then that there are spatial concepts, such as presheaves, deployed in models for modal logic.