[Agda] Positive but not strictly positive types

[Martin Escardo]

On 10/04/15 01:21, Martin Escardo wrote:
> More interestingly, phi is also a final coalgebra. But I will skip
> this here, so that you have something to think about yourself. :-)

Actually, what I meant to say is that (N->2) is the final coalgebra.

Because we have ((N->2)->2) ~ N, exponentiating on both sides with
base 2, we get

 (((N->2)->2)->2) ~ (N->2).

So N->2 is another fixed point of ((- -> 2) -> 2), this time in such a
way as to get a final coalgebra.

Martin