Definition pathssec3 {X Y : UU} (s : X -> Y) (p : Y -> X) (eps : ∏ x : X, p (s x) = x) {x x' : X} (e : x = x') : pathssec2 s p eps _ _ (maponpaths s e) = e. Proof. intros. induction e. simpl. apply pathssec2id. Defined.