It's not redundant. As you point out: selecting rows _before_ aggregation and _after_ are different beasts. You can't exclude rows from aggregation with HAVING.
In theory¹ a DB that supports skip-scanning could use feedback from some HAVING clauses to short-circuit such a scan significantly, for instance if HAVING COUNT(*)<4 is present and a fourth row for that grouping comes up it can discard the row and skip to the next value. This would likely only be useful for indexes containing large numbers of the same few values though.
[1] I'm not aware of any engine that does this. It might be that the time cost of assessing if the optimisation is worthwhile² far outways the sum benefit over time of the saving when it is actually found to be worthwhile.
[2] Similarly, writing+testing+maintaining the code to do so might not be good use of dev time compared to other improvements
I will post the link later, if necessary in a comment.
SELECT x ... HAVING y => SELECT * FROM (x ...) t WHERE yOne inner σ (WHERE) and one outer σ (HAVING).
If subqueries are allowed, then you don't need that.