Polynominal

Lambek/Scott の Higher order categorical logic の続き。

　　Polynominal　　変数として使う射x : Hom A 1 a を追加した圏Aの拡張 A[x]
　　Functional Completeness　x を使った推論の正規形 a ∧ b → b の unique な射ψ(x)
　　internal language 集合を含む直観主義論理を表す A 上の record

で、ψ(x) が { x∈a | ψ(x) } : Hom A 1 (P a) になるってことらしい。これで internal language で集合が扱えるようになります。

結果的に全部つながってめでたいのだが、いろいろ大変だった。

　　そもそも、x は A に入ってないはずだろ? しかし、x : Hom A 1 a と書いてある....
　　Hom A 1 a は複数あるが、それは変数名なので同じものを指すはず
　　Hom A 1 a があるとは限らないじゃん

x を使った推論は5種類しかない(証明なし)。これで場合わけする。これは data φ で表す。

本には「分解してgraphで再構成」とかご無体なことが書いてある。結論から言うと、

　record Poly (a c b : Obj A )　: Set (c₁ ⊔ c₂ ⊔ ℓ)　where
　　field
　　　 x :　Hom A １ a
　　　 f :　Hom A b c
　　　 phi　:　φ x {b} {c} f

という record がψ(x)に相当する。そもそも x は局所変数なので大域的に持ってはいけないらしい。

Functional Completeness は

　record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set　(c₁ ⊔ c₂ ⊔ ℓ) where
　　x = Poly.x p
　　field
　　　fun　: Hom A (a ∧ b) c
　　　fp　 : A [　fun ∙ <　x ∙ ○ b　 , id1 A b　>　≈ Poly.f p　]
　　　uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b　 , id1 A b　>　≈ Poly.f p ]
　　　　 → A [ f　≈ fun　]

で良いらしい。fun には x は関与してないし、使う時にはxは既に存在する射 Hom A 1 α に置き換えられる。

これの存在を示すのは fp まではφの場合わけで良いだが、uniq は

　　f ≈ g → k f (ψ(x)) ≈ k g (ψ'(x))

が必要になる。locally smallなら単なる cong だが、そうでないと自明には成立しそうにない。特に、
ψ(x)と ψ'(x)の x は型が合ってるだけで値が同じとは限らない。これは「分解してgraphから再構成」
からしかでない。そして、それはまだ書けてない。なので、仮定してしまうのが早いらしい。
locally small からは出るので矛盾にはならない。

internal language と接続はこんな感じ。まだ正しいとは限らないが。

　　select : {a : Obj A} → ( φ :　Poly a Ω １ ) → Hom A １ (P a)

あとは、これを internal language で使うε形式に直せば良い。

　-- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →　f ∙ x ≈　φ x　
　record Fc {a b : Obj A } ( φ :　Poly a b １ )
　　　　 :　Set ( suc c₁　⊔　suc c₂ ⊔ suc ℓ ) where
　　field
　　　sl :　Hom A a b
　　g :　Hom A １ (b <= a)
　　g　= (A [ sl　o π' ]　) *
　　field
　　　isSelect : A [　A [ ε　o < g　, Poly.x φ　> ]　≈　Poly.f φ　]
　　　isUnique : (f : Hom A １ (b <= a) )　→ A [　A [ ε o < f , Poly.x φ　> ]　≈　Poly.f φ　]
　　　　→　A [ g　 ≈ f ]

とすれば良い。g は変わった記号を使うんだが、k14にないので作らないと...

これを示すには、そこそこ計算が必要。CCC の計算練習みたいなものだが。型を書いてみて分かったのだが、

　　εは型を持つ

なので、CCCで変換する時にεを生成する型を間違えると当然致命的。型変換 s・s ⁻¹ を挟んで途中で
切って合わせてやると良いらしい。

そこまで気がつけば、Fc の生成できました。長いけど時間がかかるだけ。これ全体がそんなものではある。

A[x]をある意味で構築できたので、coMand な関手S(a) : a ^ b → b の Kleisli 圏S(a)を考えれば普遍問題になる。
つまり、任意のA[x]がS(a)に iso になるというのが functional completeness で、それはS(a)が CCC関手である
ことを示せば良いらしい。ただ、record Poly は技巧的なので、それに使えるかどうかは謎です。

でも、とりあえず、これで、Polyniominal 圏、Functional Completeness、Internal language まではつながりました。
まだ、直観主義論理の公理はチェックしてないけど。CCCのは成立するので集合分、つなり、fuctional completeness
の確認作業になるはずです。

https://github.com/shinji-kono/category-exercise-in-agda/blob/master/src/Polynominal.agda