Definition K_0 (M:ExactCategory) : abgr := presented_abgr (π₀ (ob M)) (K_0_hrel M).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.