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