[Agda] defining coinductive types

Nils Anders Danielsson nad at cse.gu.se
Wed Dec 18 13:14:11 CET 2013

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.)


More information about the Agda mailing list