Lemma eqrel_from_hreldirprod {X X' : UU} (R : hrel X) (R' : hrel X') (HR : isrefl R) (HR' : isrefl R') : eqrel_from_hrel (hreldirprod R R') = hreldirprod (eqrel_from_hrel R) (eqrel_from_hrel R'). Proof. apply funextfun. intro x. apply funextfun. intro x'. apply weqtopathshProp. apply logeqweq. - refine (minimal_eqrel_from_hrel _ (eqreldirprod (make_eqrel _ (iseqrel_eqrel_from_hrel _)) (make_eqrel _ (iseqrel_eqrel_from_hrel _))) _ _ _). intros y y' Hy. induction Hy as [Hy1 Hy2]. split; apply eqrel_impl; easy. - intros Hx R0 H. induction Hx as [Hx1 Hx2]. refine (eqreltrans R0 _ _ _ (Hx1 (prod_eqrel_pr1 R0 (pr2 x)) _) (Hx2 (prod_eqrel_pr2 R0 (pr1 x')) _)). + intros y y' Hy. apply H. split. * exact Hy. * apply HR'. + intros y y' Hy. apply H. split. * apply HR. * exact Hy. Qed.