AddGrpCat.uliftFunctorFullyFaithful =
  {
    preimage := fun {X Y} f =>
      AddGrpCat.ofHom
        (AddEquiv.ulift.toAddMonoidHom.comp ((AddGrpCat.Hom.hom f).comp AddEquiv.ulift.symm.toAddMonoidHom)),
    map_preimage := @AddGrpCat.uliftFunctorFullyFaithful._proof_1,
    preimage_map := @AddGrpCat.uliftFunctorFullyFaithful._proof_2 }