AddGrpCat.uliftFunctor =
  { obj := fun X => AddGrpCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      AddGrpCat.ofHom
        (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }