Theorem isweqrdistrtoprod (X Y Z : UU) : isweq (rdistrtoprod X Y Z). Proof. intros. set (f := rdistrtoprod X Y Z). set (g := rdistrtocoprod X Y Z). assert (egf: ∏ a, (g (f a)) = a). intro. induction a as [ d | d ]. induction d. apply idpath. induction d. apply idpath. assert (efg: ∏ a, (f (g a)) = a). intro. induction a as [ t x ]. induction x. apply idpath. apply idpath. apply (isweq_iso f g egf efg). Defined.