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