proposition: Lemma CokernelUniqueness {M:PreAdditive} {x y z z' : M} {f : x --> y} {g : y --> z} {g' : y --> z'} : isCokernel' f g -> isCokernel' f g' -> iscontr (IsoArrowFrom g g').
proof: Proof. intros i j. apply iscontraprop1. - exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)). - induction (iscontrpr1 (pr2 j _ g (pr1 i))) as [p P]. induction (iscontrpr1 (pr2 i _ g' (pr1 j))) as [q Q]. use tpair. + exists q. exists p. split. * apply (CokernelIsEpi _ _ i). rewrite assoc. rewrite Q. rewrite P. rewrite id_right. reflexivity. * apply (CokernelIsEpi _ _ j). rewrite assoc. rewrite P. rewrite Q. rewrite id_right. reflexivity. + cbn. exact Q. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions