[Agda] defining coinductive types

[Nils Anders Danielsson]

On 2013-12-16 20:36, Andreas Abel wrote:
> this looks like a kind of negative translation to me:
>
>        nu X. A * X
>    --> forall R. ((nu X. A * X) -> R) -> R
>    --> forall R. (mu X. (A -> R) + X) -> R
>
> Might be a way to work with coinductive types.  A bit of an
> inconvenience is that thus encoded coinductive types "up" the universe
> level.

This encoding also has the problem that certain forms of nesting aren't
supported. The type

   μA.νX. A × X

is encoded as

   μA.∀R. (μX. (A → R) + X) → R,

which isn't strictly positive.

(Currently Agda doesn't support μA.νX. A × X, but this should be fixed.)

-- 
/NAD