Sniffnoy comments on No coinductive datatype of integers

[Sniffnoy]

Though with the standard definitions, that requires some form of choice.