English
Replace the move-indexing types by equivalent types via given equivalences el and er. The resulting game relabel(el,er) has LeftMoves = xl' and RightMoves = xr', with moves defined by composing the original moves with the equivalences.
Русский
Заменить типы индексирования последующих ходов на эквивалентные через заданные эквивалентности el и er. Полученная игра relabel(el,er) имеет LeftMoves = xl' и RightMoves = xr', а ходы заданы как композиции исходных ходов с эквивалентностями.
LaTeX
$$$ \\mathrm{relabel}(x;xl',xr')(el\\colon xl' \\simeq x.LeftMoves)(er\\colon xr' \\simeq x.RightMoves) = \\langle xl',\\; xr',\\; x.moveLeft \\circ el,\; x.moveRight \\circ er \\rangle. $$$
Lean4
/-- Replace the types indexing the next moves for Left and Right by equivalent types. -/
def relabel {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) : PGame :=
⟨xl', xr', x.moveLeft ∘ el, x.moveRight ∘ er⟩
