[Agda] Agda's coinduction incompatible with initial algebras

[Thorsten Altenkirch]

On 7 Oct 2011, at 05:30, Dan Doel wrote:

> Induction-recursion is not (from what I've read) justified by functors
> over the category of types, but by functors over a related category.
> But their actions are supposed to be strictly positive there, I
> believe.

Do you mean that IR defs are containers in Fam(D)?

I don't think this is the case. If I remember correctly containers in Fam(D)
give rise to functors where the first component (e.g. U : D) does not depend
on the 2nd (eg T :  U -> Set).

Thorsten
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111007/757e4801/attachment.html