プロップの定義
nLabのプロップの定義はなんか変だと思う。
プロップやオペラッドの話だと、セオリーとモデル（代数＝加群＝表現）の混同がけっこうある。
んで、スッキリしたプロップの定義がやっと見つかった。
- Title: On the category of props
- Authors: Philip Hackney, Marcy Robertson
- URL: http://arxiv.org/abs/1207.2773
この論文でのプロップは、色付きΣ作用付きプロップ。Σは有限対称（置換）の圏。Σ作用を除くとnon-Σプロップというらしいが、形容詞の付け方による名称の違いは色々ある。
ハックニー／ロバートソンのいいところは、プロップ全体を圏としてみているところだ。実際はモノイド2-圏になる。モノイド二重圏（イクイップメント）になるかも知れない。
- 0-セル プロップ
- 1-セル プロップ関手（propic functor）
- 2-セル プロップ自然変換（propic natural transformation）
Catと類似のPropという圏（2-圏）が出来る。
注目すべきは、閉性（closedness）定理で、Propで内部ホムが存在する。Propは、
- 対称モノイド圏
- 完備
- 余完備
- モノイド閉
つまり、ベナボウ・コスモスになっている。
閉性定理を使うと、プロップをセオリーとみなしてのモデル圏が再びプロップになることが示せる。この定理は使い方によって凄い役に立つ。
Cがモノイド圏のとき、標準的なプロップが作れる。つまり、P:MonCat→Prop という関手がある。Aがプロップのとき、A→P(C) in Propが、C値のA-代数を定義する。よって、A-代数の全体からなる圏は [A, P(C)] in Propと指数（内部ホム）で与えられる。
