∀ (X : AddCommMonCatᵒᵖ),
  { app := fun N => AddCommMonCat.ofHom (AddCommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id X).unop).compHom',
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { obj := fun N => AddCommMonCat.of (↑(Opposite.unop X) →+ ↑N),
        map := fun {X_1 Y} f => AddCommMonCat.ofHom (AddMonoidHom.compHom (AddCommMonCat.Hom.hom f)), map_id := ⋯,
        map_comp := ⋯ }