Theorem weqfunfromcoprodtoprod (X Y Z : UU) : (X ⨿ Y -> Z) ≃ ((X -> Z) × (Y -> Z)). Proof. intros. simple refine ( make_weq _ (isweq_iso (@funfromcoprodtoprod X Y Z) (@prodtofunfromcoprod X Y Z) _ _)). - intro a. apply funextfun; intro xy. induction xy as [ x | y ]; apply idpath. - intro a. induction a as [fx fy]. apply idpath. Defined.