Lemma is_merely_split_monic_weq_precomp_is_surjection (m : A --> B) : is_merely_split_monic m <-> ∏ c : ob C, issurjective (@precomp_with _ _ _ m c). Proof. unfold is_split_monic. split. - intros is_split ?. apply (merely_split_monic_to_split_monic m). + apply isapropissurjective. + intro; apply is_split_monic_to_precomp_is_surjection. assumption. + assumption. - intros is_surjective. specialize (is_surjective _ (identity _)). refine (factor_through_squash _ _ is_surjective). + apply propproperty. + intro fib. apply hinhpr. exists (pr1 fib). apply (pr2 fib). 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.