http://www.pas.tsukuba.ac.jp/english/syllabus/detail/?lang=en&major=1&am... http://www.pas.tsukuba.ac.jp/english/syllabus/detail/?lang=en&major=1&am...
上記の通年の講義、４月１２日の３時限より始めます。前半（春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への変わり目がどこかは誰も即答できません。
にしむら 筑波大学 数学
追伸：オマケです。手持無沙汰な折にでもどうぞ。