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