Lemma dirprodeq (A B : UU) (ab ab' : A × B) : pr1 ab = pr1 ab' -> pr2 ab = pr2 ab' -> ab = ab'. Proof. intros H H'. induction ab as [a b]. induction ab' as [a' b']; simpl in *. induction H. induction H'. apply idpath. Defined.