proposition: Lemma precomp_with_epi_isincl {C : category} {A B : ob C} {f : A --> B} : isEpi f -> ∏ c, isincl (@precomp_with _ _ _ f c).
proof: Proof. intros is_epi ? ?. apply invproofirrelevance. intros z w. apply subtypePath; [intros ? ?; apply homset_property|]. apply (is_epi _ (hfiberpr1 _ _ z) (hfiberpr1 _ _ w)). exact (hfiberpr2 _ _ z @ !hfiberpr2 _ _ w). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Core.Functors