[0001] 型理論

ホモトピー型理論は型理論の一種であり、型理論は一般になんらかの対象を構成するための規則群と構成されたものに関する定義を表す規則群によって定められる。[0001]では、ホモトピー型理論の基礎となる構成規則を導入する。

型理論一般における概念や表記をいくつか導入する。以下の用語は形式的に定義することもできるが、当面は普通の自然言語の意味で解釈して問題ない。

定義により等しいとは、定義を表す規則を使って等しいと導けることを意味する。定義により等しい対象は全く同じものとして扱ってよい。

構成にはいくつかの仮定が置かれることもある。仮定\(x\)の下での対象とは、どんな対象\(x\)に対しても妥当な構成で得られる対象である。

どのような種類の対象を構成できるかは型理論によって異なるが、通常は型とその要素が最も興味のある対象である。各要素には型が割り当てられている。