[Agda] Agda's coinduction incompatible with initial algebras

[Dan Doel]

On Tue, Oct 4, 2011 at 7:33 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
> The problem, as I see it, is that sized types doesn't work with coinduction,
> which we already knew.

I've never looked into sized types much. Are we supposed to be able to
apply a function whose termination is justified by decreasing size to
a value whose size is ∞? Because that seems like part of the conflict
here: infinite coinductive values get an infinite size, but then we're
allowed to fold them anyway because the fold decreases the size (from
∞ to ∞ at each step :)).

Of course, the way that Mu becomes Nu when applied to a particular
functor is also weird.

-- Dan