Theorem twooutofsixu {X Y Z K : UU} {u : X -> Y} {v : Y -> Z} {w : Z -> K} (isuv : isweq (funcomp u v)) (isvw : isweq (funcomp v w)) : isweq u. Proof. intros. set (invuv := invmap (make_weq _ isuv)). set (pu := funcomp v invuv). set (hupu := homotinvweqweq (make_weq _ isuv) : homot (funcomp u pu) (idfun X)). set (invvw := invmap (make_weq _ isvw)). set (pv := funcomp w invvw). set (hvpv := homotinvweqweq (make_weq _ isvw) : homot (funcomp v pv) (idfun Y)). set (h0 := funhomot v (homotweqinvweq (make_weq _ isuv))). set (h1 := funhomot (funcomp pu u) (invhomot hvpv)). set (h2 := homotfun h0 pv). set (hpuu := homotcomp (homotcomp h1 h2) hvpv). exact (isweq_iso u pu hupu hpuu). Defined.