proposition: Lemma right_inv_epi_is_left_inv {C : category} {x y : C} (f : x --> y) (f_is_epic : isEpi f) (g : y --> x) (is_right_inv : f · g = identity _) : g · f = identity _.
proof: Proof. apply (maponpaths (fun k => k · f)) in is_right_inv. rewrite id_left in is_right_inv. rewrite <- id_right in is_right_inv. rewrite <- assoc in is_right_inv. apply f_is_epic in is_right_inv. apply is_right_inv. 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