新DOTN

DOTNを新記法にして、次の規則を導入しようと思う。

• Eを自明な単位圏とする。|E| = {e}, Mor(E) = {e^}
• 対象a, 射f に対して、それの格上げを a~、f~ とする。
• 関手の結合と自然変換の横結合を * とする。
• 自然変換の縦結合を ; とする。

定義：

• e.a~ := a :E→C
• e^.a~ := a^ :E→C
• e.f~ := f ::a~⇒b~ :E→C

次が成立する。

1. (a^)~ = (a~)^
2. (f;g)~ = f~;g~
3. (a.F)~ = a~*F
4. (f.F)~ = f~*F^