Theorem weqhfibercoprodf1 {X Y X' Y' : UU} (f : X -> X') (g : Y -> Y') (x' : X') : weq (hfiber f x') (hfiber (coprodf f g) (ii1 x')). Proof. intros. set (ix := @ii1 X Y). set (ix' := @ii1 X' Y'). set (fpg := coprodf f g). set (fpgix := λ x : X, (fpg (ix x))). assert (w1 : weq (hfiber f x') (hfiber fpgix (ix' x'))) by apply (samehfibers f ix' (isinclii1 _ _) x'). assert (w2 : weq (hfiber fpgix (ix' x')) (hfiber fpg (ix' x'))). { split with (hfibersgftog ix fpg (ix' x')). unfold isweq. intro y. set (u := invezmaphf ix fpg (ix' x') 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 iscontrhfiberofincl. apply (isinclii1 X Y). - apply (fromempty ((negpathsii2ii1 x' (g y0)) e)). } apply (weqcomp w1 w2). Defined.