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