locally small

こっちは圏論の話。圏論の本では良く出てくるんですが、

　　locally small とは圏のHom Setが集合なこと

って、何っているんだかさっぱりわかりません。そもそも圏論だと集合論やらないし公理も出てこない。

なんだけど、Agda で圏論の証明をやってると、

　　Hom Set の等号 ≈ には cong がない

ってのに気がつく。cong は congruent 合同なわけですが、

　　cong-≈ : ( x y : Hom A a b ) → ( f : Hom A a b → Hom A a' b' ) → x ≈ y → f x ≈ f y

のこと。Hom Set の等号は関係なので f が関係を保存しない限り、結果が等号になるかどうかはわからない。つまり反例がある。
群の写像があったとしても群の構造を保存しないなら準同型写像にはならないというわけ。圏の対象は群だったりするから。

なんだけど、集合なら

　　cong : ( x y : A ) → ( f : A → B ) → x ≡ y → f x ≡ f y

になります。これは Agda 的には x ≡ y が

data _≡_ {A} : A → A → Set where
refl : {x : A} → x ≡ x

と定義されてるから。つまり「項として単一化されるものが≡として等しい」ってことは、

　　項として同じ正規形を持つなら等しい

ってこと。λ式として記号的に等しいってことでもあるな。ということは、

　　圏論で Set ってのは、λ項の世界のこと

なわけ。なるほどね。Agda のSetであって、集合論のSetではないと。

　　≡←≈ : ( x y : Hom A a b ) → x ≈ y → x ≡ y

があれば、 cong-≈ は cong から作れます。上の逆は ≈ が同値関係なことからでるので。これは上の反例があるのでAgdaでは証明できません。

なので、≡←≈ を仮定して使ってれば locally small を使ってることがわかるわけ。

さらに、何か I : Set があって、

hom→ : Hom A i j → I
hom← : ( f : I ) → Hom A i j
hom-iso : hom← ( hom→ f ) ≈ f
hom-rev : hom→ ( hom← f ) ≡ f

であれば、確かに Hom A は集合だと言えます。正確には「ある集合に isomorphic 」だな。

じゃぁ、どういう局面で locally small と使うかと言うと、

　　cong-≈ を使いたい時
　　Hom Set と集合を対応させる時 (そのまんまやん)

一つは Sets の Completeness つまり Sets でのLimitの存在を示す時。同じだけど、 Limitを equalizer と product から作る時だな。
もう一つは米田レンマを使う時ですね。 フロイドの随伴関手定理は米田レンマを使うので locally small を使います。

これだけかな。

≈ は同値関係なので、 locally smallness は対応する同値類があることに相当します。じゃぁ、同値関係あるのに同値類作れないことってあるの?
選択公理がないと代表元が取れないので同値類を集合として作れない場合があるらしい。やっぱり選択公理お前だったのか。集合論に戻ってきました。