Lemma K_0_map_universal_property {M:ExactCategory} {G:abgr} : monoidfun (K_0 M) G ≃ ∑ f : ob M -> G, ∏ E:ShortExactSequence M, f(Ob2 E) = f(Ob1 E) + f(Ob3 E). Proof. apply (weqcomp (presented_abgr_universal_property (K_0_hrel M) G)). apply (weqtotal2 π₀_universal_property). intros h. apply weqiff. + split. * intros i E. exact (i _ _ (K_0_related E)). * intros k w w' r. apply (squash_to_prop r (setproperty _ _ _)). clear r; intros [E [e e']]. induction (!e), (!e'); clear e e'. exact (k E). + apply isapropiscomprelfun. + apply impred_isaprop; intros E. apply setproperty. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.