ホモトピー型理論
[000M] 定義

\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型とする。型\(A\times B:\mathcal {U}(i)\)\(\sum _{x:A}B\)と定義する。