fact: Definition merely_isconnected n A `{IsConnected n.+1 A} : merely A := @center _ (isconnected_pred_add' n (-1) A).
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc