項tに対する型宣言 t:A を、「tはA（のひとつ）を具体的に構成する方法である」と読むと、構成的な感じがする。さらに、「tはAという命題の具体的な証明である」と読めば、証明論的な真偽解釈（に関する主張）だとも思える。型環境（変数の型宣言のリスト）Δ…