  This article presents a new game semantics for Martin-L\"of type theory
(MLTT), in which each game is equipped with selected isomorphism strategies
that represent (computational) proofs for (intensional) equality between
strategies on the game. These isomorphism strategies interpret propositional
equalities in MLTT. As a main result, we have obtained a first game semantics
for MLTT that refutes the principle of uniqueness of identity proofs (UIP) and
validates univalence axiom (UA) though it does not model non-trivial higher
equalities. Categorically, our model forms a substructure of the classic
groupoid model of MLTT by Hofmann and Streicher. Similarly to the path from the
groupoid model to the $\omega$-groupoid model, we are planning to generalize
the game semantics to give rise to an omega-groupoid structure to interpret
non-trivial higher equalities in homotopy type theory (HoTT).
