Mercurial > hg > Members > kono > Proof > category

comparison src/CCC.agda @ 1016:bbbe97d2a5ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Mar 2021 14:41:47 +0900
parents a104c3baefe4
children 90224a662c4e
comparison
equal deleted inserted replaced
1015:e01a1d29492b 1016:bbbe97d2a5ea
182 182
183 ---- 183 ----
184 -- 184 --
185 -- Sub Object Classifier as Topos 185 -- Sub Object Classifier as Topos
186 -- pull back on 186 -- pull back on
187 -- ○ b 187 --
188 -- b -----------→ 1 188 -- iso ○ b
189 -- | | 189 -- e ⇐====⇒ b -----------→ 1
190 -- m | | ⊤ 190 -- | | |
191 -- ↓ char m ↓ 191 -- | m | | ⊤
192 -- a -----------→ Ω 192 -- | ↓ char m ↓
193 -- h 193 -- + ------→ a -----------→ Ω
194 -- ker h h
194 -- 195 --
195 open Equalizer 196 open Equalizer
196 open import equalizer 197 open import equalizer
197 198
198 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where 199 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
199 field 200 field
200 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ] 201 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ]
201 202
202 open Mono 203 open Mono
204
205 open import equalizer
203 206
204 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) 207 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)
205 ( Ω : Obj A ) 208 ( Ω : Obj A )
206 ( ⊤ : Hom A (CCC.１ c) Ω ) 209 ( ⊤ : Hom A (CCC.１ c) Ω )
207 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])) 210 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ]))
208 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 211 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
209 field 212 field
210 char-uniqueness : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) 213 char-uniqueness : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m)
211 → A [ char m mono ≈ h ] 214 → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
212 ker-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → IsoL A m (equalizer (Ker ( char m mono ))) 215 ker-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → IsoL A m (equalizer (Ker ( char m mono )))
216 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a
217 ker h = equalizer (Ker h)
218 mm : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → A [ A [ equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ] ≈ m ]
219 mm m mono = IsoL.L≈iso (ker-iso m mono)
220 mequ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Equalizer A (char m mono) (A [ ⊤ o (CCC.○ c a) ])
221 mequ {a} {b} m mono = record { equalizer-c = b ; equalizer = m ; isEqualizer =
222 subst (λ k → IsEqualizer A k _ _ ) {!!} --
223 ( equalizer+iso (Ker (char m mono)) (Iso.≅→ (IsoL.iso-L (ker-iso m mono)))
224 (Iso.≅← (IsoL.iso-L (ker-iso m mono))) (Iso.iso→ (IsoL.iso-L (ker-iso m mono))) (Iso.iso← (IsoL.iso-L (ker-iso m mono))) ) }
225 char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
226 char-m=⊤ {a} {b} m mono = begin
227 char m mono o m ≈⟨ {!!} ⟩
228 char (ker (char m mono) ) {!!} o m ≈⟨ {!!} ⟩
229 char m mono o (ker (char m mono) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ {!!} ⟩
230 (char m mono o ker (char m mono) ) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈⟨ {!!} ⟩
231 {!!} ≈⟨ {!!} ⟩
232 (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩
233 ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
234 ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A
213 235
214 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 236 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
215 field 237 field
216 Ω : Obj A 238 Ω : Obj A
217 ⊤ : Hom A (CCC.１ c) Ω 239 ⊤ : Hom A (CCC.１ c) Ω
218 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ]) 240 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])
219 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω 241 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω
220 isTopos : IsTopos A c Ω ⊤ Ker char 242 isTopos : IsTopos A c Ω ⊤ Ker char
221 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a
222 ker h = equalizer (Ker h)
223 Monik : {a : Obj A} (h : Hom A a Ω) → Mono A (equalizer (Ker h)) 243 Monik : {a : Obj A} (h : Hom A a Ω) → Mono A (equalizer (Ker h))
224 Monik h = record { isMono = λ f g → monic (Ker h ) } 244 Monik h = record { isMono = λ f g → monic (Ker h ) }
225 char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
226 char-m=⊤ {a} {b} m mono = begin
227 char m mono o m ≈⟨ car (IsTopos.char-uniqueness isTopos m mono) ⟩
228 (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩
229 ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
230 ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A
231 245
232 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 246 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
233 field 247 field
234 Nat : Obj A 248 Nat : Obj A
235 nzero : Hom A １ Nat 249 nzero : Hom A １ Nat