All Modalities are HITs

Last Friday at IAS, Guillaume Brunerie presented a very nice proof that $\pi_k(S^n)=0$ for all $k <n$ . 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 $n \ge -2$ . 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 $\mathsf{Type}_n$ 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 $\mathsf{Type} \to \mathsf{Type}$ (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 $B : A \to \mathsf{Type}$ , and define a type X to be “B-local” if every function $B(a) \to X$ is constant, for all $a:A$ . 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 $X \to (B(a) \to X)$ 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.

5 Responses to All Modalities are HITs

Steve Awodey says:

19 November 2012 at 10:28

could resizing help here?
for example, the resizing for hProps seems to be of this sort.

- Mike Shulman says:
  
  19 November 2012 at 10:37
  
  Yeah, there does seem to be a resizing sort of thing going on. At first I started to write something along those lines, suggesting that one might consider incorporating a Vopenka-like principle into type theory, by modifying the universe-assignment rules for HITs in a way that would allow localize X to always remain in the same universe as X. But then I decided there was more to it than that, because not only do you want localize X not to increase in size relative to X, you want it to have the correct universal property with respect to all modal types, not just those belonging to the same universe as X. So it seems that you want something like “universe-polymorphic constructors” where the universe polymorphism doesn’t carry over to the universe level of the inductive type itself! Perhaps this an example of something interesting one can do with Type:Type that isn’t covered by resizing or universe polymorphism?
  
Guillaume Brunerie says:

20 November 2012 at 10:54

That’s very nice!

I have a question which is perhaps related to Steve’s question:
Is the double negation modality accessible?
I have the impression that you would need something like resizing rules for that, because we need all the propositions to be controlled by some small set of propositions.

- Mike Shulman says:
  
  20 November 2012 at 11:06
  
  That’s a good point; I think you’re right. I can’t think of any reason for double negation to be accessible with predicative hprop. (With impredicative hprop, I think it certainly is; it should be equivalent to (-1)-truncating and then killing all the hprops whose double negation is contractible.)
  
  That makes me wonder whether there are other modalities that are classically accessible, but not constructively/predicatively. Maybe “only a question of size” should instead be “only a question of size and classicality/impredicativity”?
  
  - Bas Spitters says:
    
    23 November 2012 at 16:33
    
    Predicativity problems with the double negation translation are treated in Nicola Gambino’s PhD-thesis.