Definition pathssec2id {X Y : UU} (s : X -> Y) (p : Y -> X) (eps : ∏ x : X, p (s x) = x) (x : X) : pathssec2 s p eps _ _ (idpath (s x)) = idpath x. Proof. intros. unfold pathssec2. unfold pathssec1. simpl. assert (e : ∏ X : UU, ∏ a b : X, ∏ p : a = b, (! p @ idpath _) @ p = idpath _). { intros. induction p0. simpl. apply idpath. } apply e. Defined.