Notion of Behaviour

"Notions of Behaviour and Reachable-Part and their Institutions"（http://www.cs.le.ac.uk/~akurz/Papers/beh-reach.ps）から。

Cに対する(for C)notion of behaviourとは：

• B:|C|→|C| （対象に対して定義された写像）
• 射の族 η = {η_M: M→B(M) | M∈|C|}

条件は：

1. η_Mはepiである。
2. (-)# : C(M, B(M)) → C(B(M), B(N))があって、η_M;f# = f

(-)# : C(M, B(M)) → C(B(M), B(N))の一意性は、epi条件から出てくるので、次のように定義してもよい。

• B:|C|→|C|
• epiの族 η = {η_M: M→B(M) | M∈|C|}
• M, Nごとに(-)# : C(M, B(N)) → C(B(M), B(N))
• 条件：η_M;f# = f

具体例は、オートマトンの圏で、B(M)はMの最小実現（つまり、マイヒル／ネロード定理の帰結）。M→B(M)は商集合への射影（epi）。

しかし、これは他の人が定義したbehaviour functorとはだいぶ違うな。notion of minimal realizationでしょう。まー、もっとも、B(M)=B(N)によって、behavioural equivalenceを定義できるからイイってことはあるだろうが。

結局、notion of behaviourは、unitがepiなidempotentモナドになっているので、新しい概念が出てくるわけではない。むしろ、他の圏へのbehaviour functorがあるとき、notion of behaviourをrespectすべしって感じで使うのだろうね。