ホモトピー型理論
[002O]

\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2},a_{3},a_{4}:A\)を要素、\(p_{1}:a_{1}=a_{2}\)\(p_{2}:a_{2}=a_{3}\)\(p_{3}:a_{3}=a_{4}\)を同一視とする。同一視\(\mathord {\textnormal {\textsf {assoc}}}(p_{3},p_{2},p_{1}):(p_{3}\circ p_{2})\circ p_{1}=p_{3}\circ (p_{2}\circ p_{1})\)を構成する。同一視型の帰納法により、\(\mathord {\textnormal {\textsf {assoc}}}(p_{3},p_{2},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}\)と定義すればよい。