タイプ理論（第五章第三節）

基本タイプ(5.31)

e,t ∈ T

a,b ∈ T である時〈a,b〉∈ T

上記以外の何物もタイプではない