ホモトピー型理論
[008C]

\(i\)を階数とする。型\(\mathord {\textnormal {\textsf {ReflGraph}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。

  • -\(\mathord {\textnormal {\textsf {Vertex}}}:\mathcal {U}(i)\)
  • -\(\mathord {\textnormal {\textsf {Edge}}}:\mathord {\textnormal {\textsf {Vertex}}}\to \mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)\)
  • -\(\mathord {\textnormal {\textsf {refl}}}:\prod _{x:\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {Edge}}}(x,x)\)
\(\mathord {\textnormal {\textsf {ReflGraph}}}(i)\)の要素を反射的グラフ(reflexive graph)と呼ぶ。