\mathrm{ITT}_n

Per Martin-Löfが構成した型理論の一つ

自然数全体の型Nや、Π-規則などから推論規則を繰り返し用いて作られる型のみを扱う