直観主義命題計算と型付きラムダ計算がCurry-Howard対応で同型になるということは計算機の世界ではよく知られているらしいが、命題6.14では直観主義命題計算にはハイティング代数、命題6.17ではラムダ計算にはデカルト閉圏に対して完全性定理が述べられてお…