Lemma is_nat_trans_epi_from_pointwise_epis (C D : precategory) (hs : has_homsets D) (F G : ob (functor_precategory C D hs)) (α : F --> G) (H : ∏ a : ob C, isEpi (pr1 α a)) : isEpi α. Proof. intros G' β η H'. use (nat_trans_eq hs). intros x. set (H'' := nat_trans_eq_pointwise H' x). cbn in H''. apply (H x) in H''. exact H''. 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.