Lemma faithful_reflects_epis {C D:precategory} (U:functor C D) (hU:faithful U) {a b:C} (f:C⟦a,b⟧) : isEpi (#U f) -> isEpi f. Proof. intros hf c u v huv. eapply invmaponpathsincl. apply hU. cbn. apply hf. rewrite <- functor_comp, <- functor_comp. now rewrite huv. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Coequalizers.