Lemma dirprod_paths {A : UU} {B : UU} {s s' : A × B} (p : pr1 s = pr1 s') (q : pr2 s = pr2 s') : s = s'. Proof. intros. induction s as [a b]; induction s' as [a' b']; simpl in *. exact (two_arg_paths p q). Defined.