All Modalities are HITs | Homotopy Type Theory

All Modalities are HITs

Last Friday at IAS, Guillaume Brunerie presented a very nice proof that for all . I hope he will write it up and blog about it himself; I want to talk instead about a question regarding modalities that was raised by his talk: is every modality a higher inductive type?

What I mean by a “modality” is what I have elsewhere called a stable factorization system. I’ve been experimenting with calling them “modalities” when speaking internally in type theory rather than semantically, and I wrote a little note explaining them from this point of view to a type theorist. Strictly speaking, these are idempotent, monadic modalities, but when that is understood we can drop the adjectives.

Some of the most important modalities are n-truncation, for any integer . Guillaume proposed the following syntax for defining “higher inductive n-types”, i.e. higher inductive types that are coerced to be n-truncated:

Inductive W : := ...

Thus, for instance, the n-truncation itself could be expressed simply by

Inductive (X) : :=
| : X X.

One can write out directly what the introduction, elimination, and computation rules ought to be for such a “higher inductive n-type”. The only differences are that the type being defined is automatically n-truncated, while the elimination rule only allows eliminating into families of n-truncated types.

On the other hand, one can implement a type with these rules as an ordinary higher inductive type, by adding two additional constructors that force every map out of an n-sphere to be contractible (using the hub-and-spoke style described here):

Inductive (X) : :=
| : X X
| hub : ( X) X
| spoke : (l : X) (s : ), hub l = l s.

The elimination rules one gets for this ordinary HIT are essentially those I mentioned above (although it takes a little bit of work to massage them into that form).

Now, in Guillaume’s proposed syntax, one can easily imagine replacing by any other modality. Thus the question was raised: can the resulting “higher inductive modal types” always be implemented as ordinary HITs, by adding extra constructors as above?

The general opinion at the time (including my own) seemed to be that this was unlikely. It turns out, however, that at least in the simplicial set model, the answer almost certainly depends on set-theoretic assumptions: it’s only a question of size. In particular, that means that any “reasonable” modality one might actually care about is going to be implementable as an HIT.

Why is this? I mentioned in my note that there are two equivalent ways to characterize a modality: by giving the modal operator (e.g. the n-truncation), or by giving the collection of modal types (e.g. the n-truncated types). Given the modal operator, a type is modal if the canonical map to its modalized version is an equivalence. And given the modal type, the modal operator is the reflector into the corresponding full subcategory of types.

There is also a third equivalent way to characterize a modality, by giving the anti-modal types: those which become contractible upon applying the modal operator. Of course, knowing the modal operator determines the anti-modal types. But it turns out that a type is modal if and only if every function into it out of an anti-modal type is constant. This is essentially the final theorem factsys_is_localization here. (The “only if” direction of this, for the n-truncation modality — whose anti-modal types are called “n-connected” — was a central ingredient in Guillaume’s proof.)

Now, suppose given any type family , and define a type X to be “B-local” if every function is constant, for all . Then the following HIT builds a modal operator whose modal type are precisely the B-local ones.

Inductive localize X : Type :=
| to_local : X localize X
| local_e1 : (a:A) (f : B a X), X
| local_s1 : (a:A) (f : B a X) (b : B a), local_e1 a f = f b
| local_e2 : (a:A) (f : B a X), X
| local_r2 : (a:A) (x:X), local_e2 a (fun _ x) = x.

The point is that the latter four constructors exhibit precisely the data making the inclusion of constant functions into an h-isomorphism. More generally, therefore, adding these four constructors to a general HIT spec will produce a “higher inductive B-local type”. Now we ought to be able to apply this to the family of all anti-modal types for any given modality, in which case (as mentioned above) the local types are precisely the modal types we started with.

The size issue, of course, is that the type of all anti-modal types in one universe will itself belong to the next higher universe. Hence, with the usual universe assignment rules for (higher) inductive types, when we use this type as an input to constructors as above (it would be the type A), the resulting HIT will also go up a universe. However, the identification of modal types with those that are local with respect to the anti-modal types only works at a fixed universe level.

But if it so happens that there is some universe level whose anti-modal types suffice to determine the modal types at all higher levels, then there is no problem. Semantically speaking, this is an “accessibility” issue; thus I think it’s reasonable to say that “every accessible modality is an HIT”.

The connection with large cardinals is supplied by this paper, which proves the following.

• Assuming Vopenka’s principle (a strong large cardinal hypothesis), every homotopy-reflective subcategory of simplicial sets is accessibly so.
• Conversely, if there are no measurable cardinals, then there is a homotopy-reflective subcategory of simplicial sets which is not accessibly so.

Neither of these is exactly about modalities, since a modality is not just a homotopy-reflective subcategory but a sort of “indexed” one (a stable factorization system). However, I would be surprised if similar results weren’t true for modalities as well.