  This work extends the present author's computational game semantics of
Martin-L\"{o}f type theory to the cumulative hierarchy of universes. This
extension completes game semantics of all standard types of Martin-L\"{o}f type
theory for the first time in the 30 years history of modern game semantics. As
a result, the powerful combinatorial reasoning of game semantics becomes
available for the study of universes and types generated by them. A main
challenge in achieving game semantics of universes comes from a conflict
between identity types and universes: Naive game semantics of the encoding of
an identity type by a universe induces a decision procedure on the equality
between functions, a contradiction to a well-known fact in recursion theory. We
overcome this problem by novel games for universes that encode games for
identity types without deciding the equality.
