Topos

卒論修論片付いたので。いや、やるべきことはあるんだけど、Topos を Agda でやってないなと言うことで。

Lambek 先生のには

　　Sub ≅ Hom(-,Ω)

とか簡単に書いてあるんだけど意味不明。Sub は Suobject Functor らしいんですが、型くらい書いてくれてもバチは当たらないんですが。

でも、もちろん、ちゃんとした定義もある。Subobject Classifier を pull back で定義するですか。実際には Equalizer 使うわけね。

書いててわかったんだけど「お前、一回もToposの定義をちゃんと読んでなかっただろ」すみません。その通りです。

record Mono　{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set　(c₁ ⊔ c₂ ⊔ ℓ)　where
　　 field
　　　　 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ]　≈ A [ mono o g ] ] → A [ f ≈ g ]

record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)　( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) :　Set ( suc c₁　⊔　suc c₂ ⊔ suc ℓ ) where
　　 field
　　　　 Ω : Obj A
　　　　 ⊤ : Hom A １ Ω
　　　　 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ])
　　　　 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω

　　　　 char-ker　: {a b : Obj A } {h : Hom A a Ω}
　　　　　　 → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ]
　　　　 ker-char : {a b : Obj A} →　(m :　Hom A b a) → (mono : Mono A m)　→ Iso A b (　equalizer-c (Ker ( char m mono )))

と割と簡単に書けた。

なんだけど、Equalizer とかがごねてるな。Agda 入れ替えたからな。と思ったら、存在量化を知らなかった頃の旧悪が露見。

Equalizer の復習からか。どこまでやるかは謎です。竹内先生の「矢印を追うだけでできるやつ。積とか」からかな。