\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(a_{1},a_{2}:A\)を要素、\(p:a_{1}=a_{2}\)を同一視、\(b_{1}:B(a_{1})\)と\(b_{2}:B(a_{2})\)を要素とする。型\(b_{1}=_{p}^{B}b_{2}:\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {transport}}}(B,p,b_{1})=b_{2}\)と定義する。\(b_{1}=_{p}^{B}b_{2}\)の要素を\(b_{1}\)と\(b_{2}\)の\(p\)上の同一視(identification over \(p\))と呼ぶ。
[0003] 高次帰納的型
高次帰納的型(higher inductive type)は一価性公理と並んで、ホモトピー型理論において重要な概念である。通常の帰納的型は要素を構成するいくつかの構成子によって自由に生成される型であった。高次帰納的型は要素の構成に加えて、同一視の構成子も許したものである。
最も汎用的な高次帰納的型はファイバー余積または押し出しで、[0033]で導入する。ファイバー余積を使って、懸垂、\(n\)次元球面、コファイバーを構成できて、有限のCW複体を構成できることがわかる。このように、高次帰納的型は豊富に高次元の同一視の構造を持つ型を構成するのに使われる。
高次帰納的型は従来の数学(例えば集合論)でも意味をなす概念である。例えばファイバー余積は集合論でもよく使われる。しかし、集合論で同一視を追加することは要素を等しくすることになるが、追加された同一視の情報が失われる。例えば、二つの要素の間の同一視を一つ追加することと二つ追加することは区別されない。このことに起因して、集合論においては高次帰納的型は必ずしも良く振る舞わないことが知られている。一方、ホモトピー型理論においては、高次帰納的型で追加された同一視の情報が失われることはない。この事実は降下性と呼ばれる性質にまとめられ、一価性公理の下で証明される([0034])。
高次帰納的型を説明するためにいくつか準備をしておく。
\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(f:\prod _{x:A}B(x)\)を関数とする。関数