前回の記事「最近の型理論： 外部化手法のもとでのパイ型と指数型」で、次のようなことを書きました。 対象を圏の外部に取り出す方法を外部化手法〈externalization〉と呼ぶとして、...[snip]... 「集合圏と似てないデカルト閉圏に対しては、外部化手法は有…