依存型理論

依存型理論(dependent type theory; DTS)

$ A

型A

$ a : A

ある対象aが型Aの要素であること

$ a =_A b : A

二つの表現式が、同じ型Aの内部で等しいこと

$ α = β : \mathrm{Type}

二つの型α、βが等しいこと

$ B(x)

関数型(function type)

$ A → B

型A, Bに対し、AからBへの関数型(function type)

$ \sum_{x:A}B(x)

$ \prod_{x:A}B(x)

関連

参考

メモ

依存型理論をどうやって学べばいいか

https://youtu.be/RPIPLXeQqXk?si=QK0ExG8mXRjw7898

Martin-Löf型理論(MTT)

https://youtu.be/WSVXbNw7IxQ?si=4g6DLgh3mO2Qh8zl