命題色々

1. Ax 2つのニョロニョロを仮定
2. Def 残り2つのニョロニョロを定義
3. Th 4つのニョロニョロのうち、2つを仮定すれば残り2つは出る
4. Ax 4つののベントジャンクションのうち、2つを仮定すれば残りは出る
5. Def 4つのジャンクションを使って、4つのベントコンビネータ (-)^∩, (-)_∪, ^∩(-), _∪(-) を定義する。
6. Th f^* = _∪(f^∩) = (_∪f)^∩
7. Th ^*f = ^∩(f_∪) = (^∩f)_∪
8. Th f^∩ = ^∩(f^*)
9. Th ^∩f = (^*f)^∩
10. Th ツイスト付きニョロニョロ定理
11. f^* = ^*f

ベクトルとフォーム

1. Th x:V ⇒ x^*:V^*→R
2. Th y:V^* ⇒ y^*:V→R

行列計算

1. Def a・x := x;a_∪
2. Th f^∩・x = x;f
3. Th (f;g)^∩ = g^∩*f^∩
4. Th V^∩ = unit_V
5. Th (a*b)_∪ = b_∪;a_∪
6. (univ_V)_∪ = V

双対と転置

1. Def 転置の定義
2. Th (a*b)^t = b^t*a^t
3. Th a^tt = a
4. Th (unit_V)^t = opunit_V
5. Th (f^*)^∩ = (f^∩)^t

matricial-vectorsの圏

1. Def unit_V = i_V
2. MVは圏となる。
3. VMとVectは圏同型（同値より強い）で、対象では恒等
4. コンパクト・シーケント計算

その他の話題

• ライデマイスター移動
• トレース付き圏
• 内積の計算
• 基底（枠、フレーム）による計算