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