[Agda] Agda's coinduction incompatible with initial algebras

[Thorsten Altenkirch]

Yes, I was including IR definitions.

In Agda this actually corresponds to the simple syntactic condition that Pi-types
are guardedness preserving in the 2nd argument but not the first.

I don't know what the semantic counterpart to this is.

We don't even know what the container form for inductive-inductive definitions are.
Peter Morris and I looked at this recently.

Thorsten

On 6 Oct 2011, at 23:47, Peter Hancock wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda