We present new game semantics of Martin-L\"of type theory (MLTT) equipped with One-, Zero-, N-, Pi-, Sigma- and Id-types. Our game semantics interprets MLTT more accurately than existing ones. Another advantage of our game semantics over existing ones is its interpretation of Sigma-types that is direct and compatible with the game semantics of product types . Besides, its mathematical structure is novel and useful; e.g., the category of our games has all finite limits, which is a key step to an extension of the present work to homotopy type theory, and our games interpret subtyping on dependent types for the first time as game semantics. Finally, we provide a new, game-semantic proof of the independence of Markov's principle from MLTT, which demonstrates an advantage of our game semantics over extensional models of MLTT such as the effective topos.

翻译：我们展示了马丁-L\"类型理论(MLTT)的新型游戏语义。 我们的游戏语义比现有语义更准确地解释MLTT。 我们的游戏语义比现有语义更准确地解释MLTT。 我们的游戏语义的另一个好处是对Sigma类型的解释,这种解释直接且与产品类型游戏语义兼容。 此外,它的数学结构是新颖和有用的;例如,我们的游戏类别有所有限制,这是将当前工作扩展至同质类型理论的关键一步,也是我们游戏首次解释依赖类型作为游戏语义的亚型的关键一步。 最后,我们为Markov原则独立于MLTT提供了一个新的游戏语义证明,它展示了我们游戏语义比MLTT的扩展模式(比如有效)的优势。