equiv_path_trunctype' {n : trunc_index} (A B : TruncType n) : (A = B :> Type) <~> (A = B :> TruncType n). Proof. refine ((equiv_ap' issig_trunctype^-1 _ _)^-1 oE _). exact (equiv_path_sigma_hprop (_;_) (_;_)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HProp.