Lemma homotweqinv' {X Y Z} (f:X->Z) (w:X≃Y) (g:Y->Z) : f ~ g ∘ w <- f ∘ invmap w ~ g. Proof. intros q x. simple refine (_ @ q (w x)). simpl. apply maponpaths, pathsinv0. apply homotinvweqweq. Defined.