Martin-Löf型理論
Martin-Löf型理論(マーティン＝レーフかたりろん、Martin-Löf's type theory; MLTT)
あらゆる数学的対象は型(type)を持つ。数学的対象$ a が型$ A を持つことを $ a: A
と書き、$ a は型$ A の要素(element)であるともいう。
数学的対象は変数(variable)に依存する場合もあり、$ a が変数$ x に依存するかもしれないことを強調するときは$ a を$ a[x] と書く。
$ a[x] 中$ x に数学的対象 $ b を代入して得られる数学的対象を $ a[b] と書く。
二つの数学的対象が等しいことを $ a \equiv b で表す。
数学的対象$ a に名前 $ f を付けるときには$ f:\equiv a と書き、$ f を$ a と定義するなどと言う。
型A, Bに対し、AからBへの関数型(function type)を$ A → B と書く。
変数$ x:A と要素$ b[x] :B に対し、λ-抽象(λ-abstraction) $ λ(x : A):b[x] : A → B
$ \Sigma : 直和(disjoint sum) 確認用
Q. Martin-Löf型理論
Q. 依存型理論
参考・出典
メモ