Theorem isweqcoprodtoboolsum (X Y : UU) : isweq (coprodtoboolsum X Y). Proof. intros. set (f := coprodtoboolsum X Y). set (g := boolsumtocoprod X Y). assert (egf : ∏ xy : X ⨿ Y , (g (f xy)) = xy). induction xy. apply idpath. apply idpath. assert (efg : ∏ xy : total2 (boolsumfun X Y), (f (g xy)) = xy). intro. induction xy as [ t x ]. induction t. apply idpath. apply idpath. apply (isweq_iso f g egf efg). Defined.