{X Y Z : Type} (f : X -> Y) (g : Y -> Z) `{IsEquiv _ _ g} : NullHomotopy (g o f) -> NullHomotopy f. Proof. intros [z e]. exists (g^-1 z). intros x; apply moveL_equiv_V, e. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma.