{n : trunc_index} {A B : TruncType n} (f : A <~> B) : path_trunctype f^-1 = (path_trunctype f)^. Proof. unfold path_trunctype; simpl. rewrite path_universe_V_uncurried. rewrite (path_sigma_hprop_V (path_universe_uncurried f)). refine (concat_p1 _ @ concat_1p _ @ _). refine (_ @ (ap inverse (concat_1p _))^ @ (ap inverse (concat_p1 _))^). refine (ap_V _ _). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HProp.