Lemma split_monic_is_monic (m : A --> B) : is_split_monic m -> isMonic m. Proof. intros is_split. apply (isMonic_postcomp _ m (pr1 is_split)). apply (transportf _ (!pr2 is_split)). apply identity_isMonic. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Retracts.