[002Z] -- ホモトピー型理論

[002Z] 規則

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。

-余積(coproduct) $A+B:\mathcal {U}(i)$ を構成できる。
-要素 $$a:A$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{1}(a):A+B$ を構成できる。
-要素 $$b:B$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{2}(b):A+B$ を構成できる。
- $$c:A+B$$ を要素、 $$j$$ を階数、 $D:A+B\to \mathcal {U}(j)$ を型の族、 $d_{1}:\prod _{x:A}D(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ を要素、 $d_{2}:\prod _{y:B}D(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を要素とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{+}(c,D,d_{1},d_{2}):D(c)$ を構成できる。
- $$a:A$$ を要素、 $$j$$ を階数、 $D:A+B\to \mathcal {U}(j)$ を型の族、 $d_{1}:\prod _{x:A}D(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ を要素、 $d_{2}:\prod _{y:B}D(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を要素とすると、 $\mathord {\textnormal {\textsf {ind}}}_{+}(\mathord {\textnormal {\textsf {in}}}_{1}(a),D,d_{1},d_{2})\equiv d_{1}(a)$ と定義される。
- $$b:B$$ を要素、 $$j$$ を階数、 $D:A+B\to \mathcal {U}(j)$ を型の族、 $d_{1}:\prod _{x:A}D(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ を要素、 $d_{2}:\prod _{y:B}D(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を要素とすると、 $\mathord {\textnormal {\textsf {ind}}}_{+}(\mathord {\textnormal {\textsf {in}}}_{2}(b),D,d_{1},d_{2})\equiv d_{2}(b)$ と定義される。