なんでラムダ計算はダメなのか

通常のラムダ計算を0-計算とすると、自然演繹が1-計算で、シーケント計算（の証明）が2-計算だろう。各次元のラムダ計算がバラバラで統合されてないのがダメ。

大きなラムダ計算は統合の試みだが、ちゃんとやってないな。

デカルト閉圏の構造を写し取るのだから、最初から結合、カリー同型、積、指数が入っているほうがいい。結合、カリー同型、積まではシーケント計算でだいたいうまくいくが、指数の計算は全然不十分。特に反変指数関手が全然ダメ。