\section{Terminal game}
Notice that, by definition, $\Pf(\Her)$ is set-theoretically equal to $\Her$. Therefore, $\Her$ admits the canonical $\Pf$-algebra structure \[\id{\Her}:\Her \to \Pf(\Her)\] and $\Pf$-coalgebra structure \[\id{\Her}:\Pf(\Her) \to \Her.\]

\begin{proposition}
    $\Her$ is a game.
\end{proposition}
\begin{theorem}[Two characterizations of $\Her$]\label{TheoremTwoUniversalities}
$\Her$ has the following two universalities.
\begin{enumerate}
    \item $\Her$ is the initial $\Pf$-algebra.
    \item $\Her$ is the terminal game.
\end{enumerate}
\end{theorem}
\begin{proof}
    For the first universality, it's immediately followed by the adamek's construction of the initial algebra (\memo{cite}). In fact, $\Pf$ preserves the following colimit:
    \[
        \begin{tikzcd}
            \emptyset \ar[r]& \Pf(\emptyset) \ar[r]& \Pf(\Pf(\emptyset)) \ar[r]&\Pf(\Pf(\Pf(\emptyset))) \ar[r]&\dots \Her.
        \end{tikzcd}
    \]

    \memo{For (2), I will write later. It's proven just by induction.}
\end{proof}

\begin{remark}[Categorical Background: Taylor's theory of well-founded coalgebras]
\end{remark}

\begin{remark}[The terminal $\Pf$-coalgebra]
\memo{finite branching (but not necessarily finite time) rooted trees}
\end{remark}