カリー／ハワード対応の使い途

計算解釈	論理解釈
項	証明
項ブロック	証明ブロック
ユニット型	真
エンプティ型	偽
型	命題
型構成子	論理結合子
依存型構成子	限量子
定数	公理
関数	定理
関数の定義項	定理の証明
関数のヘッダ	定理のヘッダ
定数・関数名	公理・定理ラベル
関数コンビネータ	定理コンビネータ＝手続き
原始コンビネータ	推論規則

ただし、ハイパーインスティチューションのなかでは、あまりカリー／ハワード対応を重要視するべきではない。対応が重要なのではなくて、ベースドクトリンと論理ドクトリンが同一の構造を持つというだけのこと。計算解釈はベース圏に対して使い、論理解釈は論理圏に対して使う。2つの解釈を同一視するのではなくて、共通性を意識しながらも使い分ける。