agda-unimath
agda-unimath copied to clipboard
Streams
Early work on streams, the coinductive version of lists. As lists are currently used for finite-dimensional linear algebra, streams seem the natural candidate for infinite-dimensional objects such as polynomial algebras and power series. The reason streams should work better than functions N -> R, say, is that lists are also streams, and the image of lists in streams is a natural way to define objects of "finite support," such as naming the polynomials among all power series.
As someone actively working on power series and polynomials right now, I'll admit I don't yet see the appeal (as compared to N -> R). That may change as this gets filled out further, but my immediate reaction is, "I've been working on multiplication of power series in a way that depends crucially on being able to plug in indices; I don't see what this buys us."
On the other hand, I'm very deliberately trying to make sure that alternate approaches can be swapped in smoothly, that anything with an appropriate equivalence to N -> R will do, so I look forward to seeing what happens with this.