AddCommMonCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddMonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddCommMonCat.instCategory._proof_1,
    comp_id := @AddCommMonCat.instCategory._proof_2, assoc := @AddCommMonCat.instCategory._proof_3 }