4
$\begingroup$

The paper "CPS Translating Inductive and Coinductive Types" mentions that there is an isomorphism between inductive (mu) and coinductive (nu) types, which they use for their translation. It states that:

$$\neg\mu Z.A(\neg Z)\ \cong\ \nu Z.\neg A(Z)$$

...but it gives no more details about it. Is this isomorphism correct? Is it constructive? Where could I find more information about it?

I've spent several hours trying to prove (any side of) it on Coq, using the standard impredicative encodings for those (e.g., see here), but failed.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.