カリー／ハワード対応を通して（標準的な）型付きラムダ計算と対応する論理は、連言（∧）と含意（⊃）を持つ論理です。これら2つの体系に共通することは、デカルト閉圏をモデルに持つことです。デカルト閉圏が繋ぎになって、2つの形式体系が結ばれていると言…

コーヒーを飲んでいて、高校生くらいの女の子達の不思議な会話。男の子が、女の子の体重やウェストを気にするのなら、まーわかるんだが。女性A：「わたし、握力、余裕で30キロ超えるから」女性B：「けっこう強いね」女性A：「27キロくらいにしておけばよかっ…