CCC計算
本編：
オカシイと文句を垂れるなら、修正案を提示しないとね。
シーケントの左辺が型宣言の集まり、右辺が型付き代入文の集まりとなる形を仮にCCCシーケントと呼ぶ。CCCシーケントの意味はデカルト閉圏の射だが、多圏を中継する。つまり、CCCシーケント → Cから作られた多圏 → デカルト閉圏C という順。
CCCシーケントに対する操作（推論規則）は次のようなものがある。
- 左アルファ変換、右アルファ変換（左右はシーケントの左辺、右辺）
- 変換同値な項の置き換え
- 左右の換
- 左右のI-増とI-減、IはCCCの単位＝終対象
- ペアリングとアンペアリング、一般にはタプリングとアンタプリング
規則を分類するのは、分類の境界が曖昧で難しいが、以上がだいたいは構造規則。論理規則と呼ぶのは適切じゃない気がするが、論理規則に相当するのは、
- カット、圏の結合に相当
- マージ、圏のモノイド積（CCCでは直積）に相当
- λ導入とその逆、カリー化と反カリー化に相当
- ガンマ計算：γ導入 、新しい概念、γアノテーションにより累乗関手を扱う
公理シーケントは3種類準備する。
- 恒等 id
- 終射 !
- 対角 Δ
証明図の始端は公理シーケントか仮定となるシーケント。証明図は高次の射と考えて、始端と終端は高次の射の入力と出力と考える。
証明図が証明項にエンコードされるので、証明項から証明図が再現できる。証明図→証明項 の対応（符号化）はレイフィケーション。
