So here we come to the case of co-inductive types. I can only for lack of time browse quickly through these definitions, that is you see here we define streams again as a maximal fixed point over an operator. And we can define the function Map over streams as the greatest fixed point of a given operator on relations.

---