{A B} := @path_trunctype (-1) A B. Global Instance istrunc_trunctype {n : trunc_index} : IsTrunc n.+1 (TruncType n) | 0. Proof. apply istrunc_S. intros A B. refine (istrunc_equiv_istrunc _ (equiv_path_trunctype@{i j} A B)). case n as [ | n']. - apply contr_equiv_contr_contr. - apply istrunc_equiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HProp.