到達不能基数を飛び越える

現在、Agda2で某論理体系を実装中、本日からタイプチェックを始めた。論理体系なので、列計算を定義したいと考えるのは自然な考えでしょう。というわけで、命題の列を定義しようとしたのだが・・・

1. Agdaのベースとなる直観主義的タイプ理論では、Proposition = Set が原則
2. だから、例えば長さが2の命題の有限列のタイプは Set × Set ということになる。
3. つまり、ZFCの用語で言い直すと（ZFCの世界に翻訳すると）、それは V_{κ_1} × V_{κ_1}（ただしV:Universe、κ_1は一番目の到達不能基数）のオブジェクトとなる。
4. つまり、Agdaのタイプ付けではタイプが Set1、その強さは V_{κ_2}（ただしκ_2は二番目の到達不能基数）に匹敵する（Set1 と V_{κ_2}の間に双方向の埋め込みがつくれる）！

ということに。考えてみれば当たり前の話ではあるけれど・・・命題の有限列を定義するだけで到達不能基数を一つ飛び越えてしまうってどんな世界だ（泣）。