Lemma ishfsqweqhfibersg'tof {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 (hfibersg'tof 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. unfold totalfun, total2asstor, 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 : _, d' (c0' z))). apply (isweqhomot _ _ (λ z : Z, (pathsinv0 (h1 z)))). apply (twooutof3c _ _ (pr2 a') (pr2 b')). apply (twooutof3a _ _ is1 (pr2 d')). Defined.