> Furthermore, even in Haskell, there is no such thing as the category of Haskell types[0] (because of things like divergence and partiality).

Divergence and partiality can easily be modeled by the category of complete partial orders and Scott-continuous maps. This is what you learn in, e.g., a course on domain theory and/or denotational semantics.

Andrej Bauer is mainly arguing that Hask isn't a category because no one has formally specified it. For example, we would need to come up with a policy on when two arrows are considered equal, and it's not clear what that notion of equality should be.