AddGrpCat.fullyFaihtfulForget₂ToAddMonCat =
  { preimage := fun {X Y} f => AddGrpCat.ofHom (AddMonCat.Hom.hom f),
    map_preimage := @AddGrpCat.fullyFaihtfulForget₂ToAddMonCat._proof_1,
    preimage_map := @AddGrpCat.fullyFaihtfulForget₂ToAddMonCat._proof_2 }