`{H : IsTrunc (-2) A} : Contr A := H. Global Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A} : forall x y : A, IsTrunc n (x = y) | 1000. Proof. generalize dependent A. simple_induction n n IH; simpl; intros A H x y. - apply contr_paths_contr. - apply istrunc_S. rapply IH. Defined.
Require Import