The lex-modal fracture theorem

The fracture theorem for two modalities O1 and O2 and a type A, when it holds, states that the naturality square

 A   -->   O1 A
 |          |
 |          |
 V          V
O2 A --> O2 (O1 A)

is a pullback. This says in a certain precise sense that A can be recovered from its O1- and O2-reflections together with some information about how they fit together. If we think of O1 and O2 as subuniverses or subtoposes, then the fracture theorem says that their "union", or more precisely their *gluing*, is the whole universe. We will prove the fracture theorem holds under the assumptions that O2 is lex, and that O1-connected types are O2-modal. Note that like lex-ness, the latter is also a "large" hypothesis. But also as with lex-ness, rather than hypothesize it polymorphically with a module type, we just hypothesize it in the obvious way and allow the polymophism of the resulting theorem to be computed automatically. This actually gives more precise information: the fracture theorem for a particular type A only depends on this hypothesis for types B lying in the same universe as A. (In fact, as we will see, it only needs the special cases of the fibers of to O1 A, but in examples it seems no harder to verify the general case.) It may sometimes happen that in addition, the "intersection" of O1 and O2 is trivial. This is naturally expressed in the context of the fracture theorem by saying that O2-modal types are O1-connected, i.e. the converse of the second hypothesis of our fracture theorem. When this also holds, we can show that the universe Type can actually be reconstructed, up to equivalence, from the universes of O1- and O2-modal types and the O2-reflection from the first to the second, using the "Artin gluing construction" from topos theory.

The fracture theorem

Here are the hypotheses of the fracture theorem

The fracture theorem.

The fracture gluing theorem

We now also assume the converse of the second hyopthesis

This implies that the universe decomposes into an O1-part, an O2-part, and a gluing map. We define these pieces separately in order to make the maps transparent but the homotopies opaque.

The first two components of our path will be applications of univalence. We begin by observing that maps we will use are equivalences.

Now we start building the path.

It remains to identify the induced function with the given f. We begin with some boilerplate.

Now we have to compute through the action of ap and transport on paths in sigmas and the universe. In applying these it helps to specify a couple of intermediate steps explicitly.

Now we're down to the real point.

The propositional fracture theorem

An easy example of the lex-modal fracture theorem is supplied by the open and closed modalities for an hprop U.

We can also prove the same thing without funext if we use the nullification versions of these modalities.