12/02/06 06:32:36.80
>>548
横レスかもしらんが、型理論型理論と言ってるように、
型理論で形式化できるものは圏論を使って形式化できる。
「通常の数学」はこの範囲。しかし「通常ではない数学」が問題。
集合論でも圏論が形式化できるかが色々微妙なように、
逆に圏論での形式化では集合論的な数学が問題になる。
特に置換公理が型理論（よって圏論）とは相性が悪いので、
このスレか関連スレでも何度か話題になっているように
置換公理を使った数学（要するに集合論的な数学）をどう評価するべきかという問題になる。