Theorem weqfuntoprodtoprod (X Y Z : UU) : (X -> Y × Z) ≃ (X -> Y) × (X -> Z). Proof. intros. simple refine (make_weq _ (isweq_iso (@funtoprodtoprod X Y Z) (@prodtofuntoprod X Y Z) _ _)). - intro a. apply funextfun. intro x. apply idpath. - intro a. induction a as [ fy fz ]. apply idpath. Defined.