proposition: Theorem weqfuntoprodtoprod (X Y Z : UU) : (X -> Y × Z) ≃ (X -> Y) × (X -> Z).
proof: 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.
imports: UniMath.Foundations.PartC