Homotopy Type Theory(HoTT)
ホモトピー型理論(Homotopy Type Theory; HoTT)
型理論をホモトピー理論と融合させたイメージ?
HoTTの基本的なアイディアは、型を空間、要素を点と解釈すること
計算機科学の型理論における「=」を, 位相幾何学のホモトピー同値「連続変形がある」の性質で解釈しようとする試み 構成される理論にHoTTがあると計算機上で数学の証明ができるようになる
Coq版のHoTTライブラリ
含まれているもの
理解するためには色々見る
$ a : A
$ A は空間で、$ a は空間の点
$ f: A → B
$ A → B
$ x: A
$ x は型$ A の変数(variable)
$ U は型の型(宇宙と呼ばれる)
確認用
Q. Homotopy Type Theory(HoTT)とは
Q. ホモトピーとは
Q. 型理論とは
Q. Martin-Löf型理論とは
Q. HoTTを学ぶと何がうれしいか
参考
動画
Felix Cherubini, A foundation for synthetic algebraic geometry - YouTube
https://www.youtube.com/watch?v=lp4kcmQ0ueY
関連