Lemma homotweqinv {X Y Z} (f:X->Z) (w:X≃Y) (g:Y->Z) : f ~ g ∘ w -> f ∘ invmap w ~ g. Proof. intros p y. simple refine (p (invmap w y) @ _); clear p. simpl. apply maponpaths. apply homotweqinvweq. Defined.