n A `{IsConnected n.+1 A} : IsConnected n A. Proof. apply isconnected_from_elim; intros C ? f. refine (isconnected_elim n.+1 C f). Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.