Definition PEq_precomp_Epi {c d : A} (P : PseudoElem c) (E : Epi A d (PseudoOb P)) : PEq P (make_PseudoElem (E · P)). Proof. use make_PEq. - exact d. - exact (identity_Epi _). - exact E. - apply id_left. Defined.
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.