proposition: Corollary twooutof3c_iff_1_homot {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (h : X -> Z) : g ∘ f ~ h -> isweq g -> (isweq f <-> isweq h).
proof: Proof. intros r i. apply (logeq_trans (Y := isweq (g ∘ f))). - apply twooutof3c_iff_1; assumption. - apply isweqhomot_iff; assumption. Defined.
imports: UniMath.Foundations.Preamble