The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

On Thu, Sep 17, 2009 at 4:27 PM, Edsko de Vries 
<edskodevries AT gmail.com>
 wrote:
> CoInductive T : Set :=
>  | A : T
>  | B : T
>  | C : T -> T.
>
> Now there are terms that live in T such as
>
>  C (C (C ... A))
>  C (C (C ... B))
>
> with infinitely many C's followed by an A or a B. However, it seems to me
> that these terms are not (constructively) definable.

This is false, there are no such elements of T. (I presume we are just
talking about the interpretation of type theory in sets, but it
doesn't really matter, there just aren't any such elements in any
model.)  Because T is by definition the final coalgebra for the
functor F(X) = {A} union {B} union {C(x) | x in X} a short calculation
shows that the final coalgebra is

T = {C^n(A) | n >= 0} union {C^m(B) | m >= 0} union {C^omega}

where n and m are non-negative integers.

With kind regards,

Andrej