カリー/ハワード/ランベック対応の辞書 続・カリー/ハワード/ランベック対応の辞書 まだあるの? まだあります!カリー/ハワード/ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論(ラムダ計算を含む)」「論理」「圏論」の三分野のあいだの対応ですが、今回は、抽象的・一般的な圏ではなくて、集合圏と位相空間の圏を取り上げます。主に、依存型理論の概念を、論理、集合圏、位相空間の圏で何に対応するかをまとめます。先に、幾つかの言葉の説明をしておきます。 バンドル〈bundle〉: 多様体上のベクトル・バンドルなどとは違って、単なる連続写像 $`f:E \to…