fact: Definition isconnmap_pred_add n m A B (f : A -> B) `{IsConnMap (n +2+ m) _ _ f} : IsConnMap m f.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc