Theorem twooutof3a {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isgf: isweq (g ∘ f)) (isg: isweq g) : isweq f. Proof. intros. set (gw := make_weq g isg). set (gfw := make_weq (g ∘ f) isgf). set (invg := invmap gw). set (invgf := invmap gfw). set (invf := invgf ∘ g). assert (efinvf : ∏ y : Y, f (invf y) = y). { intro y. assert (int1 : g (f (invf y)) = g y). { unfold invf. apply (homotweqinvweq gfw (g y)). } apply (invmaponpathsweq gw _ _ int1). } assert (einvff: ∏ x : X, invf (f x) = x). { intro. unfold invf. apply (homotinvweqweq gfw x). } apply (isweq_iso f invf einvff efinvf). Defined.