Lemma PEq_isEpi {c d : ob A} (f : c --> d) : isEpi f <-> (∏ (b : PseudoElem d), PFiber f b). Proof. split. - intros isE b. set (E := make_Epi _ _ isE). set (Pb := Abelian.Pullbacks A _ _ _ E b). set (isEpi1 := AbelianPullbackEpi2 E b Pb). set (E2 := make_Epi A _ isEpi1). use (make_PFiber _ _ (make_PseudoElem (PullbackPr1 Pb))). use make_PEq. + exact Pb. + exact E2. + use identity_Epi. + cbn. rewrite id_left. exact (! PullbackSqrCommutes Pb). - intros H. set (fib := H (make_PseudoElem (identity _))). set (P1 := PFiber_Elem fib). set (e := PEqEq (PFiber_Eq fib)). use isEpi_precomp. + exact (PEqOb (PFiber_Eq fib)). + exact (PEqEpi2 (PFiber_Eq fib) · P1). + cbn in e. rewrite id_right in e. rewrite assoc in e. use (isEpi_path A _ _ e). apply EpiisEpi. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.AbelianPushoutPullback. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.