Theorem total2_paths_equiv {A : UU} (B : A -> UU) (x y : ∑ x, B x) : x = y ≃ x ╝ y. Proof. intros. exists (λ r : x = y, tpair (λ p : pr1 x = pr1 y, transportf _ p (pr2 x) = pr2 y) (base_paths _ _ r) (fiber_paths r)). apply (isweq_iso _ (λ pq, total2_paths_f (pr1 pq) (pr2 pq))). - intro p. apply total2_fiber_paths. - intros [p q]. simpl. apply (two_arg_paths_f (base_total2_paths q)). apply transportf_fiber_total2_paths. Defined.