{n : trunc_index} {A : TruncType n} : path_trunctype (equiv_idmap A) = idpath. Proof. unfold path_trunctype; simpl. rewrite (eta_path_universe_uncurried 1). rewrite path_sigma_hprop_1. reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HProp.