Reals as final coalgebra (exercise)

[Tom Leinster <T.Leinster@dpmms.cam.ac.uk>]

Fans of the characterization of the real interval as a final coalgebra might
be interested to see the exercise I set the Part III (first year graduate)
students in Cambridge taking this year's Category Theory course.  It's a bit
too cumbersome to reproduce in plain text, but can be found as the last
question on sheet 3 at

http://www.dpmms.cam.ac.uk/~leinster/categories

and consists of a guided proof of the fact that the closed real interval is
terminal in a certain category of coalgebras.

I tried to make the exercise as quick and easy as possible, which is why
there is no mention of the wedge product, nor orderings, nor digital
expansions.  I don't know whether this (particularly the omission of the
wedge) is at some cost to understanding.  If anyone has any suggestions as to
how the exercise might be made more transparent then I'd be interested to
hear; I'm aware that there are plenty of people on this list who have a
deeper understanding of this result than I do.

Flagged "highly optional" as it was, no-one as far as I'm aware has actually
tried *doing* this question...

Tom