Isomorphic Types

Nothing to do with differential geometry but there was a question on the haskell-cafe mailing list asking for “a proof that initial algebras & final coalgebras of a CPO coincide”. I presume that means a CPO-category.

A category is a CPO-category iff

• There is a terminator, 1.
• Each hom-set, ${\rm Hom}(A,B)$, is a CPO with a bottom.
• For any three objects, arrow composition ${\rm Hom}(A,B) \times {\rm Hom}(B,C) \longrightarrow {\rm Hom}(A,C)$ is strict continuous.
• Idempotents split, that is, if $f\circ f = f$ then $f= u\circ d$ and $d\circ u = 1$.

The following lemma answers the poster’s question.

Lemma
If $T$ is a covariant endofunctor on a CPO-category, then $$ is an initial $T$-algebra with respect to the sub-category of strict maps if and only if $$ is a final $T$-co-algebra.

Proof
See Freyd.

We can do a bit more. We borrow some notation from Meijer, Fokkinga and Paterson. If, for a given functor, the initial algebra exists and $\phi : FA \longrightarrow A$ is an algebra then we denote the unique arrow from the initial algebra to this algebra as $(\![\phi]\!)$. Dually, if for a given functor, the final co-algebra exists and $\phi : A \longrightarrow FA$ is a co-algebra then we denote the unique arrow to the final co-algebra as ${[\!(\phi)\!]}$.

Theorem
In a CPO-category, if $\phi : TA \longrightarrow A$ is an isomorphism then $(\![\phi]\!) \circ {[\!({\phi^{-1}})\!]} = 1$ and ${[\!({\phi^{-1}})\!]} \circ (\![\phi]\!) = 1$.

Proof
Let $a : TA \longrightarrow A$ be the initial $T$-algebra and let $b : B \longrightarrow TB$ be the final $T$-co-alegebra. Then by the above lemma, we have that $A=B$ and $b=a^{-1}$. We also have

Since there is only one arrow from the initial algebra to itself $1_A$ then we must have ${[\!({\phi^{-1}})\!]} \circ (\![\phi]\!) = 1$.

For the other way, there is always a morphism from the algebra $\phi : TC \longrightarrow C$ to the initial algebra. Therefore, $\phi : TC \longrightarrow C$ must be isomorphic to the initial algebra.