{n : trunc_index} {X Y : Type} (f : X -> Y) `{IsTrunc n Y} : IsTrunc n (NullHomotopy f). Proof. apply @istrunc_sigma; auto. intros y. apply (@istrunc_forall _). intros x. apply istrunc_paths'. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma.