Theorem isweqcoprodasstor (X Y Z : UU): isweq (coprodasstor X Y Z). Proof. intros. set (f := coprodasstor X Y Z). set (g := coprodasstol X Y Z). assert (egf : ∏ xyz, (g (f xyz)) = xyz). intro xyz. induction xyz as [ c | z ]. induction c. apply idpath. apply idpath. apply idpath. assert (efg : ∏ xyz, (f (g xyz)) = xyz). intro xyz. induction xyz as [ x | c ]. apply idpath. induction c. apply idpath. apply idpath. apply (isweq_iso f g egf efg). Defined.