Definition pathssec2 {X Y : UU} (s : X -> Y) (p : Y -> X) (eps : ∏ (x : X), p (s x) = x) (x x' : X) (e : s x = s x') : x = x'. Proof. intros. set (e' := pathssec1 s p eps _ _ e). apply (e' @ (eps x')). Defined.