[logic-ml] homotopy type theory

[logic at math.tsukuba.ac.jp]

まだ第４回目の講義録をupしていませんが、
ここまでで

depdendent type theory with intensional identities

がどんなものかは感触はつかめたと思うので、
第５回からはそれのModelがどのようなものかの
感触をつかんでもらうことを目指します。
古典的なCategory theoryをざっと復習した後、
higher categoriesとは何なのか、どんなものでなければ
いけないか、といった点を理解してもらうつもりです。
Higher categoriesも一昔前は

そこへ踏み込んではいけない、泥沼に
足をとられるから、

と言われたものですが、今は逆にhigher categoriesなしでは
２１世紀の数学を語ることができないと言える状況だと
思います。たとえば

http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf

や

https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/master-mathematical-physics.pdf

をご覧ください。後者については私のreviewを

https://www.ems-ph.org/journals/journal.php?jrn=news

を今年の３月号でご覧いただけます。Spaceの関係で
全文を載せられなかったので、
それは筑波大学のRepositoryにおいています。

https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=35978&item_no=1&page_id=13&block_id=83

その後、∞ーgroupoidsの織り成す世界が上記の

depdendent type theory with intensional identities

のModelにほぼなっているという話をします。”ほぼ”と
いったのは、とりあえずcoherenceの問題は捨象して
という意味です。

これは強調されていることですが、上記の

depdendent type theory with intensional identities

はdecidableです。これはTaitの方法で簡単に
示すことができます。しかし

Homotopy type theory

と言った場合は、そこにunivalence axiomが入ってきますから、
これがdecidabilityを破壊してしまわないかは、まだ未解決問題です。
もしもこれが破壊してしまうという話になると
homotopy type theoristsの間に激震が走るでしょう。
その衝撃はGödelが不完全定理でHilbertの第２問題に
対して与えた衝撃に匹敵すると思います。
皆さん、そんなことはありえないとかなり楽天的に
構えています。

にしむら

追伸：オマケです。手持無沙汰な折にでもどうぞ。

https://www.youtube.com/watch?v=ibjTE5LsN1U

> 現在筑波大学で上記について講義を
> 行っていますが、それの講義Notesを
> 筑波大学のRepositoryに置いていきますので、
> ご案内しておきます。
>
> https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=37910&item_no=1&page_id=13&block_id=83
>
> にしむら
> 筑波大学
> 数学
>
> 追伸：オマケです。手持無沙汰な折にどうぞ。
>
> https://www.youtube.com/watch?v=RpppLxnESaU
>
>
> _______________________________________________
> Logic-ml mailing list
> Logic-ml at fos.kuis.kyoto-u.ac.jp
> http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
>