I'd say this is close, with a slight twist.

Insisting on a formal definition that would work across contexts is harmful. If someone comes up with one, that's nice (I doubt this). But even then, others might come up with "type systems" that fall outside of this definition and that's still perfectly fine.

The twist is that we do not need formal definition to talk about types across multiple contexts. I do not know what the best way to do this is, but the essay has some suggestions inspired by philosophy, which might be interesting precisely because they do not need clear formal definition.

His summary ends with:

"Rather than seeking the elusive definition of what is a type (which does not exist), I believe that we should look for innovative ways to think about and work with types that do not require an exact formal definition."

So he doesn't want to stop at your point 1, but rather wants to find generalizations that apply to the commonality between these variations.

I thought he was calling for exactly the opposite? A generalization that applies between contexts would require formal definition, no?

No. There may be some magic formal definition that would work between contexts. Until we have such a definition, though, he says it's better (at least between contexts) to work off of an informal, inexact definition, and to be aware that you are doing so.