Mercurial > hg > Members > kono > Proof > category

comparison src/CCC.agda @ 1095:0211d99f29fc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Topos Sets char-iso done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 18 May 2021 15:38:46 +0900
parents 10b4d04b734f
children 321f0fef54c2
comparison
equal deleted inserted replaced
1094:bcaa8f66ec09 1095:0211d99f29fc
249 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where 249 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
250 field 250 field
251 ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ]) 251 ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
252 char-uniqueness : {a b : Obj A } {h : Hom A a Ω} 252 char-uniqueness : {a b : Obj A } {h : Hom A a Ω}
253 → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ] 253 → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
254 -- char-iso : {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) →
255 -- Iso A a a' → A [ char p mp ≈ char q mq ]
254 char-iso : {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) → 256 char-iso : {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) →
255 Iso A a a' → A [ char p mp ≈ char q mq ] 257 (i : Iso A a a' ) → A [ p ≈ A [ q o Iso.≅→ i ] ] → A [ char p mp ≈ char q mq ]
256 char-cong : {a b : Obj A } { m m' : Hom A b a } { mono : Mono A m } { mono' : Mono A m' } 258 char-cong : {a b : Obj A } { m m' : Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
257 → A [ m ≈ m' ] → A [ char m mono ≈ char m' mono' ] 259 → A [ m ≈ m' ] → A [ char m mono ≈ char m' mono' ]
258 char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) 260 char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) ( begin
261 m ≈⟨ m=m' ⟩
262 m' ≈↑⟨ idR ⟩
263 m' o Iso.≅→ (≡-iso A b) ∎ ) where open ≈-Reasoning A
259 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a 264 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a
260 ker h = equalizer (Ker h) 265 ker h = equalizer (Ker h)
261 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 ] ] 266 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 ] ]
262 char-m=⊤ {a} {b} m mono = begin 267 char-m=⊤ {a} {b} m mono = begin
263 char m mono o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono) ⟩ 268 char m mono o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono) ⟩