Definition K_0_universal_map {M:ExactCategory} {G:abgr} (f : ob M -> G) : (∏ E:ShortExactSequence M, f(Ob2 E) = f(Ob1 E) + f(Ob3 E)) -> monoidfun (K_0 M) G. Proof. intros c. exact (invmap K_0_map_universal_property (f,,c)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.