Lemma isweqhfibersg'tof {X X' Y Z : UU} (f : X -> Y) (f' : X' -> Y) (g : Z -> X) (g' : Z -> X') (hf : hfsqstr f f' g g') (x' : X') : isweq (hfibersg'tof f f' g g' hf x'). Proof. intros. set (is := pr2 hf). set (h := pr1 hf). set (a' := weqtococonusf g'). set (c' := make_weq _ is). set (d' := weqhfptohfpoverX' f f'). set (b0' := totalfun _ _ (hfibersg'tof f f' g g' h)). assert (h1 : ∏ z : Z, (d' (c' z)) = (b0' (a' z))). intro. unfold b0'. unfold a'. unfold weqtococonusf. unfold tococonusf. unfold totalfun, hfibersg'tof; simpl. assert (e : (pathsinv0 (h z)) = (pathscomp0 (pathsinv0 (h z)) (idpath (f' (g' z))))). apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath. assert (is1 : isweq (λ z : _, b0'(a' z))). apply (isweqhomot _ _ h1). apply (twooutof3c _ _ (pr2 c') (pr2 d')). assert (is2 : isweq b0'). apply (twooutof3b _ _ (pr2 a') is1). apply (isweqtotaltofib _ _ _ is2 x'). Defined.