∀ (X : Type u_1ᵒᵖ) (X_1 : AddCommGrpCat),
  AddCommGrpCat.ofHom
      (Pi.addMonoidHom fun i =>
        (AddCommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.id X_1)).comp (Pi.evalAddMonoidHom (fun a => ↑X_1) i)) =
    CategoryTheory.CategoryStruct.id (AddCommGrpCat.of (Opposite.unop X → ↑X_1))