Now we can put natural numbers defined as from 0 jump 1, odd numbers from 1 jump 2, even numbers from 0 jump 2, and we can also define the function, which essentially zips two streams by interleaving one element from each. And now we come to the problem of how do we show the stream of natural numbers is obtained by interleaving the stream of even numbers with the stream of odd numbers? Well, here we apply co-induction. What we do is we characterise equality over streams as a maximal fixed point of a given operator and we show that a given relation is indeed a post fixed point of that operator. Now for this reason it means that all such objects are equal as streams but by looking at what it means that these are equal this is essentially the fact, this is essentially the assertion that nought is equal to even plus odd. You just need to expand it. Other interesting co-inductive types are binary streams. Here a nice exercise is to characterise as a maximal fixed point the predicate for a stream of being fair. And again you can see how to define finite and indefinite trees.

---