n m A `{H : IsConnected (n +2+ m) A} : IsConnected m A. Proof. induction n. 1: assumption. apply IHn. apply isconnected_pred. assumption. Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.