圏の圏化としての高次圏

自然演繹とシーケント計算の関係は圏の圏化になっているような気がする。圏化とは、イコールを同型で置き換えることだが、一般化すると、nセルのイコールを(n+1)の可逆セルで置き換えることだ。

書き換えルールや書き換え系が重要な例。書き換えルールの適用列をセルだと思うと、「そのセルの変形＝書き換え履歴の書き換え」が出てくる。リファクタリングとか最適化だな。