型理論
type theory
單純型附きλ計算 (simply-typed lambda calculus)$ \lambda\to
型無しλ計算
分岐型理論 (ramified type thory)
依存型理論 (dependent type theory) homotopy 型理論 (homotopy type theory; HoTT)
univalence axiom
higher inductive type
等式型 (identity type。path type)
部分構造型 (substructual type system)