[0000] はじめに

ホモトピー型理論(homotopy type theory, HoTT) [HoTT-Book]はホモトピー論(homotopy theory)と型理論(type theory)が融合した分野である。ホモトピー論は古典的には空間のホモトピー型(良い位相空間をホモトピー同値で同一視したもの)を調べる分野で、現代ではより一般的、抽象的になんらかの「ホモトピー」と呼ばれる緩い同一視の概念がある状況に使われる。一方、型理論は形式体系の一種で、数学の基礎言語、の内部言語、プログラミング言語、定理証明支援系などに使われる。

型理論をホモトピー論的な文脈で解釈することでこの二つの分野は密接に繋がれる。典型的には、空間のホモトピー型の集まりが型理論のモデルになる。これによって、型理論の中でのあらゆる構成は空間のホモトピー型に関する構成に翻訳できる。逆に、空間のホモトピー型のなすモデルにおいて妥当な構成を型理論に取り込むこともできる。ホモトピー型理論と言った場合、型理論とホモトピー論を関連付けて双方を調べる研究分野のことを指す場合と、ホモトピー論的に妥当な構成を取り入れた型理論のことを指す場合がある。本書では、後者のホモトピー論的に妥当な構成を取り入れた型理論とはどのようなものなのかを解説する。

ホモトピー論が型理論にもたらした重要な概念の二つは一価性公理(univalence axiom)と高次帰納的型(higher inductive type)である。一価性公理は、二つの型の間に同値(適当な意味で逆関数を持つ関数)がある時にそれらの型は同一視されることを保証する。従来の数学でも、二つの集合の間に全単射がある時にそれらの集合を同一視するのが自然であるが、この同一視は非形式的である。例えば公理的集合論において二つの集合が同一視されるのはそれらの要素が一致する時であり、全単射があるだけで本当に同一視してしまうと当然矛盾する。一方、一価性公理は形式体系における公理であり、同値がある二つの型は本当に同一視される。この同一視は型理論をホモトピー論的に解釈して初めて正当化される。

高次帰納的型は帰納的型の一般化である。通常の帰納的型はいくつかの要素の構成で自由に生成された型で、自然数のなす型、リスト型、余積などがその例である。高次帰納的型は要素の同一視の構成も含めることができる。商型、押し出しなどの余極限が典型例である。ホモトピー論的解釈を念頭に置くと、ここでいう余極限はホモトピー余極限と呼ばれるもので、円周、球面、トーラスなどの高次のホモトピー論的な情報を豊富に持つ空間を表す型を含む。