Theorem isweqcoprodcomm (X Y : UU) : isweq (coprodcomm X Y). Proof. intros. set (f := coprodcomm X Y). set (g := coprodcomm Y X). assert (egf : ∏ xy : _, (g (f xy)) = xy). intro. induction xy. apply idpath. apply idpath. assert (efg : ∏ yx : _, (f (g yx)) = yx). intro. induction yx. apply idpath. apply idpath. apply (isweq_iso f g egf efg). Defined.