[003R] -- ホモトピー型理論

[003R] 規則

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

-ファイバー余積(fiber coproduct) $A\mathbin {{}_{f}\smash {+}_{g}}B:\mathcal {U}(i)$ を構成できる。
-要素 $$a:A$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{1}(a):A\mathbin {{}_{f}\smash {+}_{g}}B$ を構成できる。
-要素 $$b:B$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{2}(b):A\mathbin {{}_{f}\smash {+}_{g}}B$ を構成できる。
-要素 $$c:C$$ に対して、同一視 $\mathord {\textnormal {\textsf {glue}}}(c):\mathord {\textnormal {\textsf {in}}}_{1}(f(c))=\mathord {\textnormal {\textsf {in}}}_{2}(g(c))$ を構成できる。
- $d:A\mathbin {{}_{f}\smash {+}_{g}}B$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(d,E,e_{1},e_{2},p):E(d)$ を構成できる。
- $$a:A$$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(\mathord {\textnormal {\textsf {in}}}_{1}(a),E,e_{1},e_{2},p)\equiv e_{1}(a)$ と定義される。
- $$b:B$$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(\mathord {\textnormal {\textsf {in}}}_{2}(b),E,e_{1},e_{2},p)\equiv e_{2}(b)$ と定義される。
- $$c:C$$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、同一視 $\mathord {\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}\mathord {\textnormal {\textsf {-}}}\mathord {\textnormal {\textsf {glue}}}}(c,E,e_{1},e_{2},p):\mathord {\textnormal {\textsf {apd}}}(\lambda d.\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(d,E,e_{1},e_{2},p),\mathord {\textnormal {\textsf {glue}}}(c))=p(c)$ を構成できる。