# Idontgetoutmuch’s Weblog

Mathematical Notes

## 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 $<F,f>$ is an initial $T$-algebra with respect to the sub-category of strict maps if and only if $<F,f^{-1}>$ 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.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 27, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 20, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.8670603632926941, "perplexity_flag": "head"}