### Modal Types Revisited

#### Posted by David Corfield

We’ve discussed the prospects for adding modalities to type theory for many a year, e.g., here at the Café back at Modal Types, and frequently at the nLab. So now I’ve written up some thoughts on what philosophy might make of modal types in this preprint. My debt to the people who helped work out these ideas will be acknowledged when I publish the book.

This is to be the fourth chapter of a book which provides reasons for philosophy to embrace modal homotopy type theory. The book takes in order the components: types, dependency, homotopy, and finally modality.

The chapter ends all too briefly with mention of Mike Shulman et al.’s project, which he described in his post – What Is an n-Theory?. I’m convinced this is the way to go.

PS. I already know of the typo on line 8 of page 4.

Posted at November 18, 2018 9:14 AM UTC
## Re: Modal Types Revisited

This is very nice! I’m about halfway through it. I really like the replacement of global “possible worlds” (which I could never really make sense of metaphysically) by a local “domain of variation” or “implicitly understood collection of relevant situations” for every usage of modalities like “necessary” and “possible” in natural language.

One suggestion: I found the notation on p13 to be kind of confusing. You seem to be using “$7(w)$” to denote the “function which sends any argument $w$ to the constant $7$”, which is the opposite of the usual convention by which $f$ denotes a function and $f(x)$ denotes its

valueat an argument $x$. I had trouble even parsing the more complicated constructions like $\Box_W(8(w)\gt 7(w))(w)$ — is this supposed to mean $\Box_W((8(w)\gt 7(w))(w))$ or $(\Box_W(8(w)\gt 7(w)))(w)$? Do both of those even make sense? What do they mean? In “(the number of planets$(w) \gt 7(w))(a)$” do the two $(w)$s denote simply “making something a function” while the $(a)$ ambiguously denotesevaluatinga function at a point $a$?I suggest a notation for making functions that is different from the notation for evaluating functions. Would your intended audience be able to deal with $\lambda$-notation? If “the number of planets” is implicitly considered a function of world, then the latter example could be written “(the number of planets $\gt_W (\lambda w.7))(a)$” (where $\gt_W$ denotes the pointwise application of $\gt$ to functions), which I find much clearer, and which can be $\beta$-reduced to “(the number of planets)$(a) \gt (\lambda w.7)(a) = 7$”.