1: \begin{abstract}

2: We present a game semantics for \emph{Martin-L\"of type theory (\textsf{MLTT})} that interprets \emph{propositional equalities} in a non-trivial manner in the sense that it refutes the principle of \emph{uniqueness of identity proofs (UIP)} for the first time as a game semantics in the literature.

3: Specifically, each of our games is equipped with (selected) invertible strategies representing \emph{(computational) proofs of (intensional) equalities} between strategies on the game; these invertible strategies then interpret propositional equalities in \textsf{MLTT}, which is roughly how our model achieves the non-trivial interpretation of them.

4: Consequently, our game semantics provides a natural and intuitive yet mathematically precise formulation of the \emph{BHK-interpretation} of propositional equalities. 

5: From an extensional viewpoint, the algebraic structure of our model is similar to the classic \emph{groupoid model} by Hofmann and Streicher, but the former is distinguished from the latter by its computational and intensional nature. 

6: In particular, our game semantics refutes the axiom of \emph{function extensionality (FunExt)} and the \emph{univalence axiom (UA)}.

7: This provides a sharp contrast to the recent \emph{cubical set model} as well.

8: Similar to the path from the groupoid model to the \emph{$\omega$-groupoid models}, the present work is also intended to be a stepping stone towards a game semantics for the \emph{infinite hierarchy of propositional equalities} in \textsf{MLTT}.

9: \end{abstract}

10: