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.