08/01/01 18:26:11
>>186
まあそうなんだけど、関数に対応するものがトポスの射になってる。
普通の集合論では、「はじめに一者あり」である。存在論的な形になっていて、その一者（実は、空）から、すべての存在が生成される。
では、Mac Lane が指摘した、論理学ではどうなるか。
ところが関数型の場合、「はじめに働きあり」である。なんじゃそりゃ、と思うかもしれない。
普通の集合論では、関数は、集合の一種（つまり、グラフ）として定義される。
でもこちらは、逆に、関数から集合を定義しようということなのだ。
この関数概念を一般化したのがシミロンのトポスの射。