Modalities

Dependent eliminators

A dependent version of the reflection universal property. For later use we generalize it to refer to different subuniverses in the reflection and the elimination target.

In particular, from this we get a dependent eliminator.

Conversely, if O is closed under path-types, a dependent eliminator suffices to prove the whole dependent universal property.

In particular, this is the case if O is a reflective subuniverse.

Of course, with funext this becomes an actual equivalence.

The strong order

Note the reversal of the order: O1 << O2 means that O2 has dependent eliminators into O1.

The strong order implies the weak order.

The strong order is not obviously transitive, but it composes with the weak order on one side at least.

Modalities

A modality is a reflective subuniverse with a dependent universal property with respect to itself.

However, it's not clear what the best bundled definition of modality is. The obvious one { O : ReflectiveSubuniverse & IsModality O} has the advantage that bundling a reflective subuniverse into a modality and then unbundling it is definitionally the identity; but it is redundant, since the dependent universal property implies the non-dependent one, and in practice most modalities are constructed directly with a dependent eliminator. Thus, for now at least, we take the following definition, which in RSS is called a "uniquely eliminating modality".

We don't declare modality_subuniv as a coercion or modality_prereflects as a global instance, because we want them only to be found by way of the following "unbundling" coercion to reflective subuniverses.

Unfortunately, sometimes modality_subuniv pops up anyway. The following hint helps typeclass inference look through it.

Modalities are precisely the reflective subuniverses that are << themselves.

When combined with isequiv_oD_to_O, this yields Theorem 7.7.7 in the book.

Of course, modalities have dependent eliminators.

Conversely, as remarked above, we can build a modality from a dependent eliminator as long as we assume the modal types are closed under paths. This is probably the most common way to define a modality, and one might argue that this would be a better definition of the bundled type Modality. For now we simply respect that by dignifying it with the unprimed constructor name Build_Modality.

A tactic that extends strip_reflections to modalities. It handles non-dependent elimination for reflective subuniverses and dependent elimination for modalities. strip_truncations does the same for truncations, but introduces fewer universe variables, so tends to work better when removing truncations.

Search for hypotheses of type O X for some O such that the goal is O-local.

Handle the non-dependent and dependent cases. The last case requires that O be a modality.

Ensure that we didn't generate more than one subgoal, i.e. that the goal was appropriately local.

Dependent sums

A dependent elimination of a reflective subuniverse O' into O implies that the sum of a family of O-modal types over an O'-modal type is O'-modal. More specifically, for a particular such sum it suffices for the O'-reflection of that sum to dependently eliminate into O.

Specialized to a modality, this yields the implication (ii) => (i) from Theorem 7.7.4 of the book, and also Corollary 7.7.8, part 2.

This implies that the composite of modal maps is modal.

It also implies Corollary 7.3.10 from the book, generalized to modalities. (Theorem 7.3.9 is true for any reflective subuniverse; we called it equiv_O_sigma_O.)

Conversely, if the sum of a particular family of O-modal types over an O'-reflection is in O', then that family admits a dependent eliminator.

And even a full equivalence of spaces of sections. This is stated in CORS Proposition 2.8 (but our version avoids funext by using ooExtendableAlong, as usual).

The rest is just extracting paths from sigma- and product types and contracting a couple of based path spaces.

Thus, if this holds for all sigma-types, we get the dependent universal property. Making this an Instance causes typeclass search to spin. Note the slightly different hypotheses, which mean that we can't just use the previous result: here we need only assume that the O'-reflection of A exists rather than that O' is fully reflective, at the cost of assuming that O is fully reflective (although actually, closed under path-spaces would suffice).

In particular, we get the converse implication (i) => (ii) from Theorem 7.7.4 of the book: a reflective subuniverse closed under sigmas is a modality.

Connectedness of the units

Dependent reflection can also be characterized by connectedness of the unit maps.

In particular, if O1 << O2 then every O2-unit is O1-connected.

Thus, if O is a modality, then every O-unit is O-connected. This is Corollary 7.5.8 in the book.

When O1 << O2, O_functor O2 preserves O1-connected maps.

Easy modalities

The book uses yet a different definition of modality, which requires an induction principle only into families of the form fun oa ⇒ O (B oa), and similarly only that path-spaces of types O A are "modal" in the sense that the unit is an equivalence. As shown in section 1 of RSS, this is equivalent, roughly since every modal type A (in this sense) is equivalent to O A. Our definitions are more convenient in formalized applications because in some examples (such as Trunc and closed modalities), there is a naturally occurring O_ind into all modal types that is not judgmentally equal to the one that can be constructed by passing through O and back again. Thus, when we apply general theorems about modalities to a particular modality such as Trunc, the proofs will reduce definitionally to "the way we would have proved them directly" if we didn't know about general modalities. On the other hand, in other examples (such as ~~ and open modalities) it is easier to construct the latter weaker induction principle. Thus, we now show how to get from that to our definition of modality.

It seems to be surprisingly hard to show repleteness (without univalence). We basically have to manually develop enough functoriality of O and naturality of to O.

The modal factorization system

Lemma 7.6.4

Slightly speeds up next line.

Slightly speeds up next line.

This is the composite of the three displayed equivalences at the beginning of the proof of Lemma 7.6.5. Note that it involves only a single factorization of f.

This is the corresponding first three of the displayed "mapsto"s in proof of Lemma 7.6.5, and also the last three in reverse order, generalized to an arbitrary path p. Note that it is much harder to prove than in the book, because we are working in the extra generality of a modality where O_ind_beta is only propositional.

Lemma 7.6.5, part 1.

Lemma 7.6.5, part 2.

Theorem 7.6.6. Recall that a lot of hard work was done in Factorization.path_factorization.