In imperative code I would write it like:

    odd := {hd: 1}
    even := {hd: 0, tail: odd}
    odd.tail := even
    blink x := x ? odd : even

I guess the cofixpoint does that loop tying sort of like this?

    fix({odd, even} => {
      odd: {hd: 1, tail: even},
      even: {hd: 0, tail: odd}
    })

Is there something like a co-Y combinator to do this in pure languages?

Is the productivity condition sort of like the dual of the positivity restriction on inductive types?