(重複で受け取られた方はご容赦ください) 皆様，

東京大学の新屋です． 以下の要領で京都大学の上村太一氏の講演会を実施いたしますので，ふるってご参加ください．

新屋良磨 東京大学大学院情報理工学系研究科コンピュータ科学専攻 email: [email protected] mailto:[email protected]

========== 日時：8/4(金) 午後2時から 場所：東京大学 理学部化学東館2階 化東236教室

題目：Homotopy Type Theory 入門 / Fibred Fibration Categories

話者：上村太一 (京都大学数理解析研究所)

第一部 (チュートリアル): Homotopy Type Theory 入門 概要: *Homotopy Type Theory* (HoTT) は Martin-Löf 依存型理論の拡張で、 ホモトピー論に特化した型理論である。 代数トポロジーと計算機科学の橋渡しとなる分野であり、 ホモトピー論、高次圏論、数理論理学、定理証明器、依存型プログラミングなどと関わりが深い。 特に定理証明器を用いた代数トポロジーおよび数学全般の形式化に使われており、 HoTT による数学の基礎付けと定理証明器上での実装は *Univalent Foundations program* と呼ばれる。 本チュートリアルでは、Martin-Löf 依存型理論の基本的な概念と、 HoTT の重要な概念である *univalence axiom* と *higher inductive type* についてインフォーマルに解説する。 また、HoTT の圏論的意味論として弱分解系、モデル圏や Shulman の type-theoretic fibration category についても触れる。

第二部: Fibred Fibration Categories 概要: We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L"{o}f type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.