Research on homotopy type theory using simplicial methods

用单纯法研究同伦型理论

• 批准号: 17J06609
• 负责人: 佐藤 玄基
• 金额: $ 1.6万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2017
• 资助国家: 日本
• 起止时间: 2017-04-26 至 2020-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17J06609/
• 关键词: ホモトピー型理論; 単体的集合; ファイブレーション; 型族; 幾何的実現

本年度は，本研究において設定された第一の大目的を達成した．最も主要な成果は，前年度までに定義した単体的集合の幾何的実現の性質をしらべて，これがホモトピー群を保存することを証明したことである．このために，新たな構成として，単体的集合の幾何的実現を拡張する新たな構成を導入した．単体的集合はホモトピー論的な空間の組合せ論的表現であるが，ある空間の各点に対して連続的に空間が対応する族を，単体的集合におけるホモトピー論ではファイブレーションと呼ばれる種類の写像で表現する．単体的集合からホモトピー型理論的空間(これを型という)を作る操作を単体的集合から位相空間を作る操作の名から幾何的実現と呼んでいるが，単体的集合のファイブレーションをホモトピー型理論における型上の型の族に翻訳するという，幾何的実現の拡張を定義した．これにより，型上の型の族として自然に定義されるホモトピー型理論における道空間と，単体的集合のファイブレーションの幾何的実現を比較することができ，単に定義を行っただけの昨年の段階に比べ様々な性質の調査を行えるようになった．ホモトピー論的空間の不変量の中で最も重要なものの一つであるホモトピー群が，幾何的実現によって保存されることは，この直接の系である．ホモトピー論的空間の性質は，集合論におけるホモトピー論で証明可能であっても，ホモとピー論的操作しか許さないホモトピー型理論において証明可能であるかは直ちに明らかではない．一方で，集合を離散空間とみなすことで集合論のホモトピー型理論への埋込みが可能であるため，単体的集合に対する事実は同様に証明可能である．本年度の結果により，集合論で証明可能な幾何的実現のホモトピー群の計算結果が，ホモトピー型理論においても証明可能であることが示される．この成果のために，海外での研究集会で収集した情報を，本年度購入したタブレット端末に収集して用いた．

This year, the first major objective of this study was achieved. The most important achievement is to define the geometric properties of the set of units in the previous year, and to prove the preservation of the set of units. The new structure of a single body is introduced into the geometry of the set. A set of units is a set of units that represent the combinatorial theory of space. Each point in space is a set of units that represent the combinatorial theory of space. The set of units is the set of units, the set of units, the set of units, A comparison of the geometric realization of the set of units and the natural definition of the family of units on the model. A comparison of the geometric realization of the set of units and the natural definition of the family of units. The most important part of the infinite space of the theory is the realization of geometry, the preservation of geometry, and the direct system. The properties of space in set theory are proved to be possible in set theory, the operation of set theory is proved to be possible in set theory, and it is proved to be possible in set theory. A set is a discrete space and a set theory is a set theory. It is possible to prove that a set of units is the same. This year's results show that set theory proves the possibility of geometric realization. The results of this research are collected at overseas research meetings.

项目成果

Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT

HoTT 中元构造的截断半单纯集的几何实现

• 发表时间: 2018
• 作者: Kazuya Ohara;Takuya Maekawa;Yasuyuki Matsushita;Genki Sato
• 通讯作者: Genki Sato