Definition weqsecovercoprodtoprod {X Y : UU} (P : X ⨿ Y -> UU) : (∏ xy : X ⨿ Y, P xy) ≃ (∏ x, P (ii1 x)) × (∏ y : Y, P (ii2 y)). Proof. intros. use (weq_iso (secovercoprodtoprod P) (prodtosecovercoprod P)). - intro. apply funextsec. intro t. induction t; reflexivity. - intro a. apply pathsdirprod. + apply funextsec. apply homotrefl. + apply funextsec. apply homotrefl. Defined.