proposition: 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: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.ExactCategories.ExactCategories UniMath.Algebra.Groups UniMath.Algebra.Free_Monoids_and_Groups