[Agda] Agda's coinduction incompatible with initial algebras

[Dan Doel]

On Fri, Oct 7, 2011 at 2:11 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>
> 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).

No (not exactly anyway), initial algebras in Fam(D) are inductive
families (if I'm not mistaken).

Dybjer models (indexed) inductive recursive definitions as initial
algebras in a category like Fam(I)/D. The idea, I believe, is that the
category has not just indexed families as objects, but pairs of
indexed families and indexed maps from said family to another, the map
being the recursive part. Then, initial algebras for functors over
that category are inductive-recursive.

I'm not an expert, though, and Dybjer actually has two models of
induction-recursion: a 'restricted' one (which is what I described
above) and a general one, which is more complicated. And I don't fully
understand the difference. I'm also not sure how the above description
is supposed to handle T : U -> Set, instead of just T : U -> S for
some small type S.

-- Dan