Lemma two_of_six_implies_two_of_three {C : category} {W : morph_class C} (p : two_of_six W) : two_of_three W. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.