This is, I'm afraid, another question that MSE couldn't answer.
It's easy to see how inductively-defined data types correspond to least fixed points. Let's take the natural numbers as an example, whose constructors are $0 : \mathbb N$ and $s : \mathbb N \to \mathbb N$. Define the operation $F(X) = \{0\} \cup \{ s(n) : n \in X \}$, which applies the constructors to all elements of $X$. The Knaster–Tarski fixed point theorem says that the least fixed point of $F$ is $\bigcap\{ X : F(X) \subseteq X \}$.
What does that set mean? Well, it's the intersection of all sets such that applying the constructors doesn't give you anything new. So, since applying the constructors throws in $0$, $0$ must be in there. Since applying the constructors throws in every successor, every successor must be in there. The minimality property ensures that there are no more elements in there, so induction holds for this set. So it's the natural numbers.
Okay, great. Something similar is going to work for other inductive datatypes too. This indicates we can consider inductively defined datatypes as $\subseteq$-least fixed points for the set operation that applies all the constructors.
But what about coinductive data types? I've heard it said, though I'm not sure anywhere reliable, that codata corresponds to greatest fixed points. Let's go look at Knaster-Tarski again: the greatest fixed point is $\bigcup \{ X : X \subseteq F(X) \}$. What does this tell us? Well, promisingly, it says that every element is either $0$ or a successor. Certainly all of the natural numbers are in this greatest fixed-point. From what I know about coinduction, I'm expecting to get the natural numbers plus a unique fixed point of the successor.
But why should the successor have a unique fixed point? Why can't we have two, violating coinduction? Certainly this depends on what $s$ is, precisely, but all we asked of $s$ when we were doing the inductive definition was that it was injective ("free" in some sense), which feels like a much lighter condition.
How do I ensure the right number of fixed points for the constructors? How do I recover the coinduction principle? Or is it just that the order for which these constructions are LFPs and GFPs respectively isn't subset inclusion?
Best Answer
You've got the levels mixed up a bit because you are thinking too set-theoretically. While it is likely that you can get the carrier sets of inductive and coinductive datatypes as least and greatest fixed points, respectively, you will still wonder where to get constructors, destructors, recursion and corecursion.
An inductive type corresponds to an initial algebra for a functor $F : \mathsf{Set} \to \mathsf{Set}$. For example, the natural numbers are the initial algebra for the functor $F(X) = 1 + X$ where $1$ is the singleton set and $+$ is disjoint sum. Similarly, the set of binary trees is the initial algebra for the functor $F(X) = 1 + X^2$. An initial algebra consists of a set $I$ and a structure map $i : F(I) \to I$. The structure map gives us the constructors for the datatype, and the initiality of $I$ gives a recursion principle. Let's look at this for binary trees:
the initial algebra for $F(X) = 1 + X^2$ is the set $T$ of finite binary trees. Its structure map $t : 1 + T^2 \to T$ can be decomposed into two parts. The first part $\mathsf{nil} : 1 \to T$ is the empty tree, and the second part $\mathsf{cons} : T^2 \to T$ is the constructor which takes two trees and puts them together into a new tree.
the initiality of $T$ says that, given any set $A$ and a map $a : 1 + A^2 \to A$ there is a unique algebra homomorphism $h : (T,t) \to (A,a)$. We decompose $a$ into an element $x_0 \in A$ and a map $g : A^2 \to A$. Then the initiality says that there is a unique map $h : T \to A$ such that $$h(\mathsf{nil}) = x_0$$ and $$h(\mathsf{cons}(u, v)) = g(h(u), h(v)).$$ This is just definition of $h$ by recursion on the structure of the tree.
Now let us look at final coalgebras, which ought to correspond to coinductive types (codata). For example, the final coalgebra for $F(X) = 1 + X$ is the set $\mathbb{N} \cup \lbrace \infty \rbrace$, the final coalgebra for $F(X) = 1 + X^2$ contains finite and infinite binary trees, while the final coalgebra for $F(X) = 2 \times X$ is the set of infinite binary streams. Again, the structure map of such a final coalgebra gives us the destructors for codata, while finality gives a way of constructing maps into the codata.
For example, consider the final coalgebra $S$ for $F(X) = 2 \times X$. The structure map $s : S \to 2 \times S$ decomposes into two maps $\mathsf{hd} : S \to 2$ and $\mathsf{tl} : S \to S$ which I am suggestively calling "head" and "tail". Finality of $S$ means that, given any set $A$ and a map $a : A \to 2 \times A$, there is a unique coalgebra homomorphism $\phi : (A,a) \to (S,s)$. If we decompose $a$ into $h : A \to 2$ and $t : A \to A$, then $\phi$ is the unique map satisying $$\mathsf{hd}(\phi(x)) = h(x)$$ and $$\mathsf{tl}(\phi(x)) = \phi(t(x)).$$ I hope I got that right.
So it is indeed the case that inductive datatypes are "least fixed points" and the coinductive datatypes are the "greatest fixed points", but in the categories of algebras and coalgebras, respectively.