内涵平等的博弈论研究
Game-theoretic Investigation of Intensional Equalities
摘要：
本文提出了一个新的马丁-洛夫类型论（MLTT）的游戏语义，其中每个游戏都配备了选定的同构策略，表示（计算）证明（内涵）之间的平等的游戏策略。这些同构策略解释了MLTT中的命题等式。作为一个主要的结果，我们已经得到了第一个游戏语义MLTT，反驳了唯一性的身份证明（UIP）的原则，并验证了univalence公理（UA），但它不模拟非平凡的高等平等。分类，我们的模型形成了一个子结构的经典群胚模型的MLTT霍夫曼和Streicher。类似的路径从广群模型的$ω$广群模型，我们正计划推广游戏语义产生一个欧米茄广群结构来解释非平凡的同伦类型论（HoTT）的高等平等。
英文摘要：
This article presents a new game semantics for Martin-Löf 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 $ω$-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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
