[Agda] Agda's coinduction incompatible with initial algebras

[Martin Escardo]

On 04/10/11 21:41, Martin Escardo wrote:
> (Domains with strict continuous maps are algebraicly compact with
> respect to continuous endo-functors.)
>
 > [...]
> It seems that you have shown that this extension of Agda with
> co-inductive types is actually an algebraicly compact extension of Agda.
>
> For the functor 1+(-), you get bi-natural numbers. By initiality, they
> have iteration, and by finality they have a point infty. Combining these
> two things, iterating infty-many times, you get fixed points, and so
> inhabitedness of all objects (by taking fixed points of identities).

In the above category, you get the so-called domain of lazy natural 
numbers for the 1+(-) functor:


                                        infty
                                 ...  /
                                2     ...
                                 \  /
                              1    succ(succ(_|_))
                               \  /
                           0     succ(_|_)
                            \   /
                             _|_

It seems that sharp, when interpreted in the above category, is doing 
lifting (?). But there is no way of making sense of lifting in the 
category of sets.

Martin