Definition pathsweq4 {X Y : UU} (w : X ≃ Y) (x x' : X) (e : w x = w x') : maponpaths w (invmaponpathsweq w x x' e) = e. Proof. intros. induction w as [f is1]. set (w := make_weq f is1). set (g := invmap w). set (ee := maponpaths g e). simpl in *. set (eee := maponpathshomidinv (g ∘ f) (homotinvweqweq w) x x' ee). assert (e1 : maponpaths f eee = e). { assert (e2 : maponpaths (g ∘ f) eee = ee). { apply maponpathshomid2. } assert (e3 : maponpaths g (maponpaths f eee) = maponpaths g e). { apply (maponpathscomp f g eee @ e2). } set (s := @maponpaths _ _ g (f x) (f x')). set (p := @pathssec2 _ _ g f (homotweqinvweq w) (f x) (f x')). set (eps := @pathssec3 _ _ g f (homotweqinvweq w) (f x) (f x')). apply (pathssec2 s p eps _ _ e3). } assert (e4: maponpaths f (invmaponpathsweq w x x' (maponpaths f eee)) = maponpaths f (invmaponpathsweq w x x' e)). { apply (maponpaths (λ e0: f x = f x', maponpaths f (invmaponpathsweq w x x' e0)) e1). } assert (X0 : invmaponpathsweq w x x' (maponpaths f eee) = eee). { apply (pathsweq3 w). } assert (e5: maponpaths f (invmaponpathsweq w x x' (maponpaths f eee)) = maponpaths f eee). { apply (maponpaths (λ eee0: x = x', maponpaths f eee0) X0). } apply (! e4 @ e5 @ e1). Defined.