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. 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.
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.