Definition PEq_Diff {x y : ob A} {a a' : PseudoElem x} (f : x --> y) (H : PEq (PseudoIm a f) (PseudoIm a' f)) : PDiff f H. Proof. set (PA := (AbelianToAdditive A) : PreAdditive). use make_PDiff. - exact (make_PseudoElem (@to_binop PA _ _ (PEqEpi2 H · a) (PEqEpi1 H · (@to_inv (AbelianToAdditive A) _ _ a')))). - exact (PEq_Diff_Eq1 f H). - intros z0 g X. use (make_PEq _ _ (identity_Epi _)). + cbn. exact (make_Epi _ _ (to_inv_isEpi PA _ (EpiisEpi PA (PEqEpi1 H)))). + cbn. exact (PEq_Diff_Eq2 f H X). 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.