[005B] 圏

$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}))$

$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}$と書く。

関数外延性を仮定する。$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)$は集合である。
• -他の公理は自明である。

$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$のそれから分かる。

$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 \} }$と定義する。

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

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

$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)$は命題である。

$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$と定義する。

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

1. 1任意の対象$x:C$に対して、恒等射$\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {Map}}}(x,x)$は同型である。
2. 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}$も同型である。

$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$と定義する。

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

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

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