[002N] 高次グルーポイド構造

要素 $a_{1},a_{2}:A$ に対して、 $a_{1}=a_{2}$ がまた型であるということは、同一視 $p_{1},p_{2}:a_{1}=a_{2}$ に対してもまた同一視型 $p_{1}=p_{2}$ がある。同一視 $q_{1},q_{2}:p_{1}=p_{2}$ に対してさらに同一視型 $q_{1}=q_{2}$ があり、これを繰り返すと好きなだけ「高次の」同一視型を得る。実は、これらの高次の同一視型たちは∞グルーポイドと呼ばれる構造の一部であることが知られている[Lumsdaine--2010-0000][van-den-Berg--Garner--2011-0000]。∞グルーポイドの構造は無限個の演算を持つ複雑なもので深入りはしない。ただ覚えておくとよいのは、あらゆる型が自動的にそのような豊富な構造を持ち、あらゆる構成が自動的にその構造と整合的になるということである。

∞グルーポイドの持つ構造の一部を挙げる。∞グルーポイドの文脈では要素 $p:a_{1}=a_{2}$ は射と呼ばれる。 $\mathord {\textnormal {\textsf {refl}}}:a_{1}=a_{1}$ は恒等射、 ${p}^{-1}:a_{2}=a_{1}$ は逆射、 $q\circ p:a_{1}=a_{3}$ は合成射と呼ばれる。 $\mathord {\textnormal {\textsf {ext}}}(p_{1},p_{2}):a_{1}=a_{2}$ は $p_{2}:a_{0}=a_{2}$ の $p_{1}:a_{0}=a_{1}$ に沿った拡張である。

[001M] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2}:A$ を要素、 $p:a_{1}=a_{2}$ を同一視とする。同一視 $\mathord {\textnormal {\textsf {ext-self}}}(p):\mathord {\textnormal {\textsf {ext}}}(p,p)=\mathord {\textnormal {\textsf {refl}}}$ を構成する。定義より $\mathord {\textnormal {\textsf {ext}}}(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ なので帰納法により $\mathord {\textnormal {\textsf {ext-self}}}(\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ と定義すればよい。

[0027] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2}:A$ を要素、 $p:a_{1}=a_{2}$ を同一視とする。同一視 $\mathord {\textnormal {\textsf {sym-sym}}}(p):{({p}^{-1})}^{-1}=p$ を帰納法により $\mathord {\textnormal {\textsf {sym-sym}}}(\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ と定義する。

[002O] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2},a_{3},a_{4}:A$ を要素、 $p_{1}:a_{1}=a_{2}$ と $p_{2}:a_{2}=a_{3}$ と $p_{3}:a_{3}=a_{4}$ を同一視とする。同一視 $\mathord {\textnormal {\textsf {assoc}}}(p_{3},p_{2},p_{1}):(p_{3}\circ p_{2})\circ p_{1}=p_{3}\circ (p_{2}\circ p_{1})$ を構成する。同一視型の帰納法により、 $\mathord {\textnormal {\textsf {assoc}}}(p_{3},p_{2},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ と定義すればよい。

[002P] 演習

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2}:A$ を要素、 $p:a_{1}=a_{2}$ を同一視とする。同一視 $\mathord {\textnormal {\textsf {unit-l}}}( p):\mathord {\textnormal {\textsf {refl}}}\circ p= p$ と $\mathord {\textnormal {\textsf {unit-r}}}( p): p= p\circ \mathord {\textnormal {\textsf {refl}}}$ を構成せよ。

[0047] 演習

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2}:A$ を要素、 $p:a_{1}=a_{2}$ を同一視とする。同一視 $\mathord {\textnormal {\textsf {inv-l}}}(p):{p}^{-1}\circ p=\mathord {\textnormal {\textsf {refl}}}$ と $\mathord {\textnormal {\textsf {inv-r}}}(p):p\circ {p}^{-1}=\mathord {\textnormal {\textsf {refl}}}$ を構成せよ。

[002R] 演習

いわゆるMac Lane五角形を表す型とその要素を構成せよ。

[002Q] 例

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

1要素 $a_{1},a_{2},a_{3}:A$ と同一視 $p_{1}:a_{1}=a_{2}$ と $p_{2}:a_{2}=a_{3}$ に対して、同一視 $\mathord {\textnormal {\textsf {ap-comp}}}(f,p_{2},p_{1}):\mathord {\textnormal {\textsf {ap}}}(f,p_{2}\circ p_{1})=\mathord {\textnormal {\textsf {ap}}}(f,p_{2})\circ \mathord {\textnormal {\textsf {ap}}}(f,p_{1})$ を構成できる。実際、 $\mathord {\textnormal {\textsf {ap-comp}}}(f,p_{2},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ と定義すればよい。
2要素 $a_{1},a_{2}:A$ と同一視 $p:a_{1}=a_{2}$ に対して、同一視 $\mathord {\textnormal {\textsf {ap-inv}}}(f,p):\mathord {\textnormal {\textsf {ap}}}(f,{p}^{-1})={(\mathord {\textnormal {\textsf {ap}}}(f,p))}^{-1}$ を構成できる。実際、 $\mathord {\textnormal {\textsf {ap-inv}}}(f,\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ と定義すればよい。

[002S] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とする。要素 $a_{1},a_{2},a_{3}:A$ と同一視 $p_{1}:a_{1}=a_{2}$ と $p_{2}:a_{2}=a_{3}$ に対して、同一視 $\mathord {\textnormal {\textsf {transport-comp}}}(B,p_{2},p_{1}):\mathord {\textnormal {\textsf {transport}}}(B,p_{2}\circ p_{1})=\mathord {\textnormal {\textsf {transport}}}(B,p_{2})\circ \mathord {\textnormal {\textsf {transport}}}(B,p_{1})$ を構成できる。実際、 $\mathord {\textnormal {\textsf {transport-comp}}}(B,p_{2},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}$ と定義すればよい。