12/02/05 05:30:41.05
>>501
そうやって一階述語論理上の理論としての圏論は考えられるのは事実だけど、
そういうのがあまり出てこないのは別の理由からじゃないか？
圏論と型理論（高階算術ともいう）との間にかなり密接な関係があることは
かなり早い段階で分かっていた。
(Lambek & Scott の Introduction to Higher Order Categorical Logic など参照。)
型理論は、圏論云々よりはるか前からある「数学の基礎」候補だった。
だから圏論に合わせた一階述語理論をわざわざ作るまでもなく、
型理論を「圏論による基礎のための一階述語理論」として研究されてきたのだと
俺は理解しているがどうか。