Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 6, 2020

Modal Homotopy Type Theory - The Book

Posted by David Corfield

My book Modal Homotopy Type Theory appears today with Oxford University Press.

As the subtitle – ‘The prospect of a new logic for philosophy’ – suggests, I’m looking to persuade readers that the kinds of things philosophers look to do with the predicate calculus, set theory and modal logic are better achieved by modal homotopy (dependent) type theory.

Since dependent type theories are thoroughly interrelated with category theory, in a sense then, all these years later, I’m still trying to get philosophers interested in the latter. But this book marks a shift in strategy in making the case not only for the philosophy of mathematics, but also for metaphysics and the philosophy of language.

The book explains in order: Why types? Why dependent types? Why homotopy types? Why modal types? I’ll discuss some such issues in forthcoming posts.

Posted at February 6, 2020 10:33 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3193

10 Comments & 0 Trackbacks

Re: Modal Homotopy Type Theory - The Book

Congratulations, David! Wow!

To what extent is it a book on philosophy, and to what extent is it a book to learn mathematics from?

Posted by: Tom Leinster on February 6, 2020 12:37 PM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

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.

Posted by: David Corfield on February 6, 2020 3:37 PM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

Wow, this is so exciting!

Congratulations! I look forward to reading the book. Modal homotopy type theory – in particular its topological or geometric flavors – is dear to my heart.

Posted by: David Jaz Myers on February 6, 2020 9:45 PM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

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.

Posted by: David Corfield on February 7, 2020 8:39 AM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

Lately I’ve been thinking that maybe homotopy theorists ought to be taking more of an interest in 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).

Homotopy theorists are well-acquainted with localizations, which seem to be well-suited to the study of stable homotopy theory. But the theory has a more “awkward” feel to it when it comes to unstable localization. For example, there Bousfield localizations of the \infty-category of spectra are plentiful and rich. But there are no nontrivial left exact localizations of the \infty-topos of spaces! (This shouldn’t be surprising – if spaces are sheaves on a point, then a left exact localization is sheaves on a subspace of a point, and there are no nontrivial subspaces of a point.)

But it’s not too hard to see that there is a bijection between nullifications of the \infty-topos of spaces (i.e. localizations whose local class of maps is generated by maps to a point – these seem to be the “better-behaved” unstable localizations) and modalities on the \infty-topos of spaces. The bijection sends a nullification PP to the modality whose left class consists of those maps with PP-null fibers. In general, the notion of a modality feels more natural to me than the notion of a nullification. So when doing unstable homotopy theory in other settings where the correspondence between nullifications and modalities is not a bijection, I suspect it’s really the modalities one ought to be thinking about.

Anyway, one thing which seems essential when thinking about modalities is the ability to take advantage of the interaction between many different modalities. This is already clear with the canonical examples of the nn-connected / nn-truncated modalities – it would be pretty silly if the theory proceeded by fixing nn once and for all; the point really is to allow nn to vary so that homotopy-theoretic problems can be addressed one layer at a time. I wonder what formal framework exists for this sort of thing? Is there a good “calculus of interrelated modalities” out there? In nullification land, one has things like Farjoun’s “cellular inequalities”, relating different nullification functors to one another. Perhaps that’s the sort of thing to look to for inspiration?

Posted by: Tim Campion on February 8, 2020 6:21 AM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

Two things come to mind: graded modalities and aufhebung.

Posted by: David Corfield on February 8, 2020 10:08 AM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

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.

Posted by: David Corfield on February 8, 2020 5:57 PM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

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 LL they construct another reflective subuniverse LL' such that the LL'-modal types are the LL-separated types, i.e. those whose identity types (\infty-categorically, their diagonal) are LL-modal. Iterating this you get a tower of subuniverses L (n)L^{(n)}, which specializes to the tower of nn-truncations if you start from the (2)(-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.

Posted by: Mike Shulman on February 11, 2020 10:55 PM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

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!

Posted by: Tim Campion on February 14, 2020 6:48 AM | Permalink | Reply to this

Re: Modal Homotopy Type Theory - The Book

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.

Posted by: David Corfield on February 14, 2020 8:57 AM | Permalink | Reply to this

Post a New Comment