まだ右と左
現状での思いと好みを記す。f:A, B → C のとき
- 左抽象 ΛL(f) = ^f:B → (A --o C) ここで、(A --o C) = AC
- 右抽象 ΛR(f) = f^:A → (C o-- B) ここで、(C o-- B) = CB
左適用、右適用、基本等式は
- AppL(a, ^f) = f
- AppR(f^, b) = f
モダスポネンスは
- A, (A --o C) |- C
- (C o-- B), B |- C
セリンガーに倣って、A*がAの右双対として、ストリートに倣って
- A -| B ⇔ A -| A* ⇔ *B -| B
BはAの右随伴であり、AはBの左随伴。右は右側に置き右星印、左は左側に置き左星印。随伴と双対は区別しない。余単位は
- ε: A, A* → 1
- ε: *B, B → 1
単位は並びが逆になるから：
- η: 1 → A*, A
- η: 1 → B, *B
εを適用と解釈するために
- ε: A, (A --o ⊥) → ⊥
- ε': (⊥ o-- B), B → ⊥
ペアリングを <-, -> と書くと、上なら<x, f> 、下なら <f, x>。
