Theorem isweqcoprodf {X Y X' Y' : UU} (w : X ≃ X') (w' : Y ≃ Y') : isweq (coprodf w w'). Proof. intros. set (finv := invmap w). set (ginv := invmap w'). set (ff := coprodf w w'). set (gg := coprodf finv ginv). assert (egf : ∏ xy : X ⨿ Y, (gg (ff xy)) = xy). intro. induction xy as [ x | y ]. simpl. apply (maponpaths (@ii1 X Y) (homotinvweqweq w x)). apply (maponpaths (@ii2 X Y) (homotinvweqweq w' y)). assert (efg : ∏ xy' : coprod X' Y', (ff (gg xy')) = xy'). intro. induction xy' as [ x | y ]. simpl. apply (maponpaths (@ii1 X' Y') (homotweqinvweq w x)). apply (maponpaths (@ii2 X' Y') (homotweqinvweq w' y)). apply (isweq_iso ff gg egf efg). Defined.