fact: Definition is0connected_isconnected (n : trunc_index) A `{IsConnected n.+2 A} : IsConnected 0 A := isconnected_pred_add' n 0 A.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc