用語集
集合論的な関数 (Function)
ある集合$ Xからある集合$ Yへの関数とは、$ Xの全ての要素それぞれを、$ Yのいずれかの要素に対応付ける方法のこと
e.g.$ X = \{ * \},$ Y = \{ a, b, c, d \}であれば、$ * \mapsto aなどが関数 (を構成する写像) の例
対象 (Object)
初出ページ：
点のこと
注意点
対象は集合とは限りません！
射 (Morphism / Arrow)
初出ページ：
点と点を結ぶ矢印のこと
注意点
射は (集合論的な意味での) 関数とは限りません！
ある対象からある対象を結ぶ射は、1 つだけとは限りません！
Hom 集合 (Hom-Set)
初出ページ：
ある対象から別の対象に向かう、すべての射を集めた集合のこと
ある対象を$ X，別の対象を$ Yで表すとき、Hom 集合は$ \mathrm{Hom}(X, Y)で表す
注意点
任意の圏 (もっと言えば任意の 2 対象) において、Hom 集合が取れるとは限りません！ s.a. Locally Small
型とプログラムの圏で Hom 集合を考えたとき、それそのものが X => Y という 1 引数プログラムの型 に一致するわけではありません！s.a. 指数対象
合成射 (Composition Morphism)
公理：合成射の存在
初出ページ：
対象$ X,$ Y,$ Zに対して、射$ f: X \to Yと射$ g: Y \to Zが存在したとする
このとき、ショートカットする$ X \to Zなる射も存在しなければならない
射$ fと射$ gに対する合成射は、$ g \circ f: X \to Zと表す ($ f \ggg gと表す流儀もある)
公理：合成射の可換性
初出ページ：
$ g \circ fの役割 (効果) は、その圏においてどのようなものを合成とみなしたいかによって異なる
一般的には、$ fの役割 (効果) を得たのち$ gの役割 (効果) を得るように$ g \circ fを定めることが多い
注意点
$ g \circ fに必ずしも直感的な役割 (効果) が割り当てられるとは限りません！
e.g. しりとりの圏での合成射 (の定義例) は、2 つの単語を末尾と先頭でくっつけてできる単語
公理：合成射の結合律
初出ページ：
対象$ X,$ Y,$ Z,$ Wに対して、射$ f: X \to Y，射$ g: Y \to Z，および射$ h: Z \to Wが存在したとする
このとき、ショートカットする$ X \to Wなる合成射の作り方は、$ h \circ (g \circ f)と$ (h \circ g) \circ fの 2 種類が存在する
結合演算$ \circは、$ h \circ (g \circ f) = (h \circ g) \circ fを常に成立させなければならない (結合律)
性質：Hom 集合同士を結ぶ自明な関数の存在
初出ページ：
対象$ X,$ A,$ Bに対して、$ \mathrm{Hom}(X, A) \ne \emptysetかつ射$ f: A \to Bが存在したとする
このとき、合成射の存在より$ \mathrm{Hom}(X, B) \ne \emptysetも言える
なおかつ、任意の$ a \in \mathrm{Hom}(X, A)に対して$ f \circ a \in \mathrm{Hom}(X, B)が常に言えるので、$ f \circ -は$ \mathrm{Hom}(X, A)と$ \mathrm{Hom}(X, B)を結ぶ関数となる
恒等射 (Identity Morphism)
公理：恒等射の存在
初出ページ：
任意の対象$ Xに対して、$ id_X : X \to Xなる自分自身に向かう射が存在しなければならない
注意点
自分自身に向かう射が、常に恒等射になるとは限りません！
公理：恒等射の (左右) 単位律
初出ページ：
対象$ Xに流入する射を$ {}_\to fで表すとする
対象$ Xから流出する射を$ f_\toで表すとする
このとき、任意の$ {}_\to fに対して、$ id_X \circ {}_\to f = {}_\to fが常に成立しなければならない (左単位律)
同様に、任意の$ f_\toに対して、$ f_\to \circ id_X = f_\toが常に成立しなければならない (右単位律)
性質：ある対象に閉じた Hom 集合の非空性
初出ページ：
恒等射の存在より、任意の対象$ Xに対して$ id_X \in \mathrm{Hom}(X, X)が言える
これより、自分自身との Hom 集合は常に非空となる
函手 (Functor)
初出ページ：
ある圏$ \mathbb{C}における対象と射が成す (図形的な) 構造を、別の圏$ \mathbb{D}における対象と射が成す (図形的な) 構造へ、定義にしたがって対応づけるもののこと
このとき、射$ f \in \mathbb{C} : A \to Bが、射$ f' \in \mathbb{D} : A' \to A'に対応することも許容される (対象が 1 点に潰れるように、構造を対応づけても良い) s.a. グラフ準同型写像
直感的には、圏をまたいだ "対象同士の対応関係"，および "射同士の対応関係"，その 2 つ組のこと
e.g. 型とプログラムの圏における (自己) 函手であれば：
型コンストラクタ (カインド) ＝ "対象同士の対応関係"
map 関数 ＝ "射同士の対応関係"
定義：函手の準同型性
初出ページ：
函手における、射の対応づけを$ F_\toで表すとする
このとき、任意の合成可能な射$ f, g \in \mathbb{C}に対して、$ F_\to(f \circ g) = F_\to(f) \circ F_\to(g)が常に成立しなければならない
直感的には、函手によって、ある圏$ \mathbb{C}の合成射は、別の圏$ \mathbb{D}においても合成射に対応づけられなければならない，ということ
定義：(函手の準同型性における) 恒等射の保存
初出ページ：
函手における、対象の対応づけを$ F_*で表すとする
このとき、任意の対象$ X \in \mathbb{C}における恒等射$ id_X \in \mathbb{C}に対して、$ F_\to(id_X) = id_{F_*(X)}が常に成立しなければならない
直感的には、函手によって、ある圏$ \mathbb{C}の恒等射は、別の圏$ \mathbb{D}においても恒等射に対応づけられなければならない，ということ
自然変換 (Natural Transformation)
初出ページ：
ある圏$ \mathbb{C}から別の圏$ \mathbb{D}への函手として、$ F = ( F_\to , F_* ),$ G = ( G_\to , G_* )の 2 つを考えられるとする
任意の対象$ X \in \mathbb{C}に対して、それぞれの函手による移り先の対象$ F_*(X), G_*(X) \in \mathbb{D}を結ぶ射$ \theta_Xを考える
また、任意の射$ f \in \mathbb{C} : A \to Bに対して、函手による移り先の射をそれぞれ考える：
$ Fによる移り先 ＝$ F_\to(f) : F_*(A) \to F_*(B)
$ Gによる移り先 ＝$ G_\to(f) : G_*(A) \to G_*(B)
$ Fから$ Gへの自然変換$ \theta : F \Rightarrow Gとは、$ \forall X \in \mathbb{C}. \: \theta_Xなる射の組であって、$ \theta_B \circ F_\to(f) = G_\to(f) \circ \theta_Aを常に成立させるもののこと
e.g. 型とプログラムの圏の (自己函手を結ぶ) 自然変換であれば：
$ F = ( \mathtt{map_{Seq}} , \mathtt{Seq[*]} ) のようにとり、
$ G = ( \mathtt{map_{Option}} , \mathtt{Option[*]} ) のようにとる場合、
$ F から$ G への自然変換$ \theta とは、$ \forall \mathtt{X}. \: \mathtt{Seq[X]} \Rightarrow \mathtt{Option[X]} なるジェネリック関数のこと
※ 任意のプログラム$ \mathtt{f} : \mathtt{A} \Rightarrow \mathtt{B}に対して、$ \theta_{\mathtt{B}} \circ \mathtt{map_{Seq}(f)} = \mathtt{map_{Option}(f)} \circ \theta_{\mathtt{A}}が常に成立しなければならない
函手圏 (Functor Category)
初出ページ：
ある圏$ \mathbb{C}から別の圏$ \mathbb{D}への函手として、$ F = ( F_\to , F_* ),$ G = ( G_\to , G_* ),$ H = ( H_\to , H_* ), ... のように複数を考えられるとする
同様に、自然変換として$ \theta : F \Rightarrow G,$ \eta : G \Rightarrow H, ... のように複数を考えられるとする
ここで、$ \eta \circ \theta = \forall X \in \mathbb{C}. \: \eta_X \circ \theta_Xのように、各対象$ Xごとに考えて射の組をとることができる
$ \eta \circ \theta自体も 自然変換になることがいえる ため、自然変換を射とみなすような圏を考えることができる ⇒ 函手圏と呼ぶ
函手圏における対象は、函手を考えればよい
函手圏における (函手$ Fに対する) 恒等射は、恒等自然変換$ id_F = \forall X \in \mathbb{C}. \: id_{F_*(X)}を考えればよい