依存型
依存型(いぞんがた、dependent type)
Martin-Löf型理論
、
依存型理論
で出てくるもの
値に依存する型
$ A: \mathcal{U}
$ \mathcal{U}
: 型の成す
宇宙
ここでいう宇宙は
グロタンディーク宇宙
$ B : A \to \mathcal{U}
型
$ A
の項
$ x : A
に応じて変わる新しい型
$ B(x)
が依存型
依存型が使えるプログラミング言語
対応するもの
(論理)
述語
$ P(x)
(集合)
集合族
$ \{ A_i\}
(型理論) 依存型
$ B(x)
(ホモトピー)
ファイブレーション
確認用
Q. 依存型
Q. 値に依存する型とは
参考
『Homotopy Type Theory: Univalent Foundations of Mathematics』
メモ
https://ja.wikipedia.org/wiki/依存型
依存型と総称型の圏論的解釈 - 檜山正幸のキマイラ飼育記 (はてなBlog)
依存型 Dependent Type: 最新の百科事典、ニュース、レビュー、研究
関連
Martin-Löf型理論
デカルト閉圏(CCC)
直観主義論理
単純型付きラムダ計算
篩型
#依存型理論
#Fleeting_Notes