proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Retracts