昨日の記事「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」で話題にしたハイティング圏について、もう少しダラッと述べます。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\cat}[1]{\mathca…

カリー／ハワード／ランベック対応については、このブログ内で何度も言及しています。 このブログ内 ハワード の検索結果 論理／型理論／圏論の三者のあいだに、精密で綺麗な対応があります -- それがカリー／ハワード／ランベック対応です。カリー／ハワー…

型理論では、「代入〈substitution〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰も…