Definition prod_eqrel_pr1 {X X' : UU} (R : eqrel (X × X')) (x' : X') : eqrel X. Proof. use ((λ x y, R (x ,, x') (y ,, x')) ,, _). abstract ( repeat split; [ intros z z' z''; apply eqreltrans | intros z; apply eqrelrefl | intros z z'; apply eqrelsymm ] ). Defined.