\documentclass{amsart}
\usepackage[left=2cm, right=2cm]{geometry}

\usepackage[utf8]{inputenc}
\usepackage{amsfonts, amsthm, amssymb, mathtools,etoolbox,stmaryrd}
\usepackage{blindtext}
\usepackage[colorlinks=true, urlcolor=blue, linkcolor=blue, citecolor=blue]{hyperref}
\usepackage{tikz,tikz-cd}
\usepackage{array}
\usepackage{framed}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{autobreak}
\usepackage[maxnames=10, sorting = nyt]{biblatex}


\renewbibmacro{in:}{}
\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*{corollary*}{Corollary}
\newtheorem{question}[theorem]{Question}

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

\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{red}{memo: #1}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\X}{\mathbb{X}}
\newcommand{\Y}{\mathbb{Y}}
\newcommand{\W}{\mathbb{W}}
\newcommand{\gS}{\mathbb{S}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\A}{\mathbb{A}}
\newcommand{\I}{\mathbb{I}}
\newcommand{\id}[1]{\mathrm{id}_{#1}}
\newcommand{\Pf}{\mathcal{P}_{\mathrm{fin}}}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\Gs}{\mathbf{Games}}
\newcommand{\nsum}{\oplus}
\newcommand{\Alg}[1]{\mathrm{Alg}_{#1}}
\newcommand{\Coalg}[1]{\mathrm{Coalg}_{#1}}
\newcommand{\PfAlg}{\Alg{\Pf}}
\newcommand{\PfCoalg}{\Coalg{\Pf}}
\newcommand{\mex}[1]{\mathrm{mex}(#1)}
\newcommand{\m}{\mathrm{mex}}
\newcommand{\G}[2]{\mathcal{G}_{#1}(#2)}
\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}}
\newcommand{\Her}{\mathbb{H}}
\newcommand{\epi}{twoheadrightarrow}
\newcommand{\mono}{rightarrowtail}
\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}



\DeclareMathOperator{\ob}{\mathrm{ob}}
\title{Games as well-founded coalgebras}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo}}
\date{\today}
\subjclass[2020]{MSC}
\keywords{combinatorial games, coalgebra of an endofunctor, Well-founded coalgebra, locally presentable category}


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

%\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
    \[
    \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{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 universal 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}


\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{proposition}
    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{proposition}
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}


\begin{remark}[Relationship with calculus]\label{RemarkCalculus}
    The crucial observation to prove the above proposition is the next equality:

%     \begin{lemma}[recursive definition of Nim-sum]
% For any two finite sets $S,T\subset \N$ of natural numbers, the following equation holds:
% % \[\mex{S}\nsum \mex{T} = \mex{\{s\nsum \mex{T}\mid s\in S\}\cup \{\mex{S}\nsum t\mid t\in T\}}.\]
\[\mex{S}\nsum \mex{T} = \mex{S\nsum \mex{T} \cup \mex{S}\nsum T},\]
% \end{lemma}
where $S\nsum \mex{T}$ is an abbreviation of $\{s\nsum \mex{T}\mid s\in S\}$. This equation is informative enough to redefine the notion of nim-sum recursively.

This equation looks like a calculation of integral. Let $\int : C^{\infty}(\mathbb{R}) \to C^{\infty}(\mathbb{R})$ be a function that sends 
\[f(x) \mapsto \int_{0}^{x}f(t) dt.\]
Then, we have 
\[\textstyle \int f  \cdot \int g  = \int (f  \cdot\int g + \int f \cdot g),\]
which is just the integral version of the Leibniz rule! It is also called (a special case of) \emph{Rota-Baxter equation}. 
There might be a relationship with other categorical treatments of differential structures 
\cite{castillo2009rota}
\cite{cockett2019integral}
\cite{laird2013constructing}
\cite{loregian2021differential}.
\end{remark}
% \memo{This equality is reminiscent of the derivative. In fact, Let $\partial_{0}:C^{\infty}(\mathbb{R}) \to C^{\infty}(\mathbb{R})$ be a function that sends $f$ to the constant function $f'(0)$. Then, a similar equation 
% \[2\cdot \partial_{0} f  \cdot \partial_{0} g  = \partial_{0} (f  \cdot\partial_{0} g + \partial_{0} f \cdot g).\]
% It is possible to define such an axiomatic notion of derivative on a semiring, but I'm not sure if it's useful or not. The definition of sum-game is quite similar to Leibniz's rule, so it should be some relation to the differential. Until now, I don't know what it is. One possibility is
% the notion of \emph{differential $2$-rig} \cite{loregian2021differential}.}

% \memo{I've noticed that it's more like integral rather than derivative. Let $\int : C^{\infty}(\mathbb{R}) \to C^{\infty}(\mathbb{R})$ be a function that sends 
% \[f(x) \mapsto \int_{0}^{x}f(t) dt.\]
% Then, we have 
% \[\textstyle \int f  \cdot \int g  = \int (f  \cdot\int g + \int f \cdot g),\]
% which is just the integral version of the Leibniz rule! (and might be related to Rota-Baxter algebra?\cite{castillo2009rota} \cite{cockett2019integral})
% }

% \memo{Some \dq{Differential Structure} is studied in \cite{laird2013constructing}.}

\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 preserves only \dq{graph-theoretic data} and do not preserve \dq{game-theoretic data}. For example, such a function might send an ending state of a game to a non-ending state of another game.
    \memo{Write a sketch}

    Modifying such a problematic point, we define the notion of game morphism as follows:
    \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{enumerate}
            \item if $x\rel_{\X} x'$ then $f(x) \rel_{\Y} f(x')$. \label{ConditionGraphpreserving}
            \item 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{enumerate}
    \end{definition}
    \memo{It is better to prove the paraphrase of the definition, using "preservation of recursive game value". But it might be tricky...?}

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}

Before proceeding to the following contents, we will prove a basic lemma.
\begin{lemma}\label{LemmaForgetfulFaithfulConservative}
    The forgetful functor $U \colon \Gs \to \Set$ is faithful and conservative.
\end{lemma}
\begin{proof}
    This is an immediate corollary of the coalgebraic description of games. Direct proof is also easy.
\end{proof}

\subsection{The universal game: 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 construction is, the terminal object of $\Gs$.
In this subsection, we will give an explicit description of the terminal game, using a set-theoretic notion \emph{hereditarily finite sets}. This is the starting point of the folllowing whole contents.
Although we will give proofs in this subsection, the contents in this subsection will be immediate corollaries of the following contents, and they will be reinterpreted, generalized, and utilized later. \memo{ref}

Considering the terminal games answers a question: when can we say that two different states of a game behaves in the same way?
In a given game, some two different states might behave in the exactly same way. For example, \memo{Draw a picture}.


% In this subsection, we show that the set of all hereditarily finite sets is the initial algebra and the terminal game, at the same time.
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.
     % A set $A$ is \emph{hereditarily finite} if all elements of $A$ are hereditarily finite.
     \memo{Rigorously speaking, a hereditarily finite set is a set that is ensured to be hereditarily finite by this recursive definition.} 
     $\Her$ denotes the set of all hereditarily finite sets.
\end{definition}

This recursive definition might look confusing. We give several examples of hereditarily finite sets.
\begin{example}\label{LabelExampleHereditarilyFiniteSets}
    The empty set $\emptyset$ is trivially hereditarily finite since it has no element. Therefore, $\{\emptyset\}$ is also hereditarily finite. By induction, every (set-theoretically encoded) natural number is hereditarily finite. In other words, 
    \[\N = \{0=\emptyset,\ 1=  \{\emptyset\},\ 2= \{\emptyset,\{\emptyset\}\},\ 3=\{\emptyset,  \{\emptyset\}, \{\emptyset,\{\emptyset\}\}\}, \dots\} \subset \Her.\] 
    Of course, $\Her$ is not covered by $\N$. For example, $\{\{\emptyset\}\}$ is a hereditarily finite set that is not a natural number.
\end{example}

\begin{definition}[Universal game]\label{DefinitionUniversalGame}
    The universal game $\Her$ is a game whose underlying set is the set of all hereditrily finite set $\Her$ and whose relation $\rel$ is defined by 
    \[A \rel B \iff B \in A.\]
\end{definition}

\begin{proposition}\label{PropositionUniversalIsTerminal}
    The universal game $\Her$ is the terminal object of $\Gs$.
\end{proposition}

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




\subsection{Subgames}
In this subsection, we will define the notion of subgames and prove some basic properties.

\begin{definition}[Subgame]\label{DefinitionSubgames}
    A subgame of a game $\X = (X, \rel)$ is a subset $S \subset X$ such that if $x\in S$ and $x\rel x'$ then $x' \in S$.
\end{definition}

Just to avoid the following argument becoming wordy, we introduce an accessibility relation in an obvious way:
\begin{definition}[Accessibility relation]\label{DefinitionAccessibility}
    For a game $\X=(X, \rel)$, an element $x\in X$ is \emph{accessible} from $x'$ if there exists a non-negative integer $n \in \N$ and a sequence of elements $x_0, \dots x_n$ that satisfy
    \begin{itemize}
        \item $x_0=x'$,
        \item $x_i \rel x_{i+1}$ for $0\leq i < n$, and
        \item $x_n=x$.
    \end{itemize}
    This accessibility relation is denoted by $x' \acc x$.
\end{definition}

\begin{remark}[Subgames are downward closed subset]
    % If one regards a game as a poset (by the reflective and transitive closure of $\rel$), 
    This accessibility relation is just the reflective and transitive closure of $\rel$, and defines a preorder on the underlying set $X$. Furthermore, due to the \dq{finite time} condition in Definition \ref{DefinitionGames}, it is a partial order.
    
    The notion of subgames coincides with the notion of downward closed subsets of the poset.
\end{remark}

\begin{lemma}[Generation and Cogeneration of subgames]\label{GenerationanadCogenerationOfSubgames}
    For a game $\X=(X, \rel)$ and a subset $S\subset X$, 
    \begin{itemize}
        \item there exists the minimum subgame of $\X$ that contains $S$.
        \item there exists the maximum subgame of $\X$ that is contained by $S$.
    \end{itemize} 
\end{lemma}
\begin{proof}
    This is an immediate corollary of the general adjoint functor theorem applied to the complete lattice inclusion from the lattice of subgames into the lattice of subsets.

    Explicitly, the former subgame is constructed as
    \[\{x\in X\mid \exists s \in S, \ s\acc x\},\]
    and the latter is 
    \[\{x\in X\mid \forall y \in X,\  (x\acc y \implies y \in S)\}\]
\end{proof}

\begin{definition}\label{SubgameGeneration}
    For a game $\X=(X, \rel)$ and a subset $S\subset X$, the minimum subgame of $\X$ that contains $S$ is called the subgame generated by $S$, and denoted by $\gen{S}$.
\end{definition}

\begin{lemma}\label{LemmaFinitelygeneratedSubgameisFinite}
    A subgame generated by a finite subset is finite.
\end{lemma}

\begin{lemma}[Image is a subgame]\label{LemmaImageisSubgame}
    For a game morphism $f\colon \X \to \Y$, its image $\Image{f}$ is a subgame of $\Y$.
\end{lemma}
\begin{proof}
    This is due to the second condition (\ref{conditionLocallySurjective}) of Definition \ref{DefinitionGameMorphism}.
\end{proof}

\begin{proposition}[Surjection-Subgame factorization]\label{PropositionSurjSubgameFactorization}
    A game morphism is uniquely factored into a composition of a surjective morphism followed by a subgame inclusion.
\end{proposition}

We obtain the following factorization system, which will turn out to be the epi-mono factorization (see \memo{ref})
\begin{proposition}[Subgames $=$ Subobjects]\label{PropositionSubgameAndSubobjectAndMono}
    For a game morphism $f\colon \X \to \Y$, the following conditions are equivalent:
    \begin{enumerate}
        \item $f$ is monic in $\Gs$. \label{ConditionMonic}
        \item $f$ is injective. \label{ConditionInjective}
        \item $f$ is (canonically isomorphic to) a subgame inclusion.\label{ConditionSubobject}
    \end{enumerate}
\end{proposition}
\begin{proof}
    The implications $\ref{ConditionSubobject} \implies \ref{ConditionInjective}$ and $\ref{ConditionInjective} \implies \ref{ConditionMonic}$ are easy to prove. We prove the converses.

    First, we prove $\ref{ConditionMonic}\implies \ref{ConditionInjective}$. Suppose $f$ is monic. We prove that $\# f^{-1}(y) \leq 1$ by induction on the well-founded order structure $(Y,\acc)$. Assuming that, for any $y' \acc y$ and $y\neq y'$, $\# f^{-1}(y') \leq 1$ holds, we prove $\# f^{-1}(y) \leq 1$. If $\# f^{-1}(y) =0$, then the proof is completed. So we can assume $\# f^{-1}(y) \geq 1$. In that case, $\# f^{-1}(y') =1$ for any $y'\neq y$ that is accessible from $y$. Let us define $S\subset X$ as
    \[
    S \coloneqq \{x\in X\mid f(x)\neq y \text{ and } y \acc f(x)\}.
    \]
    It is not hard to prove that $S$ is a subgame of $\X$. We define a new game $\W$,
    % whose underlying set is $S \coprod \{\ast_0, \ast_1\}$. The relation $\ast_i \rel_{\W} s$ for $i=0,1$ and $s\in S$ is defined by
    % \[
    % \ast_i \rel_{\W} s \iff y\rel_{\Y} f(s)
    % \]
    % and no other relation is added.
     whose underlying set is $S \coprod \{\ast\}$. The relation $\ast \rel_{\W} s$ for $s\in S$ is defined by
    \[
    \ast \rel_{\W} s \iff y\rel_{\Y} f(s)
    \]
    and no other relation is added. \memo{This is a game, since $S$ is finite.}Then, for any $x\in f^{-1}(y)$, the function $g_{x} \colon \W \to \X$ defined by
    \[
    g_{x}(w) =
    \begin{cases}
        s &(w=s\in S)\\
        x & (w= \ast)
    \end{cases}
    \]
    is a game morphism. It is because, for any $x'\in \X$,
    \begin{align*}
        x \rel_{\X} x' &\iff y= f(x) \rel_{\Y} f(x')\\
        &\iff x'\in S \text{ and }y \rel_{\Y} f(x')\\
        &\iff x'\in S \text{ and }\ast \rel_{\W} x',
    \end{align*}
    where the first equivalence is due to the induction hypothesis. For any (possibly non-distinct) $x_0, x_1 \in f^{-1}(y)$, we have a diagram
    \[
    \begin{tikzcd}
        \W\ar[r,"g_{x_0}", shift left]\ar[r,"g_{x_1}"',shift right]&\X\ar[r,"f"]&\Y,
    \end{tikzcd}
    \]
    with the same composite.
    Since we assumed that $f$ is monic, we obtain $g_{x_0} = g_{x_1}$ and $x_0 = x_1$.

    Next, we prove $\ref{ConditionInjective}\implies \ref{ConditionSubobject}$. Suppose $f$ is injective. Then $f$ is factored as 
    \[
        \X \to \Image{f} \to \Y,
    \]
    where $\Image{f} \to \Y$ is a subgame inclusion (Proposition \ref{PropositionSurjSubgameFactorization}). Since $\X \to \Image{f}$ is a bijective game morphism, it is an isomorphism (Lemma \ref{LemmaForgetfulFaithfulConservative}).
\end{proof}




%\newpage
\section{Games as coalgebras}
\subsection{Games are well-founded 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}

Now, we automatically obtain two categories: $\PfAlg, \PfCoalg$.

Notice that our formulation of games is a special case of $\Pf$-coalgebra.
In fact, for a game $\X = (X,\rel)$, we can define a structure map $\str:X \to \Pf(X)$ as $ x \mapsto \str (x) =\{x'\in X\mid x\rel x'\}$. The definition of games ensures the finiteness of $ \str(x)$.

\begin{example}[Nim as a coalgebra]\label{ExampleNimCoalgebra}
    Let $\nu:\N \to \Pf(\N)$ denote the $\Pf$-coalgebra structure map of the 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{Such an appearance of a set-theoretic phenomenon is kind of necessary. Because both the initial algebra and the terminal game are the set-theoretic object $\Her$, the set of all hereditarily finite sets, and Nim (with this structure map) is the sub-coalgebra of the terminal game $\Her$. See next subsection.}
\end{example}


\begin{proposition}\label{PropositionEquivalenceWithWellFoundednessandRecursiveness}
    For a $\Pf$-coalgebra $\X$, the following conditions are equivalent:
    \begin{itemize}
        \item $\X$ is a game.
        \item $\X$ is well-founded. (Appendix \ref{AppendixCoalgebraicMethod})
        \item $\X$ is recursive. (Appendix \ref{AppendixCoalgebraicMethod})
    \end{itemize}
\end{proposition}
\begin{proof}
    \cite{adamek2020well}
\end{proof}


\begin{theorem}[Games are well-founded coalgebras]\label{TheoremGamesAreWellFoundedCoalgebras}
    The category of games $\Gs$ is isomorphic to the category of well-founded $\Pf$-coalgebras ($=$ the category of recursive $\Pf$-coalgebras.)
\end{theorem}

% \begin{definition}[Category of Games]
%     The category of games $\Gs$ is the full subcategory of $\PfCoalg$ that consists of all games.
% \end{definition}



\subsection{Classical values of games are hylomorphisms}
\memo{I'll rewrite this in terms of recursive coalgebra, later.}

% By Theorem \ref{TheoremTwoUniversalities}, now we have a categorical machinery! 
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}

For a game $\X = (X,\str)$ and a $\Pf$-algebra $\A = (A,\alpha)$,
we have the canonical function $!_{\A} \circ !_{\X}:X \to A$ given by 
\[
    \begin{tikzcd}
        X\ar[r,"!_{\X}"]\ar[d,"\str"]&\Her \ar[r,"!_{\A}"]\ar[d,<->,"\id{\Her}"]& A\\
        \Pf(X)\ar[r,"\Pf(!_{\X})"]& \Pf(\Her) \ar[r,"\Pf(!_{\A})"]& \Pf(A) .\ar[u,"\alpha"']
    \end{tikzcd}
\]
The morphism $!_{\X} :\X \to \Her$ is the unique morphism to the terminal game $\Her$, and the morphism $!_{\A} :\Her \to \A$ is the unique morphism from the initial algebra $\Her$.
\begin{center}
    \includegraphics[scale=0.15]{images/Picture_Coalg.jpeg}
\end{center}

Then, to obtain a nice value on a game state, now it's enough to define a nice $\Pf$-algebra! \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 able to be dealt with by some appropriate algebras. Furthermore, we can consider other data of graphs, 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 $\Her$ 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.}



So far, we have observed that once we fix a $\Pf$-algebra $\A=(A,\alpha)$, then we obtain a canonical function $X\to A$ from an arbitrary game $\X=(X,\str)$. In this subsection, we show how the notion of the Grundy number is derived from this framework.

Because we need a function from the set of game states $X$ to $\N$, we define $\Pf$-algebra structure on $\N$. But what is that? Is there any \dq{canonical} way to define a $\Pf$-algebra structure $\Pf(\N)\to \N$?

We already know that there is a natural $\Pf$-coalgebra structure $\nu:\N \to \Pf(\N)$ (see \ref{ExampleNimCoalgebra}). This is canonical in some senses. 
\begin{itemize}
    \item It is the sub-game of the terminal game $\Her$.
    \item It is $\Nim{1}$.
    \item Under the conventional set-theoretic formulation of natural numbers, it is just the inclusion of the subset (von Neumann's definition).
\end{itemize}

Now, we need a natural function $\N\to \Pf(\N)$, and we need an opposite direction function in a canonical way.
Then we category theorists think that \dq{ok, then consider its adjoint!}
\[
    \begin{tikzcd}
        \N \ar[r, shift left= 5pt,"\nu" name=A]&\Pf(\N)\ar[l, shift left= 5pt, "?"name=B]\ar[phantom, from= A, to=B, "\dashv" rotate=-90]
    \end{tikzcd}
\]
And the adjoint turns out to be mex! Here, we consider the usual orders, namely, the usual order $\leq$ on $\N$ and the inclusion relation on $\Pf(\N)$. \memo{there is also a left adjoint. And it also gives an interesting value of a game state, called \emph{birthday} of a game}

\begin{proposition}[Origin of mex]
    The right adjoint of $\nu$ is $\m$.
    \[
    \begin{tikzcd}
        \N \ar[r, shift left= 5pt,"\nu" name=A]&\Pf(\N)\ar[l, shift left= 5pt, "\m"name=B]\ar[phantom, from= A, to=B, "\dashv" rotate=-90]
    \end{tikzcd}
\]
\end{proposition}
\begin{proof}
    Take any $n\in \N$ and $S\in \Pf(\N)$. Then, we have
    \begin{align*}
                n\leq \mex{S} 
        &\iff   n\leq \min {S^{\mathrm{c}}}\\
        &\iff   \nu (n)^{\mathrm{c}} \supset S^{\mathrm{c}}\\
        &\iff   \nu (n) \subset S.
    \end{align*}
\end{proof}

In this sense, $(\N, \m)$ is one canonical choice of $\Pf$-algerba structure on $\N$. 

Then we have the canonical function from $\Her$ to $\N$.

\begin{definition}\label{DefinitionMu}
    $\mu:\Her \to \N$ denotes the unique $\Pf$-algebra morphism from the initial algebra $(\Her, \id{\Her})$ to  $(\N, \m)$.
\end{definition}

\begin{theorem}[Origin of Grundy number]
    % For a game $\X = (X, \str)$, the value of $x \in X$ by the canonical function coincides with the Grundy number $\G{\X}{x}$.
    For a game $\X$, the composite function $\mu \circ !_{\X}$ coincide with $\mathcal{G}_{\X}$
        \[
            \begin{tikzcd}
                X\ar[r,"!_{\X}"]\ar[rr,bend right,"\mathcal{G}_{\X}"']&\Her\ar[r,"\mu"]&\N
            \end{tikzcd}
        \]
\end{theorem}

% \memo{A morphism from a coalgebra to an algebra is called a \emph{coalgebra-algebra morphism}. Furthermore, such a unique coalgebra-algebra morphism is called \emph{a hylo morphism} in computer science. Games are characterized in terms of coalgebra-algebra morphisms. See Appendix \ref{AppendixGameAsWellFounded}.}



\begin{example}[Grundy number vs Birthday]
    Let $\mathrm{xem}$ be the left adjoint of $\nu$. (This is the dual of $\m$!)
    \[
    \begin{tikzcd}
        \N \ar[r, shift left= 5pt,"\nu" name=A]&\Pf(\N)\ar[l, shift left= 5pt, "\mathrm{xem}"name=B]\ar[phantom, from= A, to=B, "\dashv" rotate=90]
    \end{tikzcd}
\]
Then, the induced value of a game state is what's called \emph{the birthday of a game}.
\end{example}

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

\begin{example}[Outcome vs Existence of possible move]
    For some poset $\mathbb{P}$, we can conduct the same procedure for another , i.e. we consider 
    \[
        \begin{tikzcd}
            \nu:\mathbb{P} \ar[r, "" name=A]\ar[r,""'name=D]&\Pf(\mathbb{P}),\ar[l, shift left= 10pt, ""name=B]\ar[phantom, from= A, to=B, "\dashv" rotate=-90]
            \ar[l, shift right= 10pt, ""'name=C]\ar[phantom, from= C, to=D, "\dashv" rotate=-90]
        \end{tikzcd}
    \]
    where $\nu(p) = \{q\in \mathbb{P}\mid q<p\}$.
    In the case of $\mathbb{P} = \{\bot,\top \}$, we have two different value of games $X \to \{\bot,\top \}$. One is the \emph{outcome} ($\bot = P, \top = N$) of a game state and the other is the truth value of \dq{There is a possible move}.
\end{example}

\begin{example}[Size vs Mobius Inversion]
    Consider the following two algebra structures on $\Z$,
    \[
    \Pf(\Z)\to \Z: S\mapsto 1\pm \sum_{s\in S} s.
    \]
    For the plus case, the induced value is what should be called the \emph{size} of game, the total number of finite sequence of moves. NOOOOOOOO\memo{This is not a common name.}

    For the minus case, it gives the generalization of the mobius function of a finite poset, introduced in \cite{rota1964foundations}. \memo{For a modern treatment via category theory, see \cite{leinster2012notions}. This may lead us to a definition of the \emph{Euler characteristics} of a game \cite{leinster2008euler}.}
\end{example}

\begin{example}[Expected time vs Losing possibilityNOOOOOOOOOOOOOOOO]
    How about the case where we change the sum term $\sum_{s\in S} s$ into the average?
    \[S \mapsto 1\pm \frac{1}{\# S}\sum_{s\in S} s\]
    Here, we regard the average $\frac{1}{\# S}\sum_{s\in S} s$ of an empty set to be $0$.

    Those values are related to the \dq{random play} of the game.
    Although game theory makes the customary assumption that the player is smart enough, we can also consider \dq{foolish enugh} players do completely random moves. 
    
    For the plus case, the induced value is the expected time the game will take to finish. For the minus case, the induced value is the losing possibility.
\end{example}

\begin{example}[Ackerman's Interpretation]
    Throughout this paper, $\Her = \Pf(\Her) $ is the crucial fact. But is it necessary to consider $\Her$? 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.
    
    One canonical choice of such bijection is
    \[\Pf(\N)\to \N \colon S \mapsto \sum_{s\in S} 2^s.\]
    It is simply a binary expression and hence bijective.

    The induced function $\mathrm{Ack}\colon\Her \to \N$ is called \emph{Ackerman's interpretation} \cite{ackermann1937widerspruchsfreiheit}. In fact, $\mathrm{Ack}$ gives an isomorphism between them as $\Pf$-algebras and $\Pf$-coalgebras (or, games).
\end{example}

\memo{Winning Strategy, Entropy}


%\newpage
\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}






%\newpage
\section{\memo{Game operations and Monoidal structures}}
\memo{This is a some sort of \href{https://ncatlab.org/nlab/show/microcosm+principle}{microcosm principle}.}

%\newpage
\section{Categorical origin of Nim sum}
Another mystery still remains: the origin of the nim-sum. In this section, we derive the nim-sum operation from the monoidal structure (game-addition) on $\Gs$.

\subsection{Addition of games as monoidal structure}
First, we state that the addition of games is monoidal. 
\begin{definition}
    The unit game $\I$ is a game with only one state $\ast$ and no possible moves.
\end{definition}
\begin{proposition}
    The addition of games $\otimes$ together with the unit game $\I$ forms a symmetric monoidal structure on the category of games $\Gs$.
\end{proposition}

\memo{Is it monoidal closed? Is there any categorical characterization (or description) of this symmetric monoidal structure?}
\subsection{\texorpdfstring{Canonical monoid structure on $\Her$}{Canonical monoid structure on Hereditarily finite sets}}
Recall that, in general, the terminal object of a monoidal category has a unique monoid structure (with respect to the monoidal structure). 
\begin{definition}\label{DefinitionCanonicalMoinoid}
    The \emph{canonical monoid structure} on $\Her$ is the unique ($\otimes$-)monoid structure on the terminal game $\Her$, denoted by \[\cp:\Her \times \Her \to \Her.\]
\end{definition}

Explicitly, it is recursively defined as 
\[A\cp B =\{a\cp B\mid a\in A\}\cup \{A\cp b \mid b \in B\},\]
and the identity element is the empty set $\emptyset$.

\memo{This is just another formulation of the addition of games. And this may be (injectively or not injectively) embedded into the abelian group of Conway games. This is also reminiscent of the Leibniz rule.}
\memo{This definition of monoidal structure is categorically similar to the construction of the monoidal structure on a local state classifier \cite{hora2023internal}. There should be some general theory of a monoid structure on a colimit of a subcategory and may be related to a factorization system...(?)}

\subsection{Categorical origin of nim-sum}

So far, we obtain two naturally defined structures, namely the monoid $\Her$ (Definition \ref{DefinitionCanonicalMoinoid}) and the canonical morphism $\mu:\Her \to \N$ (Definition \ref{DefinitionMu}). By those canonical structures, we can derive the structure of nim-sum.

\begin{theorem}[Origin of nim-sum]
\memo{Just to emphasize that we could derive the nim-sum, we divide theorem into two parts.}
    \begin{enumerate}
        \item There is exactly one monoid structure on $\N$ such that $\mu: \Her \to \N$ is a monoid homomorphism.
        \item The unique monoid structure coincides with nim-sum $\oplus$.
    \end{enumerate}
\end{theorem}

\memo{When the canonical map induce monoid structure?}


%\newpage

%\newpage
\section{\memo{Application to Cyclic Nim}}

\subsection{\memo{The universal quotient of a monoid of games}}

\begin{definition}
    For a monoid $M$, a set $S$ and a function $f\colon M \to S$, the \emph{universal quotient} of $M$ with respect to $S$ is a surjective monoid homomorphism $p\colon M \to N$ such that
    \begin{enumerate}
        \item $f$ factors through $p$ (as a function). \label{ConditionSfactor}

        \item For an arbitrary surjective monoid homomorphism $p' \colon M \to N'$ satisfying condition (\ref{ConditionSfactor}), there exists a monoid homomorphism $q\colon N' \to N$ such that $p = q\circ p'$.

                \[
        \begin{tikzcd}
            M\ar[rr,"f"]\ar[rd,"p'", two heads]\ar[rdd,"p"', two heads]&&S\\
            &N'\ar[ru,dashed]\ar[d,"q", dashed]&\\
            &N\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 universal quotient of $M$ with respect to $S$ exists, and is unique (up to a canonical isomorphism).
\end{proposition}
\begin{proof}
    This follows from the general adjoint functor theorem.
\end{proof}

\begin{proposition}[Grundy number is the universal quotient of Conway addition with respect to outcomes!]\label{PrpopositionElementaryOriginOfGrundyNumber}
    The universal quotient of the monoid $(\Her, \cp)$ of hereditarily finite sets and the Conway addition, with respect to the outcome $f\colon \Her \to \{P, N\}$ is given by the monoid of nim-sum $(\N, \nsum)$ and the surjective monoid homomorphism $\G{\Her}{}\colon \Her \to \N$ sending a hereditarily finite set to its Grundy number. 
\end{proposition}

\begin{proposition}[Remoteness]\label{PrpopositionElementaryOriginOfRemorteness}

\end{proposition}

\memo{We are interested in the universal quotient of selective sum w.r.t. Grundy number.}


%\newpage

\section{Future works}\label{SectionFutureWorks}
Replacing $\Pf$ with other endofunctors to describe other types of game theory, like partisan, probabilistic, mis\`ere, transfinite, and loopy games.
\appendix
% %\newpage
% \section{Games and Grundy numbers}
%\newpage
\section{Coalgebraic Methods}\label{AppendixCoalgebraicMethod}
\subsection{Coalgebras of an endofuntors}
\begin{definition}[Coalgebra]\label{DefinitionCoalgebra}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a $T$-coalgebra is a pair of an object $X \in \ob{\C}$ and a morphism $\theta \colon X \to TX$.
\end{definition}

\begin{definition}[Coalgebra morphism]
\label{DefinitionCoalgebraMorphism}
    For an endofunctor $T\colon \C \to \C$ on a category $\C$, a morphism of $T$-coalgebras from $(X, \theta)$ to $(X',\theta')$ is a morphism $f\colon X \to X'$ in $\C$ such that 
    \[
    \begin{tikzcd}
        X\ar[r,"f"]\ar[d,"\theta"]&X'\ar[d,"\theta'"]\\
        TX\ar[r,"Tf"]&TX'
    \end{tikzcd}
    \]
    commutes.
\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}$.
\end{notation}

\begin{proposition}[Colimits of coalgebras]\label{PropositionColimitsOfCoalgebras}
    The canonical forgetful functor $\Coalg{T}\to \C$ is conservative and strictly creates all colimits that $\C$ has.
\end{proposition}
\begin{proof}
    \memo{Cite!}
\end{proof}


\subsection{Well-founded coalgebras}
For details of what follows and advanced topics, see \cite{taylor1999practical}.
For now, see \href{https://ncatlab.org/nlab/show/well-founded+coalgebra}{[well-founded coalgebra]} in nLab.

\begin{definition}[Inverse image]\label{DefinitionInverseImage}
    An \emph{inverse image} is a pullback of a cospan
    \[
    \begin{tikzcd}
        &B\ar[d,"f"]\\
        C\ar[r,"g"]&D,
    \end{tikzcd}
    \]
    where either $f$ or $g$ is monic.
\end{definition}

\begin{definition}[taut functor]\label{DefinitionTaut}
    Assuming a category $\C$ has all inverse image, a functor $T\colon \C \to \D$ is said to be \emph{taut} if $T$ preserves all inverse image.
\end{definition}

\begin{lemma}\label{LemmaTautPreservesMonos}
    A taut functor preserves monomorphisms.
\end{lemma}

\begin{definition}
    Let $\C$ be a finitely complete category $\C$ and $T \colon \C \to \C$ a taut endofunctor.
    For a $T$-coalgebra $\theta \colon X\to TX$,
    \begin{itemize}
        \item A subobject $S\rightarrowtail X$ is \emph{$\theta$-inductive}
    \end{itemize}
    is \emph{well-founded} if
\end{definition}


\subsection{Recursive coalgebras and Hylomorphisms}
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.

\section{\memo{N-player wins almost all games}}

\section{\memo{Games fail to be sheaves}}
\subsection{\memo{The site of short games}}

We call a game with \dq{starting state} a short game.
\memo{This is a common convention in combinatorial game theory.}
\begin{definition}[Short game]\label{definitionShortGames}
    A game $\X= (X, \rel)$ is a \emph{short game} if there exists $x\in X$ such that every element is accessible from $x$.
\end{definition}
In other words, a short game is a game generated by one element.


\begin{lemma}
    A short game is finite.
\end{lemma}
\begin{proof}
    Due to K\"onig's lemma.
\end{proof}

\begin{definition}
    A \emph{site of short games} $(\C, J)$ is defined as follows:
    \begin{itemize}
        \item $\C$ is the full subcategory of the category of games $\Gs$ that is spanned by all short games.
        \item A site $S$ is $J$-covering if $S$ contains an epimorphism.
    \end{itemize}
\end{definition}
\memo{Check the stability}

\begin{question}
    Is the sheaf topos $\mathrm{Sh}(\C,J)$ equivalent to $\Gs$?
\end{question}

\begin{question}
    If so, is it coherent?
\end{question}

\memo{If so, that implies that $\Gs$ is locally finitely presentabile.}

\memo{The category of short game is not coherent, since it does not have a terminal object. (One might be able to replace $\C$ with the category of countable-size games.) But it really resembles a regular topology.}

\begin{question}
    Does the notion of birthday coincide with the levels of the topos? Maybe not, they might be downward closed sets of hereditarily finite sets.
\end{question}

% \subsection{\memo{Simplicail set like strucure}}
% Levels of topos, just like simplicial sets.


\printbibliography
\end{document}