\documentclass{amsart}
\usepackage[left=2cm, right=2cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsfonts, amsthm, amssymb, mathtools,etoolbox}
\usepackage{blindtext}
\usepackage[colorlinks=true, urlcolor=blue, linkcolor=blue, citecolor=blue]{hyperref}
\usepackage{tikz,tikz-cd}
\usepackage{array}
\usepackage[style=alphabetic,sorting=nyt]{biblatex}
\renewbibmacro{in:}{}
% \addbibresource{biblio.bib}
\addbibresource{CommonBiblio20240922.bib}
\addbibresource{GamesAsWellFoundedCoalgebras.bib}
\tikzset{pullback/.style={minimum size=1.2ex,path picture={
\draw[opacity=1,black,-,#1] (-0.5ex,-0.5ex) -- (0.5ex,-0.5ex) -- (0.5ex,0.5ex);%
}}}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{todo}[theorem]{Todo}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}

\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{question}[theorem]{Question}
\newtheorem{idea}[theorem]{Idea}

\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{red}{memo: #1}}
\newcommand{\invmemo}[1]{\textcolor{blue}{memo: #1}}
\newcommand{\para}[1]{\paragraph{\textbf{#1}}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Func}[2]{[#1,#2]}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\demph}[1]{\textbf{#1}}
\newcommand{\ob}{\mathrm{ob}}


\newcommand{\X}{\mathbb{X}}
\newcommand{\Y}{\mathbb{Y}}
\newcommand{\W}{\mathbb{W}}
\newcommand{\gS}{\mathbb{S}}
\newcommand{\A}{\mathbb{A}}
\newcommand{\I}{\mathbb{I}}
\newcommand{\Pf}{\mathcal{P}_{\mathrm{fin}}}
\newcommand{\Gs}{\mathbf{Games}}
\newcommand{\nsum}{\oplus}
\newcommand{\Alg}[1]{\mathbf{Alg}_{#1}}
\newcommand{\Coalg}[1]{\mathbf{Coalg}_{#1}}
\newcommand{\RecCoalg}[1]{\mathbf{RecCoalg}_{#1}}
\newcommand{\PfAlg}{\Alg{\Pf}}
\newcommand{\PfCoalg}{\Coalg{\Pf}}
% \newcommand{\mex}[1]{\mathrm{mex}(#1)}
\newcommand{\mex}{\mathrm{mex}}
\newcommand{\xem}{\mathrm{xem}}
\newcommand{\hylo}{\mathrm{hylo}}
% \newcommand{\G}[2]{\mathcal{G}_{#1}(#2)}
\newcommand{\G}{\mathcal{G}}
\newcommand{\rel}{\to}
\newcommand{\red}{\mathrm{red}}
\newcommand{\cp}{\ast}
\newcommand{\acc}{\rightsquigarrow}
\newcommand{\str}{\theta}
\newcommand{\Image}{\mathrm{Im}}
\newcommand{\HF}{\mathbb{HF}}
\newcommand{\Nim}[1]{\mathrm{Nim}_{#1}}
\renewcommand{\H}{\mathbb{H}}
\newcommand{\epi}{twoheadrightarrow}
\newcommand{\mono}{rightarrowtail}
\newcommand{\RB}{\mathcal{R}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\rd}{\mathrm{rd}}
\newcommand{\ADJ}[4]
    {
    \begin{tikzcd}[ampersand replacement = \&, column sep = small]
        {#1}
        \ar[rr, shift right=1.3ex, "{#2}"']
        \&\perp\&
        {#3}
        \ar[ll, shift right=1.3ex,"{#4}"']
    \end{tikzcd}
    }
\DeclarePairedDelimiter{\gen}{\langle}{\rangle}
\newcommand{\oc}{\mathsf{Outcome}}

\title{Games as recursive coalgebras\\ A categorical derivation and generalization of Nim-sum}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo}}
% \date{\today}
\subjclass[2020]{MSC}
\keywords{Keywords}


\begin{document}
\begin{abstract}
    
\end{abstract}
\maketitle
\tableofcontents
\section{Introduction}

\para{Context in combinatorial game theory}
Bouton's classical result \cite{bouton1901nim}\footnote{This is published in 1901, not 2001.} provides a winning strategy of Nim, with the notion of \demph{Nim-sum}.
\begin{definition}
    A \demph{Nim-sum} of two natural numbers is the bit-wise excluded disjunction.
\end{definition}
For example, the Nim-sum of $3$ and $5$ is $6$. Later, Nim-sum is proven to be important not only for Nim, but also for general combinatorial game theory. (See textbooks on combinatorial game theory, including \cite{siegel2013combinatorial}.)

This paper provides a convenient categorical framework for combinatorial game theory, and as its application, de

\para{Context in category theory} 

History:
\url{https://ncatlab.org/nlab/show/game+theory}



Category of games
\begin{itemize}
    \item \cite{joyal1977remarques}
    \item \cite{blass1992game}
    \item \cite{laird2013constructing}
\end{itemize}

Recursive coalgebras
\begin{itemize}
    \item Paul Taylor defined it.  \cite{taylor1999practical}
    \item Well-foundedness and recursiveness \cite{adamek2020well}
\end{itemize}

\para{Context in Logics and computer science}
\para{Conway's appendix}

\textbf{Acknowledgement}
% I would thank to my supervisor Ryu Hasegawa for his continuous supports and advices and also for suggesting me to consider hylomorphisms in this context, which turns out to be crucial.

% I would like to thank Ryo Suzuki, for suggesting me to consider Nim-sum through the Ackermann interpretation.

% I would like to thank my appreciation to Tomoaki Abuku, Suetsugu, Paul Taylor, Takeshi Tsukada, Kazuyuki Asada, Keisuke Hoshino for thier discussions.

% I extend my graditude for Syoei Suzuki for discussion.


I would like to express my gratitude to my supervisor, Ryu Hasegawa, for his continual support and guidance, and for suggesting that I consider hylomorphisms in this context, which proved to be essential.

I am also grateful to Ryo Suzuki for recommending the use of Nim-sum through the Ackermann interpretation.

My appreciation extends to Tomoaki Abuku, Suetsugu, Paul Taylor, Takeshi Tsukada, Kazuyuki Asada, Syoei Suzuki, Kyosuke Higashida, and Keisuke Hoshino for their valuable discussions.

% Finally, I would like to thank Syoei Suzuki, Kyosuke Higashida for engaging in discussions with me.


Throughout this paper, $\N$ denotes the set of all non-negative integers $\N = \{0,1,2, \dots\}$.

\para{Motivation to consider recursive coalgebras?}
\begin{description}
    \item[Philosophical motivation] motivation is that combinatorial game theory is inherently recursive. \memo{Write about Conway's word}
    \item[Game-theoretic] Why nim-sum works?
    \item[Categorical] locally finitely presentable + epi-mono factorization + subonject classifier
\end{description}


\subsubsection{Related works}
Categories that subsume our category: 
\begin{itemize}
    \item The category of Kripke models and p-morphisms.
    \item The category of game graphs.
\end{itemize}


\memo{compare with \cite{bavsic2024categories}}

Category of games
%\newpage
\section{Games as graphs}
In this section, we recall \dq{classical} game-theoretic notions and phenomena, which will be reinterpreted and generalized later. \memo{See \cite{siegel2013combinatorial} for details.}

\subsection{Elementary definition of Games}
There are so many different definitions of impartial games. \memo{add bib} In this paper, we adopt a graph-theoretic one. Informally speaking, a vertex is a state of the game, and an edge is a possible move.
\begin{definition}[(impartial) games]\label{DefinitionGames}
    A \emph{game} $\X$ is a pair $\X = (X, \rel)$ of a (possibly infinite) set $X$ and a relation $\rel\subset X \times X$ that satisfies two finiteness conditions:
    \begin{enumerate}
        \item (finite options) For any $x \in X$, the number of options $\# \{x' \in X \mid x\rel x'\}$ is finite.
        \item (finite time) There is no infinite path. $x_0 \rel x_1 \rel x_2 \rel \dots$
    \end{enumerate}
\end{definition}

To win a given game, we need to know \dq{$N$-states} (Next-player-winning states) and \dq{$P$-states} (Previous-player-winning states), defined as follows. The following definition is not circuler, due to the \dq{finite time} condition.
% its winning states and losing states.
\begin{definition}[Outcome]\label{DefinitionOutcome}
    For a game $\X=(X, \rel)$ and its state $x\in X$,
    the outcome of $x$ is recursively defined by
    \[
    \oc(x)\coloneqq
    \begin{cases}
        N& \text{(if there exists $x\rel x'$ whose outcome is $P$.)}\\
        P& \text{(otherwise)}
    \end{cases}
    \]
\end{definition}

We end this subsection by giving several famous examples of combinatorial games.

\begin{example}[Nim]\label{ExampleNim}
    Let $\Nim{n}$ denote a nim game with $n$-heaps. In our formulation, it is $(\N^{n}, \rel)$, where $(a_1, \dots a_n)\rel (b_1, \dots b_n)$ if and only if there exists $1\leq i \leq n$ such that $a_i > b_i$ and for any $j \neq i$, $a_j = b_j$.
\end{example}

\begin{theorem}[Bouton's theorem]
    
\end{theorem}

\begin{example}[Subtraction Game]\label{ExampleSubtractionGame}
\memo{Write!}
\end{example}

\begin{example}[Wythoff]\label{ExampleWythoff}
\memo{Write!}
\end{example}

The next example is not well-known (at least in the following form), but will turn out to be theoretically important and is worth being called \emph{the universal game}.
\begin{example}[The terminal game: Binary exponent nim]\label{ExampleTheUniversalGameInTermsOfNumbers}
% The underlying set of the universal game is g
% \end{example}
% \begin{remark}[The universal game of natural numbers]
    % Since the terminal object is defined by universality, it is unique up to canonical isomorphism. Another description of the terminal object is given by \emph{Ackerman's interpretation} of hereditarily finite sets. \memo{ref}
    The underlying set of the binary exponent nim is $\N$, and the relation $n \rel m$ is defined by
    \[n \rel m \iff 2^m \text{ appears in the binary expansion of }n.\]
    For example, when $n=10000$, since
    \[
    n=10000=2^{13}+2^{10}+2^{9}+2^{8}+2^{4},
    \]
    there are $5$ possible moves, namely $10000\rel4,8,9,10,13$.
    The state $n=10000$ is $N$-state, because the next player can move to $8$, then the other player has no choice other than moving to $3$, and the last move $3\to 0$ terminates the game. 

    Later, we will observe that this game is universal, in the following senses:
    \begin{itemize}
        \item This game is the terminal object of the category of games.
        % $\Gs$.
        \item This is the universal \dq{recursively defined data} of games
        \item Every state of every game is canonically \dq{equivalent} to the unique state (i.e., natural number) of this game.
    \end{itemize}
    \memo{write the game!}
    
    \memo{"almost all states are N-state"}

    \memo{Is it related to the product-exp description of games?}
\end{example}

\begin{example}[The universal game: Hereditarily finite sets]\label{ExampleHereditarilyFiniteSets}
    
\end{example}

\begin{definition}[Birthday]
    
\end{definition}

\subsection{Game addition and Grundy number}

\begin{definition}[mex]
    For a finite set of natural numbers $S\subset \N$, $\mex(S)$ is the minimum natural number that does not belong to the subset $S$. In other words, mex of $S$ is the minimum element of the complement of $S$:
\[\mex(S) = \min S^{\mathrm{c}}.\]
\end{definition}

\begin{definition}[Grundy number]
    For a game $\X = (X, \rel)$ and a state $x\in X$, \emph{Grundy number} $\G_{\X}(x)$ is recursively defined as
\[\G_{\X}(x)=\mex(\{\G_{\X}(x')\mid x \rel x'\}).\]
\end{definition}
This recursive definition does work because of the finiteness conditions in the definition of games.

The importance of Grundy number is due to the following proposition.
\begin{proposition}
    The P-player (Previous player) wins the game $\X$ with the initial state  $x\in X$ if and only if $\G_{\X}(x) = 0$.
\end{proposition}
\begin{proof}
\memo{add bib}
\end{proof}

% Moreover, Grundy number is compatible with the \emph{addition of games}.
Next, we introduce the notion of the sum game. It is conventionally called sum and denoted by $\X + \Y$, but in this paper, we prefer the tensor symbol $\X\otimes \Y$.
\begin{definition}[Addition of games]
For two games $\X = (X,\rel_{\X}), \Y = (Y,\rel_{\Y})$, their \emph{sum} $\X \otimes \Y$ is a game $(X\times Y, \rel_{\X \otimes \Y})$, where $(x,y) \rel_{\X \otimes \Y} (x',y')$ if and only if 
$(x \rel_{\X} x' \land y=y')$ or $(x=x' \land y \rel_{\Y}y')$.
\end{definition}
\memo{This is called \dq{box product} in graph theory. \cite{kapulkin2023closed}}
\begin{example}
    The $n$-heaps nim game is the sum of $n$-copies of ($1$-heap) nim games.\[\Nim{n} = \Nim{1} \otimes \dots \otimes \Nim{1}\]
\end{example}

There is a well-known way to calculate the Grundy number of a state of a sum game: nim-sum.

\begin{definition}[Nim-sum]
    \emph{Nim-sum} is the abelian group structure on $\N$, induced by the bijection $\N \to \bigoplus_{k=0}^{\infty} \Z/2\Z$ given by the binary expansion . In other words, nim-sum is the digit-wise exclusive disjunction (xor) of the binary expansion.
\end{definition}
For example, $7\nsum 5 = (111)_{2} \nsum (101)_{2} = (010)_{2} = 2$.

The following famous proposition is not due to me. For a proof, see \memo{add bib}
\begin{theorem}[Nim-sum rule= generalized Bouton's theorem \memo{citation}]\label{theoremNimSumRule}
    For two games $\X = (X,\rel_{\X}), \Y = (Y,\rel_{\Y})$ and states $x\in X, y\in Y$, the Grundy number of $(x,y)$ is given by Nim-sum:
    \[\G_{\X\otimes\Y}(x,y)= \G_{\X}(x)\nsum\G_{\Y}(y).\]
\end{theorem}
Combining two propositions above, we can deduce a winning states of a sum game.
\begin{example}[Analysis of nim]\label{ExampleAnalysisOfNim}
    For example, we can deduce a winning strategy of $n$-heap nim $\Nim{n}$, which is a sum of $n$-copy of $\Nim{1}$.
    \memo{Write}
\end{example}


% \section{Category of games}\label{SectionCategoryOfGames}
\subsection{Category of games}\label{SubSectionCategoryOfGames}
    In this subsection, we will define the category of games, which will be rephrased in category-theoretic terminology in the latter part of this paper.

    A naive idea of \emph{game morphisms} might be functions that preserve the transition relation. In other words, a game morphism from $\X$ to $\Y$ might be guessed to be a function $X \to Y$ such that, if $x\rel_{\X} x'$ then $f(x) \rel_{\Y} f(x')$.

    However, for several reasons, we will not adopt that naive definition. One intuitive reason is that they preserve only \dq{graph-theoretic data} and do not preserve \dq{game-theoretic data}. For example, such a \dq{graph-theoretic} function might send a $P$-state to an $N$-state and does not preserve the Grundy number and the birthday of games.
    \memo{Write a sketch}

    Modifying such a problematic point, we define the notion of game morphism utilizing the \dq{path-lifting property}:
    \begin{definition}[Game morphism]\label{DefinitionGameMorphism}
        A \emph{game morphism} from a game $\X = (X, \rel_{\X})$ to $\Y = (Y, \rel_{\Y})$ is a function $f\colon X \to Y$ such that
        \begin{description}
            \item[Graph morphism] if $x\rel_{\X} x'$ then $f(x) \rel_{\Y} f(x')$. \label{ConditionGraphpreserving}
            \item[Path-lifting] if $f(x) \rel_{\Y} y$, then there exists $x' \in \X$ such that $x\rel_{\X}x'$ and $f(x')= y$. \label{conditionLocallySurjective}
        \end{description}
    \end{definition}

Later, we will see that this notion of game morphisms coincides with the notion of coalgebra homomorphisms \memo{ref}, and that game morphisms preserve all \dq{recursively defined data} of games, including ending states, outcomes, Grundy numbers, and birthdays.

\begin{notation}\label{NotationCategoryOfGames}
    The category of games and game morphisms is denoted by $\Gs$, and the canonical forgetful functor is denoted by $U \colon \Gs \to \Set$.
\end{notation}

\begin{remark}[Categorical properties of the category of games]
How well does the category of games behave categorically? Investigating the categorical properties of the category of games is not the main topic of this paper, but here I will list some facts.
\begin{itemize}
    \item The category of games $\Gs$ is locally finitely presentable. In particular, it has all small limits and small colimits.
    \item The forgetful functor $U\colon \Gs \to \Set$ is cocontinuous, but not continuous.
    % \item  The category of games $\Gs$ has a subobject classifier.
    % \item The category of games $\Gs$ is not cartesian closed.
    \item  The category of games $\Gs$ is not a topos, but has all small limits, all small colimits, a small generating set, a subobject classifier, epi-mono factorization, ... \memo{write}
\end{itemize}
\end{remark}


\section{Games as recursive coalgebras}

\subsection{Coalgebras and recursive coalgebras}\label{subsectionCoalgebraicMethod}
% \subsection{Coalgebras of an endofuntors}
\begin{definition}[Coalgebras and algebras]\label{DefinitionCoalgebra}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a \demph{$T$-coalgebra} is a pair of an object $X \in \ob(\C)$ and a morphism $\str \colon X \to TX$. A \demph{$T$-algebra} is a pair of an object $X \in \ob(\C)$ and a morphism $\alpha \colon TX \to X$.
\end{definition}

\begin{definition}[Coalgebra homomorphism and algebra homomorphism]
\label{DefinitionCoalgebraMorphism}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a homomorphism of $T$-coalgebras from $(X, \str)$ to $(X',\str')$ is a morphism $f\colon X \to X'$ in $\C$ such that 
    \[
    \begin{tikzcd}
        X\ar[r,"f"]\ar[d,"\str"]&X'\ar[d,"\str'"]\\
        TX\ar[r,"Tf"]&TX'
    \end{tikzcd}
    \]
    commutes. Homomorohisms between $T$-algebras are similarly defined.
\end{definition}

\begin{notation}\label{NotationCoalg}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, the category of $T$-coalgebras and $T$-coalgebra homomorphisms is denoted by $\Coalg{T}$. The category of $T$-algebras and $T$-algebra homomorphisms is denoted by $\Alg{T}$.
\end{notation}

\begin{definition}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a \demph{coalgebra-algebra morphism} from a $T$-coalgebra $(X, \str)$  to  a $T$-algebra $(A,\alpha)$ is a morphism $f\colon X\to A$ in the category $\C$ such that the diagram
    \[
    \begin{tikzcd}
        X\ar[d,"\str"]\ar[r,"f"]&A\\
        TX\ar[r,"Tf"]&TA\ar[u,"\alpha"']
    \end{tikzcd}
    \]
    commutes.
\end{definition}

\begin{definition}
    A $T$-coalgebra $\X=(X,\str)$ is a \demph{recursive coalgebra} if for any $T$-alegebra $\A=(A,\alpha)$, there is a unique coalgebra-algebra morphism $\X\to \A$. The full subcategory of $\Coalg{T}$ that consists of all recursive coalgebras is denoted by $\RecCoalg{T}$.

    For recursive coalgebra $\X=(X, \theta)$ and a $T$-algebra $\A=(A, \alpha)$, the unique coalgebra-algebra morphism $X\to A$ is called the \demph{hylomorphism} and denoted by $\hylo_{\A, \X}\colon X \to A$.
\end{definition}

\begin{remark}
\cite{taylor1999practical}
For now, see \href{https://ncatlab.org/nlab/show/recursion+scheme}{[recursion scheme]} in nLab.
For the relationship with well-founded coalgebra, see the recent study \cite{adamek2020well} by Adamek, Milius, and Moss.
\end{remark}

\begin{proposition}[\memo{Labek+ Taylor}]\label{PropositionTerminalRecursiveCoalgebra}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, if a $T$-algebra $\A=(A,\alpha)$ is the initial $T$-algebra, then
    \begin{itemize}
        \item the structure map $\alpha \colon TA \to A$ is an isomorphism, and
        \item the coalgebra $(A, \alpha^{-1}\colon A \to TA)$ is the terminal recursive coalgebra.
    \end{itemize}
\end{proposition}
\begin{proof}
    The first assertion is known as Lambek's lemma. The second assertion immediately follows from the related definitions.
\end{proof}




\subsection{Games as recursive coalgebras}
\begin{definition}[finite powerset functor]\label{DefinitionPf}
    The finite powerset functor $\Pf:\Set \to \Set$ is the subfunctor of the covariant powerset functor $\mathcal{P}:\Set \to \Set$ such that 
    $\Pf(X) = \{S \subset X\mid \# S < \infty\}$.
\end{definition}

\begin{theorem}
    The category of games is equivalent to the category of recursive $\Pf$-coalgebras.
    \[
    \Gs\simeq \RecCoalg{\Pf}
    \]
\end{theorem}
\begin{proof}
    % Notice that our formulation of games is a special case of $\Pf$-coalgebra.
For a game $\X = (X,\rel)$, we can define a structure map $\str:X \to \Pf(X)$ by $ x \mapsto \str (x) \coloneq \{x'\in X\mid x\rel x'\}$. The \dq{finite options} condition in the definition of games ensures the finiteness of $\str(x)$.

This correspondence defines a fully faithful functor $\Gs \to \Coalg{\Pf}$. This follows since a function $f\colon X \to X'$ is a $\Pf$-coalgebra homomorphism if and only if $f(\str(x))=\str'(f(x))$. The inclusion relation $f(\str(x))\subset \str'(f(x))$ is equivalent to the \dq{Graph morphism condition}, and the other inclusion relation $f(\str(x))\supset \str'(f(x))$ is equivalent to the \dq{Path-lifting condition}.

To prove the essential image of the fully faithful functor is the full subcategory of recursive coalgebras, it suffices to see that a $\Pf$-coalgebra $(X,\str)$ is recursive if and only if the corresponding graph satisfies the \dq{finite time} condition. If the graph satisfies the finite time condition, we can resursively construct the unique coalgebra-algebra morphism, and prove that it is recurisive coalgebra. Conversely, suppose a coalgebra $\X= (X,\str)$ is a recursive coalgebra. Define a $T$-algebra $\A=(\N,\xem)$ by
\[
\xem(S) \coloneq \min\{n \in \N\mid \text{for any }m\in S, m<n\},
\]
and consider the hylomorphism $\hylo_{\A,\X}\colon X \to N$. If $x\to x'$, then we can prove that $\hylo_{\A,\X}(x)>\hylo_{\A,\X}(x')$. By the well-foundedness of the poset $(\N,<)$, this proves that thecorresponding graph of the coalgebra $\X=(X, \str)$ satisfies the finite time condition, thus is a game.
\end{proof}

\begin{remark}
    \cite{adamek2020well}
\end{remark}



\begin{example}[Nim is von Neumann's natural numbers!]\label{ExampleNimCoalgebra}
    Let $(\N, \nu:\N \to \Pf(\N))$ denote the 
    $\Pf$-coalgebra corresponding to the ($1$-heap) nim game $\Nim{1}=(\N, >)$. This function $\nu$ is given by 
    \[\nu:\N \to \Pf(\N): n \mapsto \{0,1, \dots, n-1\}.\]
    In other words, this is von Neumann's set-theoretic definition of natural numbers.
    % \memo{
    % }
\end{example}

Such an appearance of a set-theoretic construction is 
    % kind of necessary. Because both the initial algebra and the terminal game are the set-theoretic object $\H$, 
    % the set of all hereditarily finite sets, and 
    due to the fact that the nim game is the subgame of the terminal game, which we will investigate in the next subsection.
    See next subsection.

\subsection{The terminal game consists of hereditarily finite sets}
\memo{ask refs}
% With the category-theoretic terminology, we can conduct universal costructions of games! The first, and

Possibly the most important game is, the terminal object of $\Gs$. This subsection aims to descrbe the terminal game.
First, we define hereditarily finite sets, by recursion.
\begin{definition}[Hereditarily finite sets]
A \emph{hereditarily finite set} is recursively defined as a finite set of hereditarily finite sets\footnote{Rigorously speaking, a hereditarily finite set is a set that is ensured to be hereditarily finite by this recursive definition.} .
     % A set $A$ is \emph{hereditarily finite} if all elements of $A$ are hereditarily finite.
     The set of all hereditarily finite sets is denoted by $\H$.
\end{definition}

This recursive definition might look confusing. We give several examples of hereditarily finite sets.
\begin{example}\label{LabelExampleHereditarilyFiniteSets}
The following sets are hereditarily finite sets:
\begin{itemize}
    \item The empty set $\emptyset$ is trivially hereditarily finite since it has no element.
    \item Therefore, the set $\{\emptyset\}$ is also hereditarily finite. 
    \item By induction, every (von Neumann's formulation of) natural number $n=\{0,1, \dots n-1\}$ is hereditarily finite. In other words, 
    \[\N = \{0=\emptyset,\ 1=  \{\emptyset\},\ 2= \{\emptyset,\{\emptyset\}\},\ 3=\{\emptyset,  \{\emptyset\}, \{\emptyset,\{\emptyset\}\}\}, \dots\} \subset \H.\] 
    \item The set $\{\{\emptyset\}\}$ is a hereditarily finite set that is not a natural number.
\end{itemize}
\end{example}

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

\begin{proposition}\label{PropositionInitialAlgebraIsHereditarilyFiniteSets}
The $\Pf$-algebra $\H$ is the initial $\Pf$-algebra.
\end{proposition}
\begin{proof}
    Since $\Pf$ preserves filtered colimits, we can utilize Adamek's construction of the initial algebra (\memo{cite}). Since the set $\H$ is the colimit of
    \[
        \begin{tikzcd}
            \emptyset \ar[r]& \Pf(\emptyset) \ar[r]& \Pf(\Pf(\emptyset)) \ar[r]&\Pf(\Pf(\Pf(\emptyset))) \ar[r]&\cdots \H,
        \end{tikzcd}
    \]
    this completes the proof.
\end{proof}

\begin{definition}[Terminal game]\label{DefinitionUniversalGame}
    The \demph{terminal game} $\H=(\H,\to)$ is a game whose underlying set is the set of all hereditrily finite set $\H$ and whose relation $\rel$ is defined by 
    \[A \rel B \iff B \in A.\]
\end{definition}

\begin{proposition}\label{PropositionUniversalIsTerminal}
    The terminal game $\H$ is the terminal object of $\Gs$.
\end{proposition}
\begin{proof}
    This is due to Proposition \ref{PropositionTerminalRecursiveCoalgebra} and Proposition \ref{PropositionInitialAlgebraIsHereditarilyFiniteSets}.
    % , it is enough to prove that $\H$ is the initial $T$-algebra.
\end{proof}

\begin{remark}[Ackerman's interpretation]
There is another way to describe the terminal game, using natural numbers $\N$ instead of hereditarily finite sets $\H$. Consider a $\Pf$-algebra structure on $\N$ defined by
 % One canonical choice of such bijection is
    \[b: \Pf(\N)\to \N \colon S \mapsto \sum_{s\in S} 2^s.\]
    % on the set of natural numbers $\N$.
    It is simply a binary expression and hence bijective.
% Throughout this paper, $\H = \Pf(\H) $ is the crucial fact. But is it necessary to consider $\H$? Just by considering the cardinality, we should be able to consider a bijection between $\N$ and $\Pf(\N)$ as well!
    % since they are both countable sets.
    The unique $\Pf$-algebra morphism $\mathrm{Ack}\colon\H \to \N$ is called \emph{Ackerman's interpretation} \cite{ackermann1937widerspruchsfreiheit} and known to be bijective.
    % In fact, $\mathrm{Ack}$ gives an isomorphism between them as $\Pf$-algebras and $\Pf$-coalgebras (or, games).
    Consequently, this $T$-algebra $(\N,b)$ is also an initial object in $\Alg{\Pf}$, and hence also gives the terminal object in $\Gs \simeq \RecCoalg{\Pf}$. This is what we called the binary exponent nim in Example \ref{ExampleTheUniversalGameInTermsOfNumbers}.
\end{remark}

\begin{notation}
    For a game $\X$, the unique game morphism to $\H$ is denoted by $\rd_{\X}\colon \X \to \H$.
\end{notation}

\begin{proposition}
    For a game $\X$ and a $\Pf$-algebra $\A=(A, \alpha)$, the hylomorphism $\hylo_{\A,\X}\colon \X \to \A$ is decomposed into 
    \[
    \begin{tikzcd}
    X \ar[r,"\rd_{\X}"] \ar[rr,"\hylo_{\A,\X}"', bend right] & \H\ar[r,"\hylo_{\A, \H}"] & A
    \end{tikzcd}
    \]
\end{proposition}

\begin{remark}[Two definitions of combinatorial games]\label{RemarkTwoDefinitionsOfCombinatorialGames}
\end{remark}



\subsection{Recursively defined values are hylomorphisms}

\begin{definition}
    A \demph{game evaluation} to a set $A$ is a family of functions
    \[
    \{v_{\X}\colon X\to A\}_{\X=(X, \str)\text{: game}}.
    \]
    from all games to the set $A$.
    A game evaluation is \demph{recursively defined} if there exists a $\Pf$-algebra $\A=(A, \alpha)$ such that for any game $\X$, the  function $v_{\X}$ is equal to the corresponding hylomorphism $\hylo_{\A, \X}\colon X \to A$.
\end{definition}

\begin{example}
    Grundy number $\{\G_{\X}\colon X \to \N\}$ is recursively defined by the $\Pf$-algebra $(\N, \mex\colon \Pf(\N) \to \N)$.
\end{example}

\begin{example}
    Outcome $\{X \to \{N,P\}\}$ is recursively defined by the $\Pf$-algebra $(\{N,P\}, o)$, where
    \[
    o\colon \Pf(\{N,P\})\to \{N,P\}\colon S \mapsto 
    \begin{cases}
        P &(P \notin S)\\
        N &(P\in S).
    \end{cases}
    \]
\end{example}

\begin{remark}
    There is a $\Pf$-algebra homomorphism from $(\N,\mex)$ to $(\{N,P\}, o)$. This proves the proposition \memo{cite}.
\end{remark}

\begin{example}
    Birthday $\{b_{\X}\colon X \to \N\}$ is recursively defined by the $\Pf$-algebra $(\N,\xem)$
    \[
    \xem \colon \Pf(\N)\to \N\}\colon S \mapsto \min\{n \in \N\mid \text{for any }m\in S, m<n\}
    \]
\end{example}

% \begin{example}[outcome]
% The outcome function $\{X \to \{\}\}$
% \end{example}

In summary, we obtain the following proposition:
\begin{proposition}
Grundy number, outcome, and birthday are recursively defined.
\end{proposition}
% \begin{proof}
%     Grundy number $\{\G \X\to \N\}$
% \end{proof}


\begin{table}
    \centering
    \begin{tabular}{|c|c|} \hline 
         Recursively defined game evaluation&  $\Pf$-algebra\\ \hline 
         outcome&  $(\{N,P\}, o)$\\ \hline 
         misere outcome&  $(\{N,P\},\mu)$\\ \hline 
         remoteness&  $(\N, \rho)$\\ \hline 
         Grundy number&  $(\N,\mex)$\\ \hline
 Birthday& $(\N,\xem)$\\\hline
    \end{tabular}
    \caption{Game evaluations and $\Pf$-algebras}
    \label{TableGameEvaluations}
\end{table}

\begin{corollary}
    A game morphism preserves all recursively defined game evaluations. In particular, a game morphism preserves
    \begin{itemize}
        \item Grundy number
        \item outcome
        \item misere outcome
        \item birthday
        \item remoteness
    \end{itemize}
\end{corollary}

There are a lot of other examples:
\begin{example}[Ended]
    
\end{example}

\begin{example}
    In combinatorial game theory, a \demph{misere game} is a game, where the player who takes the last move loses. For misere games, the notion of outcome should be modified so that the ending state is a $N$-state.
    Defining a $\Pf$-algebra $(\{N,P\},\mu)$ by
    \[
     \mu \colon \Pf(\{N,P\})\to \{N,P\}\colon S \mapsto 
    \begin{cases}
        P &(S=\{N\})\\
        N &(S\neq \{N\}),
    \end{cases}
    \]
    the corresponding game evaluation is the \demph{misere outcome}. 
\end{example}

\begin{example}[remoteness]
    
\end{example}

\begin{remark}[Grundy number and Birthday are dual]
    
\end{remark}



\section{Application: Nim-sum type theorem schema}
This section aims to provide a theorem schamea that generarizes the nim-sum rule \ref{theoremNimSumRule}.

\subsection{Raw bouton monoid}
\begin{proposition}
    For a monoidal category $(\C, I, \otimes)$ with a terminal object $1$, the object $1$ has a unique monoid structure with respect to the monoidal structure.
\end{proposition}
\begin{proof}
    All structural maps, $\eta\colon I \to 1$ and $\mu\colon 1\otimes 1 \to 1$, are uniquely determined. All needed commutattivities are trivial since $1$ is the terminal object. 
\end{proof}

We will utilize the following well-known fact.
\begin{proposition}[Well-known]
    A lax monoidal functor $F\colon (\C, I_{\C}, \otimes_{\C})\to (\D,I_{\D},\otimes_{\D} )$ sends a monoid object in $\C$ to a monoid object in $\D$.
\end{proposition}

\begin{definition}We adopt the following terminologies:
\begin{itemize}
    \item For a monoidal category $(\C, I_{\C}, \otimes_{\C})$ with a terminal object $1$, the \demph{terminal monoid} is the unique monoid object whose underlying object is $1$, which is the terminal object of the category of monoid objects.
    \item For a lax monoidal functor $F\colon (\C, I_{\C}, \otimes_{\C})\to (\D,I_{\D},\otimes_{\D})$, the \demph{$F$-terminal monoid} is the monoid object in $\D$, obtained by sending the terminal monoid of $\C$ by the functor $F$.
\end{itemize}
\end{definition}

\begin{example}
    The terminal monoid in $(\C, I_{\C}, \otimes_{\C})$ is $\id_{\C}$-terminal monoid.
\end{example}

\begin{example}
    For the free abelian group functor $F\colon \Set\to \mathbf{Ab}$, the $F$-terminal monoid is the ring of integers $\Z$.
\end{example}

% \begin{remark}
%     In fact, the terminal monoid is the terminal object of the category of monoid objects in $(\C, I_{\C}, \otimes_{\C})$.
% \end{remark}

% For many lax monoidal functors, the $F$-monoid is tirivial. For example, the forgetful functor 

\begin{definition}
    For a monoidal structure $(\Gs, I, \ast)$ on the category of games $\Gs$ such that the forgetful functor $U \colon (\Gs, I, \ast) \to (\Set,1,\times)$ is lax monoidal, the \demph{raw bouton monoid} $\RB_{\ast}$ is the $U$-terminal monoid with respect to the monoidal structure $\ast$. 
    % The raw bouton monoid is denoted by $(\rB, \rm, \ru)$.
\end{definition}
The raw bouton monoid is a usual monoid (i.e., a monoid in $\Set$), and whose underlying set is $\H$ due to Proposition \ref{PropositionUniversalIsTerminal}.

% \begin{proposition}
%     For a monoidal structure $(\Gs, \ast, I)$ on the category of games $\Gs$ such that the forgetful functor $U \colon \Gs \to \Set$ is lax monoidal, the underlying set of $\RB_{\ast}$ is the set of hereditarily finite set $\H$. 
% \end{proposition}

\begin{notation}
    We adopt the following notation:
    \begin{itemize}
        \item The multiplication function of the raw bouton monoid $\RB_{\ast}$ is denoted by $\circledast \colon\H\times \H \to \H$. Notice that this multiplication function depends on the monoidal structure $\ast$.
        \item For two games $\X=(X,\rel_{\X})$ and $\Y=(Y,\rel_{\Y})$, the coherence map of the lax monoidal functor is denoted by $\mu_{\X,\Y}\colon X\times Y = U\X \times U\Y \to U(\X\ast \Y)$, and $\mu_{\X,\Y}(x,y)\in  U(\X\ast \Y)$ is simply denoted by $(x,y) \in  U(\X\ast \Y)$.
    \end{itemize}
\end{notation}

\begin{proposition}[Raw generalized nim-sum rule]
For two games $\X=(X,\rel_{\X})$ and $\Y=(Y,\rel_{\Y})$, we have the following equation in the raw bouton monoid $\RB_{\ast}$:
    \[
    \rd_{\X\ast\Y}(x,y) = \rd_{\X}(x) \circledast \rd_{\Y}(y).
    \]
\end{proposition}
\begin{proof}
    Since $\H$ is the terminal game, we have the following commutative diagram in $\Gs$:
    \[
    \begin{tikzcd}
        &\X\ast \Y\ar[rd,"\rd_{\X\ast \Y}"],\ar[d,"\rd_{\X}\ast \rd_{\Y}"']&\\
        &\H\ast\H\ar[r,"\rd_{\H\ast \H}"]&\H.
    \end{tikzcd}
    \]

    By sending this diagram by $U$ and utilizing the naturality of $\mu$, we have the following commutative diagram in $\Set$:
    \[
    \begin{tikzcd}
        X\times Y=U\X\times U\Y \ar[d,"U\rd_{\X}\times U\rd_{\Y}"']\ar[r,"\mu_{\X,\Y}"]&U(\X\ast \Y)\ar[rd,"U(\rd_{\X\ast \Y})"],\ar[d,"U(\rd_{\X}\ast \rd_{\Y})"']&\\
        \H \times \H=U\H \times U\H\ar[r,"\mu_{\H,\H}"]\ar[rr, bend right , "\circledast"']&U(\H\ast\H)\ar[r,"U(\rd_{\H\ast \H})"]&U(\H)=\H.
    \end{tikzcd}
    \]
    This proves the proposition.
\end{proof}

\subsection{Bouton monoid}
\subsection{Example 1: Nim-sum}
\subsection{Example 2: Remoteness}


% In principle, the raw Bouton monoid $\RB_{\ast}$ contains sufficient information to analyze games by decomposition, but practically, it is too large to compute efficiently. Therefore, in order to calculate desired information about games (such as outcome), we define an appropriate size quotient monoid of the raw Bouton monoid.

In principle, the raw Bouton monoid $\RB_{\ast}$ contains sufficient information to decompose and analyze games, but practically, it is too large to compute. Therefore, by quotienting the monoid to the size necessary to calculate desired information about the game (such as outcome of games), a more practical \demph{Bouton monoid} will be defined in this subsection.

\begin{definition}[Minimum quotient monoid]
    For a monoid $M$, a set $S$ and a function $f\colon M \to S$, the \demph{minimum quotient monoid} of $f\colon M \to S$ is a surjective monoid homomorphism $q_f \colon M \twoheadrightarrow M_f$ such that
    \begin{enumerate}
        \item $f$ factors through $q_f$ (as a function). \label{ConditionSfactor}

        \item For an arbitrary surjective monoid homomorphism $q \colon M \to N$ such that $f$ factors thorough $q$,
        % satisfying condition (\ref{ConditionSfactor})
        there exists a function $r\colon N \to M_f$, (which is necessarily unique and is a surjective monoid homomorphism) such that $q_{f} = r\circ q$. \label{ConditionMinimum}

                \[
        \begin{tikzcd}
            M\ar[rr,"f"]\ar[rd,"q", two heads]\ar[rdd,"q_{f}"', two heads]&&S\\
            &N\ar[ru,dashed]\ar[d,"r", dashed]&\\
            &M_{f}\ar[ruu,dashed]&
        \end{tikzcd}
        \]
    \end{enumerate}
\end{definition}

\begin{proposition}[Unique existence]\label{PropositionUniqueExistenceOfUniversalQuotient}
    For a monoid $M$, a set $S$, and a function $f\colon M \to S$, the minimum quotient monoid of $f$ exists and is unique (up to a canonical isomorphism). Furthermore, the corresponding congruence relation $\sim_{f} \subset M\times M$ is given by
    \[
    m\sim_{f} m' \iff \text{for any }a,b\in M, f(amb)=f(am'b).
    \]
    That is, the quotient map $q_{f}\colon M\twoheadrightarrow M_{f}$ is (isomorphic to) the canonical surjection $M \twoheadrightarrow M/{\sim_{f}}$.
\end{proposition}
\begin{proof}
% The maximum quotient monoid is the quotient o
% % Since the maximum quotient monoid is the right adjoint of the embedding functor
% % \[
% % \text{(the complete latice of quotient monoids of $M$)}\to M/\Set,
% % \]
% % the proposition follows from the general adjoint functor theorem.
First, we need to prove the equivalence relation $\sim_f$ is a congruence relation. If $m\sim_f m'$ and $n\sim_f n'$, for any $a,b\in M$, we have
\[
f(amnb)= f(am'nb)=f(am'n'b),
\]
and thus $mn\sim_f m'n'$. This proves that $\sim_f$ is a congruence relation, and $q_f\colon M \to M_f \coloneqq M/{\sim_f}$ is a surjective monoid homomorphism.

In order to prove the condition \ref{ConditionSfactor}, we need to prove $m\sim_f m' \implies f(m) = f(m')$, and this immediately follows from the definition of $\sim_f$.

Lastly, we prove the condition \ref{ConditionMinimum}. We prove $q(m) = q(m') \implies m\sim_f m'$.  If $q(m) = q(m')$, then for any $a,b\in M$, we have $q(amb)=q(a)q(m)q(b)= q(a)q(m')q(b)=q(am'b)$, and $f(amb)=f(am'b)$, since $f$ factors through $q$. This proves that $q(m) = q(m') \implies m\sim_f m'$ and the condition \ref{ConditionMinimum}.
\end{proof}

\begin{remark}
    The construction of minimum quotient monoid is ubiquitous in combinatorial game theory. For example, even the \dq{equality} of games is conventionally defined in this way! See \cite{siegel2013combinatorial}.
\end{remark}

\begin{definition}[Bouton monoid]
For a monoidal structure $(\Gs,I, \ast)$ such that the forgetful functor $U\colon (\Gs,I,\ast) \to (\Set, 1,\times)$ is lax monoidal and a $\Pf$-algebra $\A=(A, \alpha)$, the \demph{Bouton monoid} $\B_{\ast, \A}$ is the minimum quotient monoid of a function 
\[
\begin{tikzcd}
    \RB_{\ast}= \H \ar[r,"\hylo_{\A,\H}"]& A.
\end{tikzcd}
\]
The canonical surjective monoid homomorphism from $\RB_{\ast}$ to $\B_{\ast,\A}$ is denoted by $q_{\ast, \A}\colon \RB_{\ast}\twoheadrightarrow \B_{\ast,\A}$.
% where $\RB_{\ast}$ is equipped with the raw Bouton monoid structure with respect to the monoidal structure $\ast$.
\end{definition}

\begin{notation}
    We adopt the following notations:
    \begin{itemize}
        \item For a game $\X=(X,\rel_{\X})$, the function
        \[
        \begin{tikzcd}
            X \ar[r,"\rd_{\X}"] & \RB_{\ast} \ar[r,"q_{\ast,\A}"] &\B_{\ast,\A}
        \end{tikzcd}
        \]
        is denoted by $\G_{\ast,\A}\colon \X \to \B_{\ast,\A}$.
    \end{itemize}
\end{notation}

\section{Discussion}\label{SectionFutureWorks}
We believe that this paper is just a starting point of the theory of "Games as recursive coalgebras". There are still a lot of things to be calculated. We post some of the remaining questions in this appendix.

\subsection{Mathematically stated questions}
\begin{question}[The closed structure]
    What is the internal hom?
\end{question}

\begin{question}
    Are the bouton functions always recursively defined?
\end{question}
\subsection{Ambiguous (but ambitious) questions!}
\memo{It's quite natural to consider a multiplayer game, probability game, 2-turns/1-turn game, and other variants of games. And might be dealt with using some appropriate algebras. Furthermore, can we consider other graph data, like entropy?  I know there is a notion of the temperature of a game. Is it an example of this framework?}

\memo{By considering coalgebra-algebra map (from now, we call it ca map) (or, profunctor Alg -> Coalg), we may able to discard $\H$ and discuss everything so far...(?) The canonical map may be the unique ca map, and a game (or well-foundedness) may be equivalent to the condition that for any algebra, there uniquely exists a ca map to it.}

\begin{question}[partisan games]\label{que:PartisanGames}
Replacing $\Pf$ with other endofunctors to describe other types of game theory, like partisan, probabilistic, mis\`ere, transfinite, and loopy games.
\end{question}
Replacing $\Pf$ with other endofunctors to describe other types of game theory, like partisan, probabilistic, mis\`ere, transfinite, and loopy games.

\begin{question}
    Double cat
\end{question}
\begin{question}
    lpac
\end{question}
\begin{question}
    semantics
\end{question}

\begin{question}
    Is there a topos-theoretic analogy?
\end{question}

\begin{question}
    As a relative local state classifier.
\end{question}

\begin{question}
    Difference structure
\end{question}

\begin{question}[Ryo Suzuki]
    Via the Ackerman interpretation, the nim-sum operation is interpreted as symmetric difference. In other words, $\Pf$ is object-wise bijective (but not isomorphic) to the monad induced by the monadic functor
    \[
    U\colon \mathrm{Vect}_{\mathbb{F}_2}\to \Set,
    \]
    and the Nim-sum structure is nothing other than the vector space structure on the minimum fixed point.
\end{question}


\appendix
\section{Categorical properties of games}
What we will prove are the following categorical properties of $\Gs$.
\begin{theorem}
The category of games has the following properties:
    \begin{itemize}
        \item $\Gs$ is locally finitely presentable.
        \item In particular, $\Gs$ is small complete and small cocomplete.
        \item The forgetful functor $U\colon \Gs \to \Set$ has a right adjoint, and creates all colimits. \memo{Is it comonadic?}
        \item $\Gs$ has a subobject classifier
        \item $\Gs$ has the epi-mono factorization
        \item The subobject lattice of the object of $\Gs$ is a Heyting algebra.
    \end{itemize}
    However, 
    \begin{itemize}
        \item $\Gs$ is not cartesian closed.
        \item In particular, $\Gs$ is not an (elementary) topos.
    \end{itemize}
\end{theorem}

\subsection{Creation of colimits}\label{SubsectionCocompleteness}

\begin{proposition}[Well-founded part adjunction]
    The category of games $\Gs$ is a coreflective subcategory of $\Coalg{\Pf}$.
\end{proposition}
\begin{proof}
    \cite{adamek2020well}
\end{proof}

\begin{proposition}\label{propositionCocompleteness}
    The forgetful functor $U \colon \Gs \to \Set$ strictly creates all small colimits. In particuler, $\Gs$ is cocomplete.
\end{proposition}
\begin{proof}
The forgetful functor is decomposed into
\[
\Gs \to \Coalg{\Pf}\to \Set.
\]
And both functors above strictly create all small colimits.
\end{proof}

\memo{Does it come from the comonadicity?}

\subsection{Forgetful-cofree adjunction
% Labeled hereditarily finite sets give the 
}

\begin{definition}[Labeled Hereditarily finite sets]\label{DefinitionLabeledHFS}
    For a set (of labels) $\Lambda$, a $\Lambda$-labeled hereditarily finite set is recursively defined as a pair $(S,\lambda)$ of a finite set $S$ of $\Lambda$-labeled hereditarily finite sets and $\lambda \in \Lambda$.

    In other words, the set of all $\Lambda$-labeled hereditarily finite sets $\HF(\Lambda)$ is defined to be
    \[
    \HF(\Lambda) = \bigcup_{k=0}^{\infty} \HF_{n}(\Lambda),
    \]
    where $\HF_{0}(\Lambda)= \emptyset$ and $\HF_{n+1}(\Lambda)= \Pf(\HF_{n}(\Lambda)) \times \Lambda$.
\end{definition}

\begin{proposition}[Forgetful-Cofree adjunction]\label{PropositionForgetfulCofreeadjunction}
    $\HF$ gives a right adjoint to the forgetful functor.
    \[\ADJ{\Set}{\HF}{\Gs}{U}\]
\end{proposition}

% \begin{notation}\label{NotationLabeledHF}
%     The set of all $\Lambda$-labeled hereditarily finite sets is denoted by $\HF(\Lambda)$.
% \end{notation}
\subsection{Epimorphisms, monomorphisms, and factorization}
\begin{proposition}[Epic and monic morphisms]\label{PropositionEpicandMonicMorphisms}
    In the category of games $\Gs$, a morphism $f \colon \X\to \Y$ is
    \begin{enumerate}
        \item epic, if and only if it is surjective. \label{StatementEpic}
        \item monic, if and only if it is injective.\label{StatementMonic}
        \item isomorphic, if and only if it is bijective.\label{StatementIsomorphic}
    \end{enumerate}
\end{proposition}
\begin{proof}
    (\ref{StatementEpic}) follows from the fact that the forgetful functor $\Gs \to \Set$ is a faithful left adjoint (Proposition \ref{PropositionForgetfulCofreeadjunction}).

    (\ref{StatementIsomorphic})
    \memo{Does it come from the comonadicity?}
\end{proof}

\begin{corollary}[Subgame]\label{CorollarySubgame}
    A subobject of a game $\X = (X, \rel)$ is (canonically isomorphic to) a downward closed subset $S\subset X$, i.e., a subset $S \subset X$ such that if $x\in S$ and $x\rel x'$ then $x' \in S$. 
\end{corollary}

\begin{corollary}
    The category of games has the epi-mono factorization system.
\end{corollary}

\subsection{The subobject classifier}\label{SubsectionSubobjectClassifier}
In this subsection, we will give an explicit description of the subobject classifier of the category of games.

\begin{figure}[ht]
    \centering
    \includegraphics[width=0.5\linewidth]{images/SubobjectClassifier.jpeg}
    \caption{An incomplete sketch of the subobject classifier}
    \label{FigureSubobjectClassifier}
\end{figure}
\begin{figure}[ht]
    \centering
    \includegraphics[width=0.5\linewidth]{images/SubobjectClassification.jpeg}
    \caption{An example of subobject classification}
    \label{FigureSubobjectClassification}
\end{figure}

Our idea of the construction is simple: utilize the cofree-forgetful adjunction (Prposition \ref{PropositionForgetfulCofreeadjunction}). Because of Corollary \ref{CorollarySubgame}, we have the following canonical injection 
\[
\mathrm{Sub}_{\Gs}(\X) \rightarrowtail \Set(X,\{\top,\bot\}) \cong \Gs(\X,\HF(\{\top,\bot\})).
\]
Therefore, by the Yoneda lemma, if a subobject classifier exists, then it should be a subobject of the game of truth-values-labeled hereditarily finite sets $\HF(\{\top,\bot\})$.

\begin{definition}\label{DefinitionTruthClosed}
    A $\{\top, \bot\}$-labeled hereditarily finite set $A\in \HF(\{\top,\bot\})$ is \emph{truth-closed} if 
    \begin{enumerate}
        \item if $A$ itself is labeled by $\top$, then every element of $A$ is also labeled by $\top$, and
        \item every element of $A$ is truth-closed.
    \end{enumerate}
\end{definition}

\begin{notation}
    The game of all truth-closed $\{\top,\bot\}$-labeled hereditarily finite sets is denoted by $\Omega$.
\end{notation}

See Figure \ref{FigureSubobjectClassifier} and Figure \ref{FigureSubobjectClassification}.


\begin{proposition}[Subobject classifier]\label{PropositionSubobjectClassifier}
    % The subgame of $\HF(\{\top,\bot\})$ that consists of a $\{\top, \bot\}$-colored set $A$ that satisfies
    % \begin{itemize}
    %     \item If 
    % \end{itemize}
    The game $\Omega$ is the subobject classifier of the category of games $\Gs$.
\end{proposition}

% \subsection{\texorpdfstring{$\Gs$ is locally finitely presentable}{The category of games is locally finitely presentable}}
\subsection{Locally finitely presentable}
% The category of games is 


\begin{lemma}\label{LemmaGamesAreLocallyFinite}
    Every game is a directed colimit of its finite subgames.
\end{lemma}

\begin{proposition}[Finitely presentable $=$ Finite]\label{PropositionFinitePresentabilityOfGames}
    A game is a finitely generated object if and only if its underlying set is a finite set.
\end{proposition}
\begin{proof}
    If a game is finitely generated, due to Lemma \ref{LemmaGamesAreLocallyFinite}, it should be finite. We prove the converse.

    Suppose a game $\X$ is finite. We will prove that the hom functor
    \[
    \Gs (\X, -)\colon \Gs \to \Set
    \]
    preserves filtered colimits.

    Let $\C$ be a filtered category, $F\colon \C \to \Gs$ be a functor, and $\{\alpha_c \colon Fc \to \Y\}_{c\in \ob{\C}}$ be the colimit cocone. Take an arbitrary morphism $f\colon \X \to \Y$. Our goal is to prove that there exists $c\in \ob{\C}$ such that $f$ has a lift $g$ along $\alpha_c$
    \[
    \begin{tikzcd}
        &Fc\ar[d,"\alpha_c"]\\
        \X\ar[r,"f"']\ar[ru, dashed,"\exists g"]&\Y.
    \end{tikzcd}
    \]
    (The essential uniqueness of the factorization follows from the case of $\Set$ and Proposition \ref{propositionCocompleteness}.)

    Since a finite set is finitely presentable in $\Set$, and $U$ preserves small colimits (in particuler, filtered colimits), there exists a function $h \colon U\X \to UFc$ such that the following diagram commutes
    \[
    \begin{tikzcd}
        &UFc\ar[d,"U\alpha_c"]\\
        U\X\ar[r,"Uf"']\ar[ru, dashed,"h"]&U\Y.
    \end{tikzcd}
    \]

    Let $\iota\colon \gS\to Fc$ be the subgame of $Fc$, generated by the image of $h$. Since $\X$ is finite, $\gS$ is also finite (Lemma \ref{LemmaFinitelygeneratedSubgameisFinite}).

    \[
    \begin{tikzcd}
        &\gS\ar[r,\mono,"\iota"]&Fc\ar[d,"\alpha_c"]\\
        \X\ar[rr,"f"']\ar[ru, dashed,"h"]&&\Y,
    \end{tikzcd}
    \]
    where $h$ is a mere function, denoted by a dashed arrow. Since $\Y$ is a filtered colimit (preserved by $U$) and $\gS$ is finite, there exists $k\colon c \to c'$ in $\C$ such that $\alpha_{c'}$ is injective on the subgame $Fk(\gS)=\Image{(Fk \circ \iota)}$ of $Fc'$ (Lemma \ref{LemmaImageisSubgame}). In other words, the morphism $\alpha_{c'}\circ m$ in the following diagram is injective. (Again, $h$ is a mere function.)
    % for the epi-mono (=Surj-subgame) factorization (Proposition \ref{PropositionSurjSubgameFactorization}) of $Fk \circ \iota$ 
    % \[
    % \begin{tikzcd}
    %     \gS\ar[r,\mono,"\iota"]\ar[d,\epi]&Fc\ar[d,"Fk"']\\
    %     Fk(\gS)\ar[r,\mono]&Fc'
    % \end{tikzcd}
    % \]
    \[
    \begin{tikzcd}
        &\gS\ar[r,\mono,"\iota"]\ar[d,\epi,"e"']&Fc\ar[dd,bend left, "\alpha_c"]\ar[d,"Fk"']\\
        &Fk(\gS)\ar[r,\mono,"m"]\ar[rd,"\alpha_{c'}\circ m"', \mono]&Fc'\ar[d,"\alpha_{c'}"']\\
        \X\ar[rr,"f"']\ar[ruu, dashed,"h", bend left]&&\Y,
    \end{tikzcd}
    \]
    Because the morphism $\alpha_{c'}\circ m$ is injective, it is a subgame embedding (Proposition \ref{PropositionSubgameAndSubobjectAndMono}). Therefore, the lift of $f$ along $\alpha_{c'}\circ m$ is a game morphism.
    \[
    \begin{tikzcd}
        &\gS\ar[r,\mono,"\iota"]\ar[d,\epi,"e"']&Fc\ar[dd,bend left, "\alpha_c"]\ar[d,"Fk"']\\
        &Fk(\gS)\ar[r,\mono,"m"]\ar[rd,"\alpha_{c'}\circ m"', \mono]&Fc'\ar[d,"\alpha_{c'}"']\\
        \X\ar[rr,"f"']\ar[ru,"h\circ e"]\ar[ruu, dashed,"h", bend left]&&\Y,
    \end{tikzcd}
    \]
    This proves that $f$ has a lift along $\alpha_{c'}$ in the category $\Gs$.
\end{proof}


\begin{theorem}\label{TheoremLocallyFinitePresentabilityOfTheGameCategory}
    The category of games $\Gs$ is locally fintiely presentble.
\end{theorem}


\begin{corollary}\label{CorollaryCompletenessOfGames}
    The category of games $\Gs$ is complete.
\end{corollary}


\subsection{Limits of games}\label{SubsectionLimitsOfGames}
In this subsection, we will give an explicit description of (small) limits of games. Since, every small limit is described by equalizers and products, we will explain only for them.
\subsubsection{Equalizer}\label{SubsubsectionEqualizer}

\subsubsection{Binary products}\label{SubSubsectionProducts}
In this subsection, we will explicitly construct the binary product of games. Its existence is already proven (Corollary \ref{CorollaryCompletenessOfGames}). Our plan is similar to the construction of the subobject classifier (subsection \ref{SubsectionSubobjectClassifier}). That is, utilizing the labeled hereditarily finite sets.

\begin{definition}\label{DefinitionProduct}
    Let $\X=(X,\rel_{\X})$ and $\Y= (Y, \rel_{\Y})$ two games.
    A $X\times Y$-labeled hereditarily finite set $(S, (x,y)) \in \HF({X\times Y})$, where $S$ is a finite set of $X\times Y$-labeled hereditarily finite sets $S=\{(S_i, (x_i,y_i))\}_{i=1}^{n}$, is \emph{enumerative}, if 
    \begin{enumerate}
        \item every element $(S_i, (x_i,y_i))$ is enumerative, 
        \item $\theta_{\X} (x) = \{x_i\}_{i=1}^{n}$, and
        \item $\theta_{\Y} (y) = \{y_i\}_{i=1}^{n}$,
        % \item $\{x_i\mid 1 \leq i \leq  n\}=\{x'\in X\mid x\to x'\}$ and $\{y_i\mid 1 \leq i \leq  n\}=\{y'\in Y\mid y\to y'\}$
    \end{enumerate}
    where $\theta_{\X}$ and $\theta_{\Y}$ denote the associated coalgebra structure functions.
    The subgame of $\HF{(X\times Y)}$, spanned by all enumerative elements, is denoted by $\X \times \Y$.
\end{definition}

\begin{proposition}\label{ProppositionProduct}
    For two games $\X=(X,\rel_{\X})$ and $\Y= (Y, \rel_{\Y})$, the game 
    % of enumerative $X\times Y$-labeled hereditarily finite sets 
    $\X\times \Y$ 
    gives the categorical product of $\X$ and $\Y$.
\end{proposition}
\memo{Write one example.}
\memo{On Infinite Products}

\begin{remark}[Relationship with the starling number]\label{RemarkStarlingNumber}
\end{remark}







\printbibliography

\end{document}