Partisan games via Pfin×Pfin

Question

How much of partisan game theory is recovered by replacing $\mathcal P_{\mathrm{fin}}$ with

This is Question 5.3 of Games as recursive coalgebras.

Established starting point: short game forms

Proposition 5.4 identifies the terminal recursive $F$-coalgebra with short partisan game forms. A position has a finite set of Left options and a finite set of Right options; recursive evaluation is well founded. This recovers forms such as

An $F$-algebra gives a recursive evaluation. For normal-play outcomes, take $O=\{0,1\}^2$, where the coordinates say whether Left wins when Left starts and when Right starts. Then

with empty join $0$ and empty meet $1$, computes the four outcome classes.

The familiar recursive definitions of sum and negation apply to forms:

What this does not yet supply

Exact option-preserving maps are not playing strategies. Normal-play equality, Conway order, simplification, and contextual quotients require their own definitions and arguments. Nor does the impartial internal-hom construction automatically prove closedness for this partisan category.

The proposed comparison with short Conway values and dyadic surreal numbers therefore belongs to a separate semantic layer. Full surreal numbers also require infinite option sets and transfinite birthdays, beyond this finite-powerset setting.

Next step

For the categorical extension, establish the colimit and Conway-sum properties of $\operatorname{RecCoalg}_F$, then prove an adjunction before asserting a partisan internal hom. For the semantic extension, state the contextual equivalence and prove that its quotient agrees with the intended game-value equivalence.

The two tasks should be kept distinct: Proposition 5.4 already provides the forms; it does not by itself establish the strategy category or the value quotient.

See also the double-category question and the impartial internal hom.