Lemma ishfsqweqhfibersgtof' {X X' Y Z : UU} (f : X -> Y) (f' : X' -> Y) (g : Z -> X) (g' : Z -> X') (h : commsqstr g' f' g f) (is : ∏ x : X, isweq (hfibersgtof' f f' g g' h x)) : hfsqstr f f' g g'. Proof. intros. split with h. set (a := weqtococonusf g). set (c0 := commsqZtohfp f f' g g' h). set (d := weqhfptohfpoverX f f'). set (b := weqfibtototal _ _ (λ x : X, make_weq _ (is x))). assert (h1 : ∏ z : Z, (d (c0 z)) = (b (a z))). intro. simpl. unfold b. 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 : _, d (c0 z))). apply (isweqhomot _ _ (λ z : Z, (pathsinv0 (h1 z)))). apply (twooutof3c _ _ (pr2 a) (pr2 b)). apply (twooutof3a _ _ is1 (pr2 d)). Defined.