Lemma total2_paths_b {A : UU} {B : A -> UU} {s s' : ∑ x, B x} (p : pr1 s = pr1 s') (q : pr2 s = transportb B p (pr2 s')) : s = s'. Proof. intros. induction s as [a b]; induction s' as [a' b']; simpl in *. exact (two_arg_paths_b p q). Defined.