[007N] -- ホモトピー型理論

[007N] 定義

$$i$$ を階数、 $A:\mathord {\textnormal {\textsf {Span}}}(i)$ をスパンとする。型 $\mathord {\textnormal {\textsf {SpanOver}}}(A):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Left}}}:A.\mathord {\textnormal {\textsf {Left}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Right}}}:A.\mathord {\textnormal {\textsf {Right}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Center}}}:A.\mathord {\textnormal {\textsf {Center}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {leg-l}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\mathord {\textnormal {\textsf {Center}}}(x)\to \mathord {\textnormal {\textsf {Left}}}(A.\mathord {\textnormal {\textsf {leg-l}}}(x))$
- $\mathord {\textnormal {\textsf {leg-r}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\mathord {\textnormal {\textsf {Center}}}(x)\to \mathord {\textnormal {\textsf {Right}}}(A.\mathord {\textnormal {\textsf {leg-r}}}(x))$

\mathord {\textnormal {\textsf {SpanOver}}}(A)

の要素を

\(A\)

上のスパンと呼ぶ。