Why do initial algebras correspond to data and final coalgebras to codata?

Question

If I understand correctly, we can model inductive data types as initial F-algebras and co-inductive data types as final F-coalgebras (for an appropriate endofunctor F) [1]. I understand that according to Lambek's lemma the initial algebras (and final coalgebras) are fixed point solutions of the isomorphism T ≅ F T, but I don't see why the initial algebra is the least fixed point, while the final coalgebra is the greatest fixed point. (Is it obvious that the isomorphism T ≅ F T has a solution?)

Also I'm not really clear on how are inductive and co-inductive data types defined in type theory. Are there any recommended resources on this topic and maybe their relationship to category theory?

Thank you!

Answer 1

My understanding is that, in principle, there may be many solutions to the fixed point equation T ≅ F T. By Lambek's lemma, the initial algebra, if it exists, is one of those fixed points. In fact it's the least fixed point.

There is a universal condition that defines the least fixed point, along the lines of there being a unique morphism to any other fixed point that satisfy certain commutation conditions.

In other words, not every fixed point defines the initial algebra.

The same argument applies to final coalgebras and greatest fixed points.

See, for instance, Least Fixed Point of a Functor .