Lemma abgr_isCokernel_uniquenss {A B C : abgr} (f : abgr_category⟦A, B⟧) (h : abgr_category⟦B, C⟧) (H : f · h = ZeroArrow abgr_Zero A C) (t : ∑ ψ : abgr_category ⟦abgr_Cokernel_abgr f, C⟧, abgr_CokernelArrow f · ψ = h) : t = make_abgr_CokernelOut f h H. Proof. use total2_paths_f. - use monoidfun_paths. use funextfun. intros x. use (squash_to_prop (abgr_Cokernel_monoidfun_issurjective f x) (setproperty C _ _)). intros hf. rewrite <- (hfiberpr2 _ _ hf). exact (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) (hfiberpr1 _ _ hf)). - use proofirrelevance. use homset_property. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. 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.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. @ZeroArrowFrom abgr_category abgr_Zero A = abgrfunfromunit A.