Modalities: generalize OO_conn_map_isconnected and other results

[jdchristensen]

OO_conn_map_isconnected is generalized to say that any map from an O-connected type to an O'-connected type is O-connected. It used to require that both types were O'-connected. The proof is just a few lines, and trivially allows us to generalize three other results. We also state the special case for n-truncations as isconnmap_isconnected, which will be useful for #2369.

As a helper result, we add the one-liner equiv_O_functor_to_O_O_leq to ReflectiveSubuniverse.v.

That's all in the second commit. The first commit exports the previously local instance O_lex_leq_Tr. I didn't notice any problems with it exported, and it comes up in isconnmap_isconnected and will in general make it easier to apply results from Descent.v.

[Copilot]

Pull request overview

This PR generalizes OO_conn_map_isconnected (and related results) in Modalities.Descent to allow maps from an O-connected type to an O'-connected type, and then specializes the result to truncation modalities.

Changes:

• Export O_lex_leq_Tr so Tr n <<< Tr n.+1 is available globally to typeclass search.
• Strengthen OO_conn_map_isconnected, OO_isconnected_hfiber, OO_isequiv_mapino_isconnected, and OO_conn_map_functor_hfiber to require only IsConnected O on the domain side where applicable.
• Add the truncation-specialized lemma isconnmap_isconnected and simplify conn_point_incl using the generalized descent lemma.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
theories/Truncations/SeparatedTrunc.v	Exports O_lex_leq_Tr : Tr n <<< Tr n.+1 for reuse via typeclass search.
theories/Truncations/Connectedness.v	Adds isconnmap_isconnected (truncation specialization) and simplifies conn_point_incl.
theories/Modalities/ReflectiveSubuniverse.v	Adds helper equivalence equiv_O_functor_to_O_O_leq.
theories/Modalities/Descent.v	Generalizes OO_conn_map_isconnected and downstream lemmas to weaker connectivity hypotheses.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[jdchristensen]

The comments about generalizing RSS were wrong, since to get the results in RSS you already had to specialize to O = O'. Once this is ready to merge, I'll squash commits 2, 3 and 4 together.