構成的圏論
圏論を知ってれば、Coqの記号がキモイ以外は読みやすい論文だった。一般の型に属する値は等しいかどうかの判定が可能とは限らないので、ある型とその型の上の同値関係のペアとしてSetoidというのを導入する。同値な要素は、等しいとみなす。まあ、HaskellのEqクラスみたいなもんかなぁ(Haskellの==は全然同値関係になってなくてもいいけど)。例えば、自然数型はCoqでもNat=Z|Suc Natみたく定義できて(記法は違うけど)、自然にSetoidとみなせる。このSetoidを集合の代わりに使って、圏を構成する。Objectの「集合」は、もはや集合ではなく、単なる型で(Object同士が等しいかどうか判定できる必要はない)、一方、射の集合は、Setoidとなっている。以下、普通の圏論のように、Setoidの圏や、圏(普通の圏じゃないので、何か呼び方考えた方がいい気が)の圏を作ることができて、こんとき、ある圏Cからある圏Dへの関手の全体にSetoidの構造が自然に入るので、圏の圏もきちんと圏になる。Objectの全体が集合やSetoidではなくて、単なる型なので、small-categoryとかbig-categoryとかいうデリケートな問題は発生しないというのが面白い。あとは、なんか適当に米田の補題まで
疑問
・有限の概念が扱いづらそう。有限Setoidとか有限圏とかどうやって定義するんだろう
・上の流儀でもToposが定義できて、Setoidの圏はToposになるんだろうか。とりあえず、有限極限とか素直に定義できなそうなので、Toposが定義できるか分からん
・Coqのライブラリ見たら普通にSetoidとかあるけど、それとは別にSetsもある。Setsは、要素が集合に含まれるか否か判定する「関数」を与える通常の集合論に近い方法(っても型理論ベースだけど)っぽい。Setoidが、型の「商」を集合とみなす感じで、Setsは、型の「部分集合」を集合にする感じ。で、Setsをベースにした圏論ってのもできると思うんだけど、それはどうなんだろう。個人的にはSetoidの方が自然だと感じる。
もっとCoq力があれば自分であれこれしたいけど、無理っぽいし、そこまでやる気も起きないな。あともっと普通の数学(群とか環考えて、表現の圏とか加群の圏とか)との接点が見えないから、あれ。
