(n : trunc_index) (A : Type) : IsEquiv (istrunc_unfold n A). Proof. simple refine (Build_IsEquiv _ _ (istrunc_unfold n A) _ _ _ _). - destruct n. + intros [center contr]; exact (Build_Contr _ center contr). + intros H. exact (istrunc_S _ H). - destruct n; reflexivity. - intros [center contr|k istrunc]; reflexivity. - intros [center contr|k istrunc]; reflexivity. Defined.