Partisan forms: what the coalgebra construction establishes

A coalgebra for $\mathcal P_{\mathrm{fin}}\times\mathcal P_{\mathrm{fin}}$ assigns Left and Right option sets to each position. In the recursive case, the terminal object recovers short partisan game forms. The relevant published statement is Proposition 5.4 in Section 5.2 of Games as recursive coalgebras.

The four forms

are distinct. This distinction is about game forms, not an identification of coalgebra maps with legal playing strategies.

Sections 3.5–3.6 of that paper concern game values and the terminal impartial game; they are not a source for a partisan Joyal duality or tensor construction.

Sum and negation can be defined recursively on partisan forms, as recorded in note 3. Establishing a strategy category, closed structure, or double category requires the additional definitions and compatibility proofs stated there and in note 1.