proposition: Lemma two_of_six_implies_two_of_three {C : category} {W : morph_class C} (p : two_of_six W) : two_of_three W.
proof: Proof. unfold two_of_three. intros. split. - intros. rewrite <- (id_right f) in X. rewrite <- (id_left g) in X. pose (p _ _ _ _ _ _ _ (pr1 X) (pr2 X)). rewrite id_right in d. apply (pr222 d). - split. intros. destruct X as [ X1 X2 ]. rewrite <- (id_left f) in X1. pose (p _ _ _ _ _ _ _ X1 X2). apply (pr122 d). intros. destruct X as [ X1 X2 ]. rewrite <- (id_right g) in X1. pose (p _ _ _ _ _ _ _ X2 X1). apply (pr1 d). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos