{n : trunc_index} {A B : TruncType n} {f : A <~> B} : ap trunctype_type (path_trunctype f) = path_universe_uncurried f. Proof. destruct A, B. cbn in *. cbn; destruct (path_universe_uncurried f). rewrite concat_1p, concat_p1. rewrite <- 2 ap_compose. apply ap_const. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HProp.