category theory

Isomorphic Types

/ Dominic Steinitz / Leave a comment

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.