How to compute the terminal coalgebra (or initial algebra) of a given functor This is sort of a soft question. I'll start with an example. Fix a set $A$, and consider the functor $F\colon \mathbf{Set} \to \mathbf{Set}$, $F\colon X \mapsto A \times X$. Now, we know that the terminal $F$-coalgebra is the set $\mathrm{Stream}[A]$ of infinite sequences of elements of $A$, equipped with the head/tail function sending $(a_0, a_1,\ldots)$ to $\big( a_0, (a_1, a_2, \ldots) \big)$.
However, suppose I didn't know a priori that $\mathrm{Stream}[A]$ was the terminal $F$-coalgebra. How could I work out that it is? I've tried unpacking the definition of "terminal $F$-coalgebra", but it's not particularly enlightening. All it says is that: we need a set $Y$ with functions $\psi_1\colon Y \to A$, $\psi_2\colon Y \to Y$, such that for any set $X$ and functions $\varphi_1\colon X \to A$, $\varphi_2\colon X \to X$, there is a unique function $f\colon X \to Y$ satisfying:
$$\begin{align*}
    \varphi_1(x) &= \psi_1 \big( f(x) \big) \\
    f \big( \varphi_2(x) \big) &= \psi_2 \big( f(x) \big)
\end{align*}$$
From here, I don't see how to conclude $Y = \mathrm{Stream}[A]$. Any insight is appreciated.
 A: There actually is a general method of computing terminal coalgebras, at least for functors which preserve certain limits.
Let $C$ be a category with a terminal object $1$, and let $F\colon C\to C$ be a functor. Then there is an arrow $!\colon F(1)\to 1$, and an arrow $F(!)\colon F^2(1)\to F(1)$, and by induction $F^{n-1}(!)\colon F^n(1)\to F^{n-1}(1)$. Thus we get a diagram $$\dots \overset{F^3(!)}{\to} F^3(1)\overset{F^2(!)}{\to} F^2(1)\overset{F(!)}{\to} F(1)\overset{!}{\to} 1$$
If this diagram has a limit $L = \varprojlim F^n(!)$ in $C$ and $F$ preserves this limit, then the comparison morphism $F(L) = F(\varprojlim F^n(!)) \to \varprojlim F^{n+1}(!)\cong L$ is an isomorphism, and its inverse $L\to F(L)$ makes $L$ into a terminal coalgebra for $F$.
This is known as Adámek's theorem. See the nLab for details. If $F$ fails to preserve this limit, the construction can be generalized by iterating transfinitely. And of course this recipe can be dualized to construct initial algebras: start with the initial object, inductively apply $F$, and take the colimit.
Now in the case $C = \mathsf{Set}$ and $F\colon X\mapsto A\times X$, we have the diagram $$\dots \overset{F^3(!)}{\to} A\times A\times A\overset{F^2(!)}{\to} A\times A \overset{F(!)}{\to} A\overset{!}{\to} 1$$ where $F^n(!)\colon (a_0,a_1,\dots, a_n)\mapsto (a_0,\dots,a_{n-1})$. The limit of the diagram is $A^\mathbb{N}$, with its natural projection maps $\pi_n\colon A^{\mathbb{N}}\to A^n$ by $(a_n)_{n\in \mathbb{N}}\to (a_0,\dots,a_n)$.
Now $F(A^{\mathbb{N}}) = A\times A^{\mathbb{N}}$, and its comparison map $A\times A^{\mathbb{N}}\to A^{\mathbb{N}}$, given by $(a,(a_n)_{n\in \mathbb{N}})\mapsto (a,a_0,a_1,\dots)$, is indeed a bijection. Its inverse $A^{\mathbb{N}}\to A\times A^{\mathbb{N}}$ is the standard "head/tail" coalgebra structure on streams.
