Regarding 2, you're right of course about subcategories of Hask, but I'm more interested in completely different categories.
My question really boils down to this: given the Category class provided in this article, which mathematical categories occur as instances of this Category? Are they necessarily all subcategories of Hask?
I think the answer to that question is better understood in the dependently-typed literature. Haskell does not have easily accessible dependent types, but many of the techniques could be translated and would help to answer your question.
Offhandedly, I'd say you could model many categories of interest, but since you're working in a "challenging" of constructive logic there are a lot of limitations on what can be modeled. At the end of the day, your objects will always be Haskell types, but a lot can be encoded in those types.
Again, though, the DT literature is really where people are attacking this question. Haskell's Category is usually just used when there's a meaningful subcategory of Hask that you want to overload composition and identity on.
My question really boils down to this: given the Category class provided in this article, which mathematical categories occur as instances of this Category? Are they necessarily all subcategories of Hask?