That's pretty much exactly it! The other thing to note is that the reduction semantics of codata are to... just sit there until it's consumed. If you use Haske

That's pretty much exactly it! The other thing to note is that the reduction semantics of codata are to... just sit there until it's consumed. If you use Haskell you get the idea that codata just expands and expands because of the behavior of the repl and laziness. Sometimes, a better intuition is that it's more like a Python generator which must be yielded explicitly (by a recursive algorithm recurring on some data).