まだ第４回目の講義録を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-m...
をご覧ください。後者については私の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=rep...
その後、∞ー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=rep...
にしむら 筑波大学 数学
追伸：オマケです。手持無沙汰な折にどうぞ。
https://www.youtube.com/watch?v=RpppLxnESaU
Logic-ml mailing list [email protected] http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml