[Agda] how to type this?

[Martin Escardo]

Thorsten,

I love co-induction, and have published more than one paper with it (and 
moreover I said "prefer" and "if possible").

However, the definitions I want to write down in Agda are certainly not 
by co-induction, and hence the co-inductive structure would, I think, 
get on my way rather than help me.  However, it is perhaps better to 
have such a definition than none, so I am still hoping for an answer 
with or without coinduction. The question remains in any case out of 
scientific curiosity: can this be expressed without co-induction?

Cheers,
Martin



Thorsten Altenkirch wrote:
>> How can this be expressed in Agda (or in type theory) in the infinite 
>> case in a simple and mathematically elegant way? (I prefer to avoid 
>> co-induction if possible.)
> 
> I sense that there is a contradiction between " a simple and 
> mathematically elegant way" and "I prefer to avoid co-induction if 
> possible". It is always possible to code up coinductive definitions 
> using functions (the constructive literature is full of this), but I 
> think this is neither simple nor elegant.
> 
> Btw, Nisse was using the new implementation of coinduction which allows 
> you to mix inductive and coinductive defintions, see 
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Codatatypes 
> 
> We also have a recently rejected paper about this:
> http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html