Lemma isweqhfibersgtof' {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 (hfibersgtof' 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 _ _ (hfibersgtof' f f' g g' h)). assert (h1 : ∏ z : Z, (d (c z)) = (b0 (a z))). intro. simpl. unfold b0. unfold a. unfold weqtococonusf. unfold tococonusf. simpl. unfold totalfun, total2asstor, hfibersgtof'; simpl. assert (e : (h z) = (pathscomp0 (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.