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