Corollary isweqpathscomp0r {X : UU} (x : X) {x' x'' : X} (e' : x' = x'') : isweq (λ e : x = x', e @ e'). Proof. intros. set (f := λ e : x = x', e @ e'). set (g := λ e'' : x = x'', e'' @ (! e')). assert (egf : ∏ e : _, g (f e) = e). { intro e. induction e. induction e'. apply idpath. } assert (efg : ∏ e : _, f (g e) = e). { intro e. induction e. induction e'. apply idpath. } apply (isweq_iso f g egf efg). Defined.