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