カリー／ハワード／ランベック対応から見る関数と定理

関数の意味：

1. 関数そのもの＝集合圏の射
2. 関数定義
3. 関数{定義}?ヘッド＋関数{定義}?ボディ
4. 関数定義ボディは計算項

定理・証明の意味：

1. 定理（証明）そのもの＝演繹圏の射
2. 定理記述
3. 定理{記述}?ヘッド＋定理{記述}?ボディ
4. 定理記述ボディは証明項

「証明」の運用：

1. 証明＝定理＝定理そのもの＝演繹圏の射
2. 証明＝証明項＝計算項
3. 証明＝定理記述のボディ（部分〈パーツ〉名）
4. 証明＝無名定理＝定理ステートメント＋証明項
5. 証明＝定理記述

「関数」の運用：

1. 関数＝関数そのもの＝計算圏の射
2. 関数＝計算項（今はあまりない、歴史的にはあったろう）
3. 関数＝関数定義のボディ（ない）
4. 関数＝無名関数
5. 関数＝関数定義