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