Kan's horn-filling property in homotopy type theory

開催日時
2017/06/12 月 16:00 - 17:30
場所
6号館609号室
講演者
佐藤玄基
講演者所属
東京大
概要

Homotopy type theory (HoTT) is relatively recently found connection between homotopy theory and type theory. Type theory is an important kind of formal theory studied in mathematical computer science and logic, to which HoTT provides a good interpretation. On the other hand, HoTT may be seen from the homotopy-theoretic point of view as a formal language
of synthetic homotopy theory. Awodey-Warren and Voevodsky found the relationship between the two theories. Voevodsky also proposed HoTT as a new foundation of mathematics, which he call the Univalent Foundation.

In this talk, the speaker gives a brief introduction of HoTT, and presents a result of his on it. The speaker re-interpreted Kan's horn-filling property, which simplicial and cubical sets require to be a Kan fibrant object, as a proposition internal to HoTT, and proved it. The result was achieved by utilizing combinatorial meta-argument. He also suggests a conjectural application of this result, in which the homotopy groups of finite simplicial complexes may probably be proven to be computable in HoTT.