依存型理論

依存型理論(dependent type theory)

型A

$ A

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

$ a : A

この対象は型理論では項

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

$ a =_A b : A

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

$ α = β : \mathrm{Type}

関数型(function type)

$ A → B

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

直和型

$ A + B

直積型

$ A \times B

関連

参考

メモ

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

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

Martin-Löf型理論(MTT)