次元概念の欠如
Isabelleの用語法の無茶苦茶さや、概念の混乱、理解のためのミッシングリンク、これらの大きな部分は「次元概念の欠如」によるのではないだろうか？ -- まず間違いない。
- 参考：シーケント計算、ムービー、高次圏 - 檜山正幸のキマイラ飼育記 メモ編
- 参考：バートレット、ラウダの論文 - 檜山正幸のキマイラ飼育記 メモ編
- 参考：ストリング図 - 檜山正幸のキマイラ飼育記 メモ編
Coqなら、次元ごとに次のような呼び方をすればよい。
- 0次元：命題、型
- 1次元：証明、項、式
- 2次元：リーズニング、推論
0次元と1次元の違いはハッキリしている。1次元と2次元がグチャグチャになりがち。証明、推論などの言葉が、1次元か2次元かハッキリしない。
Isabelleでは、
- 0次元：型
- 1次元：命題、項、式
- 2次元：証明、、推論
- 3次元：リーズニング、推論
1, 2, 3次元がグチャグチャになってる。標準的に次の言葉を使うことにする。
- 0次元：型
- 1次元：項、命題＝特別な型の項
- 2次元：証明図＝ストリング図
- 3次元：リーズニング図＝ストリング描き変え図（Bartlettのwire diagram）
0と1の区別はしているが、1,2,3次元のセルが悲惨にグチャグチャになっている。1,2,3を1次元ずつ落として、0,1,2として、命題、証明図、リーズニング図を区別すべき。証明図を2次元ストリング図（エリアなし）で表して、リーズニングをrewrite（redraw）とすると、バートレット流のwire diagramになる。
wire diagramは、チャンバーなしの3次元ストリング図（サーフェイス図）になる。サーフェイス図においては、
- 3次元図形：背景 （0-セル）
- 2次元図形：命題 （1-セル）
- 1次元図形: 命題のあいだの証明 （2-セル）
- 0次元図形： 証明のあいだのリーズニングや変形 （3-セル）
