ホモトピー型理論
[006U] 記法

関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(x:C\)を対象とする。要素\(\mathord {\textnormal {\textsf {gen}}}(x):\mathord {\textnormal {\textsf {よ}}}(C)(x)(x)\)\(\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace \)と定義する。