Library HoTT.Modalities.Meet

We construct "canonical" binary meets of reflective subuniverses (that is, whose underlying subuniverse is an intersection), without assuming accessibility. In particular, we will show: 1. Given two reflective subuniverses L and O, if L O X is O-modal, then it is a reflection into the canonical meet. In particular, this is always the case if L preserves O-modal types; this is Theorem 3.30 of RSS. 1. If L and O are lex modalities satisfying an additional "composability" condition, then the composite functor L o O converges to a reflection into the canonical meet after n+2 applications when applied to an n-type for some finite n. The latter gives in particular a synthetic approach to higher sheafification (stack completion). As described at https://ncatlab.org/nlab/show/plus+construction+on+presheaves, for any site C the topos of presheaves on its Grothendieck topology is cohesive and even totally connected, so that its shape and sharp modalities are both lex. Their canonical meet is the topos of sheaves for the given topology, and the composite functor shape o sharp is the usual "plus construction" on (higher) presheaves. Thus, we recover synthetically the result that an n-truncated type can be stackified by (n+2) applications of the plus construction. We also refer to L o O as a "plus construction" in the general case of reflective subuniverses.

The canonical meet of two subuniverses is their intersection.

The basic tool in studying its reflectivity is the "plus construction" that applies the two reflectors in sequence.

This is not necessarily a reflector, but it is a well-pointed endofunctor.

Moreover, it has the desired factorization property of a reflector (though it may not belong to the meet subuniverse itself).

Moreover, its fixed points, as a pointed endofunctor, are the types in the meet.

It follows that if Plus X ever *does* lie in the meet, then it is a reflection.

Recalling that a type is connected for a reflective subuniverse if and only if its reflector is nullhomotopic, we define a type to be "plus-connected" if its map to plus is nullhomotopic. If the meet is reflective, this coincides with connectedness for that reflective subuniverse.

Similarly, we say a map is plus-connected if all of its fibers are.

Let's now assume we are trying to intersect two lex modalities.

The plus construction, being a composite of two lex functors, is also lex. Thus, it preserves path-types.

This implies that plus-connected types are closed under path-spaces.

And hence plus-connected maps are closed under diagonals.

The plus-construction also preserves fibers.

And pullbacks.

And diagonals.

Recall that a modality is characterized by connectedness of the units. Analogously, we can now prove that the plus-units are all plus-connected. This is equivalently a sort of coherence axiom for the homotopy wellpointed_plus, that when precomposed with to_plus it becomes to_plus_natural.

Recall also (from nsep_iff_trunc_to_O) that a type is n-separated for a lex modality O if and only if its O-unit is an n-truncated map. We can now prove the analogous fact for the plus-construction. We state this using MapIn (Tr n) instead of IsTrunc n because we have more useful lemmas for MapIn.

We now make one more assumption, that the plus-construction inverts plus-connected embeddings. In the case of the plus-construction for stacks, this corresponds roughly to the "local character" condition on a Grothendieck topology.

This implies, by induction, that the plus-construction decreases the truncation-level of any finitely truncated plus-connected map.

It follows, by applying this to the plus-unit and using well-pointedness, that the plus-construction on *types* decreases their plus-separatedness.

Therefore, if a type starts out as n-plus-separated, then n+2 applications of the plus-construction suffice to make it (-2)-plus-separated, i.e. in the meet subuniverse. Hence it has a reflection.