Internal Language

圏論の続き。竹内外史先生の層圏トポス、Lambek/Scott の Higher order categorical logic の
両方の中心的なところ

　　圏のトポスから直観主義論理を導出する

ってところですね。やっとここまで来た的な。ところが、Lambek ではInternal Language は1 page。

これが難い。そもそもAgdaは直観主義論理なので、自分自身を書くようなことになる。万能Turing machine
みたいなものだが、気をつけないと書けなくなったり、逆に変数を番号で表して詳細を展開するような羽目に。

論理をdataで構文木に展開したりするとかなり大変。竹内先生の方ではそうしていて十数ページ。なぜ、

　　1 page に収まっているのかが謎 definition 3.5

でも「型は圏A/Toposのそれ(対象)」とか書いてある。ToposはCCCだしN(自然数)も入っているので
* 0 Sn <a,b> はそれをそのまま使って良いんじゃないか? 残るは三つ。a=a' と a∈αはそこに書いてある
ように射を組み立てるだけでできた。 要するに直観主義論理の要素を圏Aの射に変換するだけなので、
マクロみたいなパターンで書いて良いらしい。

これは簡単。つまり、Topos と同じで、CCCな圏に射を付け加えるrecordとして inernal language を作れる。
これだと、Topos <=> Internal Language は、ほぼ対等になるのでよろしい。

問題は最後なんですが

{x∈a|ψ x} is λ (x∈a) →ψ x , the unique arrow α : 1 → P a such that x∈a ≈ ψ x

ってなんだよ。その the ってなんですか。ψ x ってなんだよ。で、さっぱりわからない。なんですが、
そのページの上の方を見ると、「λ (x∈a) →ψ x」がそのままある。そこか。

この前、格闘した Functional Completeness を使うとある。ところが前にやったのは割とインチキでなぁ。
そのままでは使えない。要するに、「λ (x∈a) →ψ x」なので x : 1 →a (aの要素を一つ指し示している射)
は引数(仮パラメータ)なわけだ。でも、x : 1 →a　は仮定なので圏Aにあるとは限らない。なので、
A[x] とか coKleisli圏とかの工夫が... 層圏トポスの方だと別なものを使ってる。でも、ヒントが。

そうか、ここで使える用に Functional Completeness を仮定してしまえば良い。それを実際に証明できる
かどうかは後回しで良い。

結果的にはかなり短くできたみたい。使えるかどうかはこれからだな。

record InternalLanguage (Ω : Obj A) (⊤ : Hom A (CCC.１ c) Ω) (P : Obj A → Obj A)
: Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
field
_==_ : {a : Obj A} (x y : Hom A (CCC.１ c) a ) → Hom A (CCC.１ c) Ω
_∈_ : {a : Obj A} (x : Hom A (CCC.１ c) a ) (α : Hom A (CCC.１ c) (P a) ) → Hom A (CCC.１ c) Ω
-- { x ∈ a | φ x } : P a
select : {a b : Obj A} (α : Hom A (CCC.１ c) (P a) ) → ( (x : Hom A (CCC.１ c) a ) → Hom A (CCC.１ c) Ω ) → Hom A (CCC.１ c) (P a)