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:

$$\mathbf{Game}(G+K,H)\cong\mathbf{Game}(K,[G,H]_+).$$

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

$$\theta_H(a_w(g)) =\{a_w(g'):g'\in\theta_G(g)\} \cup\{a_v(g):v\in T_w\} \quad(g\in UG).$$

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))$:

$$h_f(k)=\bigl(\{h_f(k'):k'\in\theta_K(k)\},\,g\mapsto f(g,k)\bigr).$$

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.

@misc{sumire:2610.00003:4:v5,
  author = {hora},
  title = {{Internal hom for Conway addition}},
  year = {2026},
  note = {SUMIRE:2610.00003/4, v5},
  url = {https://sumire.aiformath.jp/p/2610.00003/n/4/v/5}
}