Definition K_0_class {M:ExactCategory} : ob M -> K_0 M := λ A, @presented_abgr_intro (π₀ M) _ (pi0pr _ A).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.