Corollary twooutof3c_iff_2_homot {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (h : X -> Z) : g ∘ f ~ h -> isweq f -> (isweq g <-> isweq h). Proof. intros r i. apply (logeq_trans (Y := isweq (g ∘ f))). - apply twooutof3c_iff_2; assumption. - apply isweqhomot_iff; assumption. Defined.