(Infinite) streams can be seen as really fundamental codata constructions as well. They're `nu (a )`, so if you believe that both codata and products are necess

(Infinite) streams can be seen as really fundamental codata constructions as well. They're `nu (a )`, so if you believe that both codata and products are necessary then you have streams. A lot* of people have rejected the first of those for most of the history of mathematics, but nobody rejects the second. Thus, streams are exactly as popular as codata/anti-foundation is.