n m A B (f : A -> B) `{IsConnMap (n +2+ m) _ _ f} : IsConnMap m f. Proof. intro b. exact (isconnected_pred_add n m _). Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.