### 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
## 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?