Descent between subuniverses

We study here a strengthening of the relation O << O' saying that O-modal type families descend along O'-equivalences. Pairs of reflective subuniverses with this relation share nearly all the properties of a reflective subuniverse O paired with its subuniverse Sep O of separated types (see Separated.v) and also many of those of a single left exact modality (see Lex.v). Thus, many of the results herein generalize those of RSS for lex modalities and those of CORS for separated subuniverses. Note that this kind of descent is not the same as the "modal descent" of Cherubini and Rijke. When we get around to formalizing that, we may need to worry about disambiguating the names.

Definitions

This definition is an analogue of the statement of Lemma 2.19 of CORS, and of Theorem 3.1(xiii) of RSS. Note that CORS Lemma 2.19 includes uniqueness of the extension, which we don't assert explicitly. However, uniqueness follows from the ReflectsD parameter -- see ooextendable_TypeO_lex_leq below.

Unfortunately, it seems that generalizing binders don't work on notations: writing `{O <<< O'} doesn't automatically add the precondition O << O', although writing `{O_lex_leq O O'} does.

Left exactness properties

We prove analogues of the properties in section 2.4 of CORS and Theorem 3.1 of RSS, but in a different order, with different proofs, to increase the generality. The proofs in CORS use Proposition 2.26 for everything else, but it seems that most of the other results are true in the generality of two reflective subuniverses with O <<< O', so we give different proofs for some of them. (To show that this generality is non-spurious, note that a lex modality O satisfies O <<< O, but does not generally coincide with Sep O.) In the case of a single modality, most of these statements are equivalent to lex-ness (as stated in Theorem 3.1 of RSS). We do not know if anything similar is true more generally.

Proposition 2.30 of CORS and Theorem 3.1(xii) of RSS: any O'-equivalence is O-connected. The special case when f = to O' A requires only O << O', but the general case seems to require O <<< O'. It is convenient to have this as an instance in this file, but we don't make it global, as it requires that Coq guess O'.

A generalization of Lemma 2.27 of CORS: functor_sigma of a family of O-equivalences over an O'-equivalence is an O-equivalence. CORS Lemma 2.27 is the case when f = to O' A and g is a family of identities.

Families of O-modal types descend along all O'-equivalences (not just the O'-units, as asserted in the definition of <<<.

Morally, an equivalent way of saying O <<< O' is that the universe of O-modal types is O'-modal. We can't say this directly since this type lives in a higher universe, but here is a rephrasing of it.

We can also state it in terms of belonging to a subuniverse if we lift O' accessibly (an analogue of Theorem 3.11(iii) of RSS).

If f is an O'-equivalence, then ap f is an O-equivalence.

Theorem 3.1(i) of RSS: path-spaces of O'-connected types are O-connected.

Proposition 2.26 of CORS and Theorem 3.1(ix) of RSS; also generalizes Theorem 7.3.12 of the book. Here we need to add the extra assumption that O' ≤ Sep O, which is satisfied when O' = Sep O but also when O is lex and O' = O. That some such extra hypothesis is necessary can be seen from the fact that Tr (-2) <<< O' for any O', whereas this statement is certainly not true in that generality.

Typeclass search can find this, but it's quicker (and may help the reader) to give it explicitly.

functor_hfiber on a pair of O'-equivalences is an O-equivalence.

Corollary 2.29 of CORS: O' preserves fibers up to O-equivalence.

Typeclass search can find this, but it's faster to give it explicitly.

Theorem 3.1(iii) of RSS: any map between O'-connected types is O-connected. (Part (ii) is just the version for dependent projections.)

Theorem 3.1(iv) of RSS: an O-modal map between O'-connected types is an equivalence.

Theorem 3.1(vi) of RSS (and part (v) is just the analogue for dependent projections).

An enhancement of Corollary 2.29 of CORS, corresponding to Theorem 3.1(viii) of RSS: when O' is a modality, the map between fibers is not just an O-equivalence but is O-connected.

Theorem 3.1(vii) of RSS

functor_pullback on a triple of O'-equivalences is an O-equivalence.

Proposition 2.28 of CORS, and Theorem 3.1(x) of RSS: the functor O' preserves pullbacks up to O-equivalence.

The "if" direction of CORS Proposition 2.31, and the nontrivial part of Theorem 3.1(xi) of RSS. Note that we could also deduce Theorem 3.1(iii) of RSS from this.

Here's the "only if" direction of CORS Proposition 2.31. Note that the hypotheses are different from those of the "if" direction, and the proof is shorter than the one given in CORS.

An interesting scholium to Proposition 2.31.

Here is the converse of ooextendable_TypeO_lex_leq.

And a version for the accessible case.