Lemma precomp_with_epi_isincl {C : category} {A B : ob C} {f : A --> B} : isEpi f -> ∏ c, isincl (@precomp_with _ _ _ f c). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Core.Functors.