[logic-ml] homotopy type theory

[logic at math.tsukuba.ac.jp]

http://www.pas.tsukuba.ac.jp/english/syllabus/detail/?lang=en&major=1&no=75
http://www.pas.tsukuba.ac.jp/english/syllabus/detail/?lang=en&major=1&no=76

上記の通年の講義、４月１２日の３時限より始めます。前半（春term）はsyntax、
後半（秋term）がsemanticsです。前半はだいたい以下の本によります。

https://homotopytypetheory.org/book/

Homotopy-invariantな形でものを考えるとは
どういうことかをわかってもらいます。たとえば
Blakers-Massey homotopy excision theoremも
まずhomotopy-invariantな形に定式化して、そのうえで証明されます。
Inductionとかinductive constructionsがいかに広範囲に及ぶか
堪能してください。代数的にはinductive typeはhomotopy-initial algebra
です。Inductive typeelimination ruleがinductionで、その特殊な場合が
recursionです。円周なんかもinductiveに定義して、そのうえでその基本群が整数が
加法についておりなす群Ｚになることが証明されます。

余談ですが、筑波大学は創立より数年前までは、他大学のように
前期後期の２学期制ではなく、高校みたいに３学期制をとってきました。
それを２学期制に変更したのですが、前期後期といわずに
春term秋termという季節感を度外視した用語を用いています。
春termは４月から７月まで、秋termは１０月から２月までです。
７月も春termとは

いとをかし

と清少納言あたりなら言うと思います。この春termをA,B,Cのmodulesにわけ、
同様に秋termをA,B,Cのmodulesにわけていますので、実際上は隠れ６学期制と
いっていいかと思います。なかなか柔軟性のあるsystemと思いますが、
AからBへの変わり目がどこかは誰も即答できません。

にしむら
筑波大学
数学

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

https://www.youtube.com/watch?v=b1a1loUaBR8&nohtml5=False