Definition K_0_map {M N:ExactCategory} (F:ExactFunctor M N) : monoidfun (K_0 M) (K_0 N). Proof. use (presented_abgrfun (π₀_map (functor_on_objects F))). intros g h. use hinhfun. intros [E [e e']]. exists (applyFunctorToShortExactSequence F E). now induction (!e), (!e'). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.