Theorem weqhfibercoprodf2 {X Y X' Y' : UU} (f : X -> X') (g : Y -> Y') (y' : Y') : weq (hfiber g y') (hfiber (coprodf f g) (ii2 y')). Proof. intros. set (iy := @ii2 X Y). set (iy' := @ii2 X' Y'). set (fpg := coprodf f g). set (fpgiy := λ y : Y, (fpg (iy y))). assert (w1 : weq (hfiber g y') (hfiber fpgiy (iy' y'))) by apply (samehfibers g iy' (isinclii2 _ _) y'). assert (w2 : weq (hfiber fpgiy (iy' y')) (hfiber fpg (iy' y'))). { split with (hfibersgftog iy fpg (iy' y')). unfold isweq. intro y. set (u:= invezmaphf iy fpg (iy' y') y). assert (is : isweq u) by apply isweqinvezmaphf. apply (iscontrweqb (make_weq u is)). induction y as [ xy e ]. induction xy as [ x0 | y0 ]. simpl. apply (fromempty ((negpathsii1ii2 (f x0) y') e)). simpl. apply iscontrhfiberofincl. apply (isinclii2 X Y). } apply (weqcomp w1 w2). Defined.