Modules for Modalities

Homotopy Type Theory

As defined in chapter 7 of the book, a modality is an operation on types that behaves somewhat like the n-truncation. Specifically, it consists of a collection of types, called the modal ones, together with a way to turn any type $latex A$ into a modal one $latex bigcirc A$, with a universal property making the modal types a reflective subcategory (or more precisely, sub-(?,1)-category) of the category of all types. Moreover, the modal types are assumed to be closed under ?s (closure under some other type formers like ? is automatic).

We called them “modalities” because under propositions-as-(some)-types, they look like the classical notion of a modal operator in logic: a unary operation on propositions. Since these are “monadic” modalities ? in particular, we have $latex A to bigcirc A$ rather than the other way around ? they are most closely analogous to the “possibility” modality of classical…

View original post 2,495 more words

This entry was posted in Philosophie. Bookmark the permalink.