Final Coalgebra

Let $F:\mathcal{C}\to\mathcal{C}$ be an Endofunctor. A final coalgebra $(\nu_{F},\mathrm{unroll})$ is a Terminal Object in the category of $F$-Coalgebras.

Explicitly, this means that for any other coalgebra $\alpha:A\to F(A)$, there exists a unique coalgebra map $!:A\to\nu_{F}$ that commutes with the coalgebras.

Coinduction

Final coalgebras provide a categorical semantics for Coinductive Types.