Corollary twooutof3c_iff_2 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) : isweq f -> (isweq g <-> isweq (g ∘ f)). Proof. intros i. split. - intro j. exact (twooutof3c f g i j). - intro j. exact (twooutof3b f g i j). Defined.