Lemma isaset_merely_split_monic (m : A --> B) : has_homsets C -> isaset merely_split_monic. Proof. intro. apply isaset_total2; [auto|]. intro; apply hlevelntosn, propproperty. 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.