{X Y : Type} {f g : X -> Y} (p : f == g) : NullHomotopy f -> NullHomotopy g. Proof. intros [y e]. exists y. intros x; exact ((p x)^ @ e x). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma.