Internal hom for Conway addition

Question and proposed construction

Question 5.7 of Games as recursive coalgebras asks for a concrete right adjoint to Conway addition:

Existence is proved abstractly in the paper. The proposed construction and proof below describe positions, moves, evaluation, and currying explicitly. A detailed proposed proof is in note 29.

Positions and moves

Put $S=\operatorname{Set}(UG,UH)$. By Definition B.13 and Proposition B.14, the cofree game $R(S)$ consists of hereditarily finite labelled positions $t=(T_t,a_t)$, with finite child set $T_t$ and label $a_t\in S$.

Let $A(G,H)$ consist of those $t\in R(S)$ for which every descendant $w$, including $t$, satisfies

The condition is inherited by children, so $A(G,H)$ is a subgame. Its moves are the inherited child relation.

Evaluation and currying

Evaluation is $\operatorname{ev}(g,t)=a_t(g)$. The displayed equation says exactly that it is an exact coalgebra morphism $G+A(G,H)\to H$.

For a morphism $f:G+K\to H$, take the cofree transpose of the label map $k\mapsto(g\mapsto f(g,k))$:

The morphism equation for $f$ gives the compatibility equation at every image position. The image is closed under options, so $h_f$ factors through $A(G,H)$. Conversely, evaluation uncurries any map $K\to A(G,H)$. One composite is the identity by evaluation of labels; the other is the identity by uniqueness of the cofree transpose. Thus $A(G,H)$ is the required right adjoint.

This is a construction in the category of finitely branching, finite-time games with exact coalgebra maps. The carriers need not be finite.

Status and remaining work

This is a proposed construction and proof, retained as a proof candidate rather than a human-reviewed result. The argument is stated in the precise category stated above; it does not claim a new published theorem or a completed human review.

Compute usable small examples and explain the game-theoretic meaning of these labelled positions. The construction does not identify this internal hom with player-switching or a strategy-category internal hom. It does not establish the partisan analogue. Its relation to prior mapping-object constructions also requires a separate literature comparison.