圏

定義

圏とは、対象のクラスとよばれるクラス $O$ と射のクラスとよばれるクラス $A$ と、写像 $\mathrm{dom},\mathrm{cod}\colon A\to O$ と、写像 $\mathrm{id}: O\to A$ と写像 $\circ \colon A\times_O A :=\{(g,f)|\mathrm{dom}(g)=\mathrm{cod}(f)\} \to A$ の組 $(O,A,\mathrm{dom},\mathrm{cod},\mathrm{id},\circ)$ であって、以下の条件を満たすもののことをいう。

• $\mathrm{dom}(h)=\mathrm{cod}(g)$, $\mathrm{dom}(g)=\mathrm{cod}(f)$ なる $f,g,h \in A$ について、$$(h\circ g)\circ f=h \circ (g\circ f)$$ が成り立つ。
• $x \in O$ について、$$\mathrm{dom}(\mathrm{id}(x))=\mathrm{cod}(\mathrm{id}(x))=x$$ が成り立つ。
• $f \in A$ について、$$f\circ \mathrm{id}(\mathrm{dom}(f))=\mathrm{id}(\mathrm{cod}(f))\circ f=f$$ が成り立つ。