[Agda] Agda's coinduction incompatible with initial algebras

[Nils Anders Danielsson]

On 2011-10-04 12:26, Andreas Abel wrote:
> I'd like to open a new round of false-golfing, below is my entry to the
> tournament.  My favorite target is Agda's coinduction mechanism.
> Partially it's flaws are known, but I cannot remember anyone presenting
> an outright proof of the absurdity.

Cool. However, you've only established that the present mechanism is
incompatible with sized types (and the usual kind of semantics of data
types, but this is not surprising). Can you do this without using sized
types?

By the way, if we ever find a light-weight language design incorporating
sized types and decide to incorporate it properly into Agda, then I
imagine that the present mechanism will be removed (or retrofitted as
sugar expanding into the new mechanism).

-- 
/NAD