[Agda] Agda's coinduction incompatible with initial algebras

[Peter Hancock]

On 06/10/2011 08:07, Thorsten Altenkirch wrote:
>
> Anyway, who needs non-strict positive definitions?
>

What does strictly positive mean? Does it mean: isomorphic
to a coproduct of hom-functors of some kind, like a container?

Do you think IR-functors, with large decode ("D") types, are
positive, strictly or otherwise?
They don't have a Sigma-Pi normal form.

(To me they make a great deal of sense, and provide one among
not many analyses of how universes of sets/indexed-sets arise.  Moreover they are
not only convenient but also entertaining.)

Hank