Definition pathssec1 {X Y : UU} (s : X -> Y) (p : Y -> X) (eps : ∏ (x : X) , p (s x) = x) (x : X) (y : Y) (e : s x = y) : x = p y. Proof. intros. apply (pathscomp0 (! eps x)). apply (maponpaths p e). Defined.