[005B] 圏

[005C] 定義

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

-対象(object)の型 $\mathord {\textnormal {\textsf {Obj}}}:\mathcal {U}(i)$
-射(morphism)の型の族 $\mathord {\textnormal {\textsf {Map}}}:\mathord {\textnormal {\textsf {Obj}}}\to \mathord {\textnormal {\textsf {Obj}}}\to \mathcal {U}(i)$
-恒等射(identity) $\mathord {\textnormal {\textsf {id}}}:\prod _{\lbrace x:\mathord {\textnormal {\textsf {Obj}}}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x,x)$
-射の合成(composition) $\mathord {\textnormal {\textsf {comp}}}:\prod _{\lbrace x_{1},x_{2},x_{3}:\mathord {\textnormal {\textsf {Obj}}}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{3})$
- $\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\mathord {\textnormal {\textsf {IsSet}}}(\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2}))$
- $\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {id}}},f)=f$
- $\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\mathord {\textnormal {\textsf {comp}}}(f,\mathord {\textnormal {\textsf {id}}})=f$
- $\_:\prod _{x_{1},x_{2},x_{3},x_{4}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\prod _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\prod _{f_{3}:\mathord {\textnormal {\textsf {Map}}}(x_{3},x_{4})}\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {comp}}}(f_{3},f_{2}),f_{1})=\mathord {\textnormal {\textsf {comp}}}(f_{3},\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1}))$

\mathord {\textnormal {\textsf {PreCat}}}(i)

の要素を(階数

\(i\)

の)前圏(precategory)と呼ぶ。

射の型 $\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ は集合であると要請される。これは、群の定義([004W])において $\mathord {\textnormal {\textsf {Carrier}}}$ は集合としたのと同様である。対して、 $\mathord {\textnormal {\textsf {Obj}}}$ は集合とは限らない。

[005D] 記法

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。 $$x$$ が $$C$$ の対象であることを $x:C.\mathord {\textnormal {\textsf {Obj}}}$ の代わりに単に $$x:C$$ と書く。対象 $x_{1},x_{2}:C$ に対して、 $C.\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ の代わりに単に $\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ と書く。 $x_{1}:C$ と書いた時点で $$C$$ の前圏の構造が暗黙に了解されるのでこの表記で曖昧性はない。同様に、対象 $$x:C$$ に対して、 $C.\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace$ の代わりに単に $\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace$ と書く。合成 $\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1})$ は二項演算子を使って $f_{2}\circ f_{1}$ と書く。

[006H] 例

関数外延性を仮定する。 $$i$$ を階数とする。前圏 $\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i):\mathord {\textnormal {\textsf {PreCat}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のように定義する。

- $\mathord {\textnormal {\textsf {Obj}}}\equiv \lbrace A:\mathcal {U}(i)\mid \mathord {\textnormal {\textsf {IsSet}}}(A)\rbrace$
- $\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (A,B).(A\to B)$
-恒等射は[0010]、合成は[0011]による。
-[0048]より、各 $\mathord {\textnormal {\textsf {Map}}}(A,B)$ は集合である。
-他の公理は自明である。

[006N] 例

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。前圏 $\mathord {\textnormal {\textsf {Op}}}(C):\mathord {\textnormal {\textsf {PreCat}}}(i)$ を次のように定義する。

- $\mathord {\textnormal {\textsf {Obj}}}\equiv C.\mathord {\textnormal {\textsf {Obj}}}$
- $\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (x_{1},x_{2}).C.\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})$
- $\mathord {\textnormal {\textsf {id}}}\equiv \lambda x.C.\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace$
- $\mathord {\textnormal {\textsf {comp}}}\equiv \lambda (x_{1},x_{2},x_{3}).\lambda (g:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3}),f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})).C.\mathord {\textnormal {\textsf {comp}}}(f,g)$
-前圏の公理は $$C$$ のそれから分かる。

前圏 $$C$$ の対象の間には、同一視型の他に同型という同一視の概念が考えらる。

[005E] 定義

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とする。

-型 $\mathord {\textnormal {\textsf {LInv}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1}),\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {inv}}}\circ f=\mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }$ と定義する。
-型 $\mathord {\textnormal {\textsf {RInv}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1}),\mathord {\textnormal {\textsf {id}}}:f\circ \mathord {\textnormal {\textsf {inv}}}=\mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }$ と定義する。
-型 $\mathord {\textnormal {\textsf {IsIso}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {linv}}}:\mathord {\textnormal {\textsf {LInv}}}(f),\mathord {\textnormal {\textsf {rinv}}}:\mathord {\textnormal {\textsf {RInv}}}(f)\mathclose {|\negmedspace \} }$ と定義する。

\mathord {\textnormal {\textsf {IsIso}}}(f)

の要素がある時、

\(f\)

は同型(isomorphism)であるという。

[005G] 補題

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とする。次は論理的に同値である。

1 $$f$$ は同型である。
2任意の対象 $$y:C$$ に対して、関数 $\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(y,x_{1})\to \mathord {\textnormal {\textsf {Map}}}(y,x_{2})$ は同値である。
3任意の対象 $$y:C$$ に対して、関数 $\lambda g.g\circ f:\mathord {\textnormal {\textsf {Map}}}(x_{2},y)\to \mathord {\textnormal {\textsf {Map}}}(x_{1},y)$ は同値である。

証明

1から2を示す。定義から、関数 $\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(y,x_{1})\to \mathord {\textnormal {\textsf {Map}}}(y,x_{2})$ は両側可逆であることが分かる。よって、[004K]よりこれは同値である。

2から1を示す。 $\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})\to \mathord {\textnormal {\textsf {Map}}}(x_{2},x_{2})$ が同値なので、射 $h:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})$ と同一視 $p:f\circ h=\mathord {\textnormal {\textsf {id}}}$ を得る。関数 $\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{1})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ が同値なので、同一視

f\circ h\circ f

\(=\)

{

\(p\)

}

\(f\)

\(=\)

{前圏の公理}

f\circ \mathord {\textnormal {\textsf {id}}}

から同一視

q:h\circ f=\mathord {\textnormal {\textsf {id}}}

を得る。よって、

\(f\)

は同型である。

1と3の同値性も同様である。

[005H] 命題

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とすると、型 $\mathord {\textnormal {\textsf {IsIso}}}(f)$ は命題である。

証明

[0041]より、 $$f$$ が同型であると仮定して $\mathord {\textnormal {\textsf {IsIso}}}(f)$ が可縮であることを示せばよいが、これは[005G]からすぐに従う。

[005F] 定義

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $x_{1},x_{2}:C$ を対象とする。型 $x_{1}\cong x_{2}:\mathcal {U}(i)$ を $\lbrace f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\mid \mathord {\textnormal {\textsf {IsIso}}}(f)\rbrace$ と定義する。

同型の基本性質は次のようにまとめられる。

[006X] 命題

$$i$$ を階数、 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏とする。

1任意の対象 $$x:C$$ に対して、恒等射 $\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {Map}}}(x,x)$ は同型である。
2任意の対象 $x_{1},x_{2},x_{3},x_{4}:C$ と射 $f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ と $f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})$ と $f_{3}:\mathord {\textnormal {\textsf {Map}}}(x_{3},x_{4})$ に対して、 $f_{2}\circ f_{1}$ と $f_{3}\circ f_{2}$ が同型ならば、 $f_{1}$ と $f_{2}$ と $f_{3}$ と $f_{3}\circ f_{2}\circ f_{1}$ も同型である。

証明

1は定義からすぐに確かめられる。2は[005G]と[002F]による。

圏とは、前圏であって対象の間の同型の型と同一視型が同値になるようなものである。

[005I] 定義

$$i$$ を階数とする。

-前圏 $C:\mathord {\textnormal {\textsf {PreCat}}}(i)$ に対して、型 $\mathord {\textnormal {\textsf {IsCat}}}(C):\mathcal {U}(i)$ を $\prod _{x:C}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{y:C}x\cong y)$ と定義する。
-型 $\mathord {\textnormal {\textsf {Cat}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を $\lbrace C:\mathord {\textnormal {\textsf {PreCat}}}(i)\mid \mathord {\textnormal {\textsf {IsCat}}}(C)\rbrace$ と定義する。

\mathord {\textnormal {\textsf {Cat}}}(i)

の要素を(階数

\(i\)

の)圏(category)と呼ぶ。

$$C$$ を圏とすると、恒等射は同型なので[001S]を適用できて、同値

\prod _{x_{1},x_{2}:C}(x_{1}=x_{2})\simeq (x_{1}\cong x_{2})

を得る。逆に、前圏

\(C\)

が圏であることを示すにはこのような同値を構成すれば十分である。

圏の典型例として、 $\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)$ ([006H])が圏であることを見る。

[006I] 補題

関数外延性を仮定する。 $$i$$ を階数、 $A,B:\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(A,B)$ を射とする。次は論理的に同値である。

1 $$f$$ は $\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)$ の射として同型である。
2 $$f$$ は関数として同値である。

証明

[004K]による。

[006J] 定理

関数外延性と一価性を仮定する。 $$i$$ を階数とすると、 $\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)$ は圏である。

証明

対象 $A,B:\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)$ に対して、[006I]より $(A\cong B)\simeq (A\simeq B)$ を得て、一価性と[0049]より $(A\simeq B)\simeq (A=B)$ を得る。